Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!olivea!mintaka!bloom-beacon!eru!hagbard!sunic!mcsun!hp4nl!charon!guido
From: guido@cwi.nl (Guido van Rossum)
Newsgroups: comp.object
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <3392@charon.cwi.nl>
Date: 22 Apr 91 15:38:14 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <3378@charon.cwi.nl> <1991Apr22.015415.28303@leland.Stanford.EDU>
Sender: news@cwi.nl
Lines: 88

>>	[me]
>	[craig]

craig@leland.Stanford.EDU (Craig Chambers) writes:

>In article <3378@charon.cwi.nl> guido@cwi.nl (Guido van Rossum) writes:
>>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.

I still don't quite understand your gripe, so here's an explanation of
ABC's type system.  It solves much more than the particular problem
you stated, and I believe that the type system could be extended to
handle cases currently not supported by the language.  Look for
yourself:

- basic types: numbers and strings
- type constructors:
	- tuple containing <type1>, <type2>, ...
	- list of <type1>
	- table with keys of <type1> and values of <type2>
- There are no pointers, nor function variables
- There are no unions
- There is no way to explicitly introduce a new type
  (there are infinitely many types possible through the type
  constructors though)
- Functions may be polymorphic
- The type inference system is "bootstrapped" with knowledge about
  the built-in operators; e.g., "+" requires two number arguments and
  returns a number, "^" operates on strings and returns a string, "#"
  (the length function) operates on strings, lists and tables, etc.

>What's the type (inferred, I guess) of the arguments to the min function?

It is (<alpha>, <alpha>), where <alpha> stands for any type but the two
occurrences must match.  This leaves the actual type unrestricted but
says that the two arguments must have the same type.

>How does the compiler know that "<" in min will work?

From the definition of min it concludes that the arguments must be
comparable to each other.  The definition of the built-in "<" operator
says that two types are comparable to each other if they are the same
type.  [As I said, ABC has no compiler since is interpreted, but
that's beside the point -- there is a static type checker that must
accept a program before it is ever passed to the interpreter.]

>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?

The latter.  Min's type would be "function with (<alpha>, <alpha>)
argument returning <alpha>".  ABC's type checker uses a unification
algorithm to combine the various things it learns about variables and
functions.

>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.

I am not a type theorist, just a former member of the ABC
implementation group, so it may be difficult for me to explain ABC's
type system to you.  Hope this has helped.  If not, I'll ask its
designer to take over...

--Guido van Rossum, CWI, Amsterdam <guido@cwi.nl>
"If this is Bolton, I shall return to the pet shop"