Xref: utzoo comp.object:3264 comp.lang.misc:7545 comp.lang.eiffel:1520
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!decwrl!stanford.edu!leland.Stanford.EDU!leland.Stanford.EDU!craig
From: craig@leland.Stanford.EDU (Craig Chambers)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: A Hard Problem for Static Type Systems
Message-ID: <1991Apr20.010347.28984@leland.Stanford.EDU>
Date: 20 Apr 91 01:03:47 GMT
Sender: news@leland.Stanford.EDU (Mr News)
Reply-To: craig@self.stanford.edu
Organization: Stanford University
Lines: 62


Here's a simple example that cannot be described by a static type
system in most statically-typed object-oriented languages.  I'm using
it to help me make sure that the static type system in my new OO
language is sufficiently powerful, but you could use it as another
example of a simple, useful program that is handled simply in a
dynamically-typed system that requires a lot of sophistication in a 
statically-typed system.

Consider the general min function (written in a dynamically-typed
C-like language):

    min(x, y) {
    	if (x < y) {
    	    return x;
    	} else {
    	    return y;
    	}
    }

Assume that we have two kinds of numbers in our language, integers and
floats, and that we've defined implementations of "<" for all four
combinations of integer and float arguments.  We define number as the
common supertype of both integers and floats; since we've defined all
possible combinations, "<" is defined over pairs of numbers.

We also have a collection hierarchy.  The "<" message is defined for
all collections of things that themselves understand "<" to do
lexicographic ordering of two collections.

Note that we do NOT have a "<" message that can take a number as one
argument and a collection as the other.

Here's the problem: we'd like to describe the type of the min
function, so that this one piece of source code can be used to compute
the minimum of two numbers or of two collections of numbers or of two
collections of collections of numbers, etc.

So here are some examples that should type-check:

    min(3, 4)
    min(3, 4.5)
    min({3,4}, {4,5,6})
    min({{3,4.5},{5},{6,8.9}}, {{1.2,4},{2}})

And here are some that shouldn't:

    min(3, {4})
    min({3,4}, {{4,6},{2,3.4,6}})

We're only allowed to use static type systems that actually make
static guarantees about no message-not-understood problems; otherwise,
we'd just be using dynamic typing.  This therefore disallows using
Eiffel's (old, currently implemented) type system based on covariant
typing.

I'm not saying that this cannot be done in a static type system; I'm
hoping that it can, in fact.  I will claim (with the hope of being
disproved) that no "practical" existing language can statically
type-check this example.

-- Craig Chambers