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!craig
From: craig@leland.Stanford.EDU (Craig Chambers)
Newsgroups: comp.object
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1991Apr22.015415.28303@leland.Stanford.EDU>
Date: 22 Apr 91 01:54:15 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <3378@charon.cwi.nl>
Organization: Stanford University
Lines: 45

In article <3378@charon.cwi.nl> guido@cwi.nl (Guido van Rossum) writes:
>craig@leland.Stanford.EDU (Craig Chambers) writes:
>
>>Consider the general min function (written in a dynamically-typed
>>C-like language):
>>[...]
>>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.
>
>This can be done in ABC, a statically typed interpreted language
>developed at CWI [1].  ABC knows a single type "number" which can hold
>a float or arbitrary-precision rational, and "lists" that are
>sorted collections of values with the same type; list items may be
>lists if their types are the same, etc.; lists are sorted
>lexicographically.  If you don't want the items sorted there is a
>"table" type that lets you determine the order; tables are really
>associative arrays.

I may not have made myself clear with the problem.  I want a general
type system that will handle examples like the one I posted.  I am not
interested in languages or type systems that have built-in data
structures that solve this particular problem but do not generalize.
It sounds from your reply that ABC falls into the second category, but
since you didn't describe ABC's type system, I can't tell whether it
is a generally useful solution to a large class of problems.  What's
the type (inferred, I guess) of the arguments to the min function?
How does the compiler know that "<" in min will work?  Does the
compiler type-check each invocation of min separately (which would be
sidestepping the issue) or does it really infer a type for min that's
usable by all its callers?

Part of the description of the problem implies to me that the type
system should include some notion of subtyping and some notion of
parameterized types.  My (partially formed) solution also uses type
variables and some notion of a type pattern (I'm not sure whether or
not this is the same as a parameterized type; I'm leaning towards yes
if I can overcome some annoying technical obstacles).

If someone posts that some type system solves the problem, please also
post enough information to give people a feel for the facilities in
the type system that allow it to solve the problem.  Thanks.

-- Craig Chambers