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!elaine35.Stanford.EDU!craig
From: craig@elaine35.Stanford.EDU (Craig Chambers)
Newsgroups: comp.object
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1991Apr24.032543.11704@leland.Stanford.EDU>
Date: 24 Apr 91 03:25:43 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <DUCHIER.91Apr23205041@albania.cs.yale.edu>
Sender: news@leland.Stanford.EDU (Mr News)
Organization: Stanford University
Lines: 114

In article <DUCHIER.91Apr23205041@albania.cs.yale.edu> duchier-denys@cs.yale.edu writes:
>Haskell has the notion of classes, and below is the code taken
>verbatim from the implementation of the Prelude. `instance (Ord a) =>
>Ord [a] where ...' basically means, if `a' is a type of class Ord,
>then `list of a' is also a type of class Ord, and the following
>operations are defined on it...'.

Several people have pointed at Haskell as a language including a type
system that solves the problem (a lot of people have sent e-mail to me
directly; I was actually hoping to spur group discussion rather than
request information).  And Haskell's system might be a reasonable
answer.  I've read the Haskell report, but since I've never programmed
in Haskell, I can't really tell.  I wonder e.g. whether the type
variables in the Ord class allow subtypes or whether all "instances"
of a type variable must be the same type.  I also wonder whether type
classes are a compile-time macro expansion type of thing for
overloading or whether they support run-time dynamic dispatching like
a full-fledged OO language.  I'd appreciate answers from people
more knowledgable about Haskell than me (I?).

In any case, I'll take this opportunity to post my thoughts on a type
system that attempts to solve the problem.

The type of the arguments to the min function must be things that
understand "<".  The straightforward (and broken) approach would be to
define a supertype called Ordered that is the type of these arguments:

type Ordered
	Ordered "<" Ordered: bool
	...
end Ordered

min(x:Ordered, y:Ordered):Ordered {
	return x < y ? x : y;
}

Numbers and collections of Ordered things are then made subtypes of
Ordered:

type Number <= Ordered
	Number "<" Number: bool
	...
end Number

type Integer <= Number
	Integer "<" Integer: bool { ... }
	Integer "<" Float: bool { ... }
	...
end Integer

type Float <= Number
	Float "<" Integer: bool { ... }
	Float "<" Float: bool { ... }
	...
end Float

type Collection[S]
	...
end Collection

type Collection[T <= Ordered] <= Ordered
	Collection[T] "<" Collection[T]: bool { ... }
	...
end Collection

Unfortunately, this doesn't work since it allows calls of the form
	min(3, {3,4})
which are not implemented anywhere.  In other words, Number and
Collection are not legal subtypes of Ordered since they violate
contravariance.

What we need is some "type pattern" which describes types that support
"<" on their elements, or more precisely, a pattern of two types that
can be compared (the type of the first argument to < doesn't have to
be the same as the second type).  I'm thinking that parameterized
types are such pattern types.  I'm looking at solutions like the
following:

type Ordered[T]
	T "<" T: bool
	...
end Ordered

type Number <= Ordered[Number]
	...
end Number

...

type Collection[T <= Ordered[T]] <= Ordered[Collection[T]]
	...
end Collection

min(x:Ordered[T], y:Ordered[T]):T {
	...
}

Now Number is a legal subtype of the Ordered[Number] instance of the
Ordered parameterized type (check the signatures), and similarly for
the Collection type (although this case begins to look a little
hairy).  The interface to min states that both arguments should be
subtypes of some common instance of the Ordered parameterized type,
and that the result of min is (a subtype of) this instantiating type.

However, I don't completely understand this type system.  Are type
patterns really the same as parameterized types?  Sometimes I get
confused whether I should say Ordered[T] somewhere or just T.  For
instance, I wonder whether the type of y in the min function above
could just as easily be T.  How would such a change affect what kinds
of objects can be passed to min?  I'm also trying to get this type
system to work out in a multiply-dispatched OO language that I've been
working on, and that's making the problem (for me) even harder.

-- Craig Chambers