Newsgroups: comp.lang.misc
Path: utzoo!utgpu!watserv1!watmath!watmsg.waterloo.edu!jlophel
From: jlophel@watmsg.waterloo.edu (John Ophel)
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1991Apr22.151149.9661@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <1991Apr20.010347.28984@leland.Stanford.EDU>
Date: Mon, 22 Apr 1991 15:11:49 GMT
Lines: 133

> Article: 7556 of comp.lang.misc
> From: craig@leland.Stanford.EDU (Craig Chambers)

> Here's a simple example that cannot be described by a static type
> system in most statically-typed object-oriented languages. 

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

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

> 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}})

> -- Craig Chambers


  Here is a solution in watML, an experimental dialect of ML developed here at
the University of Waterloo. watML basically adds ideas presented in the paper
by Cormack and Wright "Type-dependent Parameter Inference" SIGPLAN'90
Conference to ML. The work on watML is being done by Gord Cormack and me.

  The first problem is that if min (3,4.5) is permitted, then what is the
result type of min (integer or real)? The solution in ML is to introduce
a discriminated (tagged) union

  - datatype number = Int of int | Real of real;

Now min (Int 3, Real 4.5) will return a number object.

watML adds overloading to ML.

  - fun min (x,y) = if x < y then x else y;
  > val min = [?<: ('a * 'a) -> bool]('a * 'a) -> 'a

The reading of the type of min is, if an appropriate instance of < can be
found by searching the environment, then min is a function that takes two
arguments of the same type and returns the lesser (as defined by the
< function that was chosen). An appropriate instance of < is selected based
on having a matching type. [As an aside, min is implemented by the compiler
as a function that takes an extra parameter (<), and for any use of min, the
compiler automatically supplies the appropriate < function to use.]

We now define an instance working over numbers (the overload construct
is not in ML)

  - overload < = fn (Int i, Int j) => i < j
                | (Int i, Real r) => (real i) < r
                | (Real r, Int i) => r < (real i)
                | (Real r, Real s) => r < s;
  > val < = fn : (number * number) -> bool

In ML syntax "fn" is "lambda", so if < gets two nums, it pattern-matches
on their constructors and selects the appropriate instance of < to use. For
example, the first case will select integer < as i and j are both integers.
The next three cases will select real <.

We can now define an instance working over lists

  - overload < = fn ([],[]) => false
                  | ([],_) => true
                  | (_,[]) => false
                  | ((a::b),(c::d)) => (a<c) orelse (b<d);
  > val < = [?<: ('a * 'a) -> bool](('a list) * ('a list)) -> bool

Notice that in the last case, there are two uses of <, the first cannot
be resolved (as the list arguments are polymorphic), the second is the
instance we are defining (< over lists). The unresolved instance of < is
reflected in the type of this instance that requires an instance of <.

  - min (Int 3, Int 4);
    Int 3 : number

  - min (Int 3, Real 4.5);
    Int 3 : number

  - min ([Int 3, Int 4],[Int 4, Int 5, Int 6]);
    [Int 3, Int 4] : number list

  - min ([[Int 3, Int 4, Int 5],[Int 5], [Int 6, Real 8.9]],
         [[Real 1.2,Int 4],[Int 2]]);
    [[Real 1.2,Int 4],[Int 2]] : (number list) list

but

  - min (Int 3, [Int 4]);

  - min ([Int 3, Int 4], [[Int 4, Int 6], [Int 2, Real 3.4, Int 6]]);

both give type errors.

  
Comments
========

  - I have not attempted to explain how overloaded instances are resolved.
We are currently working on a paper that describes the system.

  - There are problems with overloading resolution, the selection
process can get into an infinite loop (in obscure cases). This needs to
be investigated.

  - Static typing solutions are occassionally more involved than dynamic typing
solutions. As more work is done with static systems, however, more and more
problems that were previously clumsy or difficult with static typing can
be naturally expressed with static typing; for example, ML's parameteric
polymorphism permits polymorphic functions to be written with the security
of static typing; ML's type inference removes the need for redundant type
declarations; watML adds overloading to a static type system. Experience
with dynamic type systems has suggested valuable concepts that languages
should be able to support; modern static type systems are attempting to provide
these concepts within secure, efficient systems.

  - Overloading with type classes is part of the Haskell language definition
(see the Haskell report or Blott & Wadler's very readable POPL'89 paper).

John Ophel