Newsgroups: comp.lang.functional
Path: utzoo!censor!geac!nixtdc!doug
From: doug@nixtdc.uucp (Doug Moen)
Subject: Re: Type Inference in ML (LML, actually)
Message-ID: <1991Jan19.135716.22591@nixtdc.uucp>
Reply-To: doug@nixtdc.UUCP (Doug Moen)
Organization: Siemens Nixdorf
References: <54161@eerie.acsu.Buffalo.EDU> <4353@undis.cs.chalmers.se> <6784@uqcspe.cs.uq.oz.au> <3603@bruce.cs.monash.OZ.AU> <1991Jan16.225903.2540@comp.vuw.ac.nz>
Date: Sat, 19 Jan 91 13:57:16 GMT

>In article <3603@bruce.cs.monash.OZ.AU>, mmcg@bruce.cs.monash.OZ.AU
>(Mike McGaughey) writes:
>|> There *is* an anomaly in the LML type inference algorithm - one which
>|> has recently prevented my use of the language for some very elegant
>|> continuation based solutions to problems.  The simplest form of the
>|> problem is that the expression
>|> 
>|> 	let x = hd o hd in x
>|> 
>|> will typecheck properly - to (List (List *a))->*a) - whereas
>|> 
>|> 	(\x.x o x) hd
>|> 
>|> will not.  The problem with the second expression seems to be that the
>|> inference algorithm erroneously expects both of the 'x' values in the
>|> x o x to have the same type signature, when in fact it is only the _form_
>|> of the signature that should be shared (perhaps a new set of type
>|> variables should be created for each occurrence of x, and then unified
>|> in the normal way).  Thus the type of x in the expression is given as
>|> (*a->*a).

In article <1991Jan16.225903.2540@comp.vuw.ac.nz>, brian@comp.vuw.ac.nz
(Brian Boutel) writes:
>This ... is quite normal Hindley/Milner typing, and other functional
>languages behave the same way. It is usually expressed by saying that
>the type variables associated with lambda-bound variables are non-generic.
>
>Indeed it is the reason why functional languages need the let (or where)
>syntax. In all respects other than type inference, let a = b in c is
>equivalent to (\a.c)b. ...
>
>The type given to \x.x o x  is Forall t. (t -> t) -> (t -> t), but it
>would appear that a more general type is  Forall T,t. (T t -> t) -> (T(T
>t) -> t), where T is a type constructor variable, e.g T could
>instantiate to List or Tree. etc. Unfortunately, quantification over
>type constructors is second order, and undecidable.

In the latest issue of Lisp and Symbolic Computation (3, 1990),
R. Ghosh-Roy presents a new type-inference system based on conjunctive
types.  His system finds more general types, and can typecheck
a larger set of programs, than the Hindley/Milner system.  His system
is decidable and semantically sound for all types.  As far as I can tell,
'let a = b in c' is completely equivalent to '(\a.c)b' in his system.

The GR system gives '\x.x o x' the type '((*a->*b) + (*b->*c)) -> (*a->*c)'.
The + means type conjunction.  This type can be read as meaning:
  the first occurrence of 'x' in the function has type (*a->*b)
  the second occurrence of 'x' in the function has type (*b->*c)

Under GR, the expression (\x.x o x)(hd) is well typed.  Given:
  (\x.x o x) : ((*a->*b) + (*b->*c)) -> (*a->*c)
  hd : (List *d)->*d
the unification algorithm is able to find the type assignments
  *a = List(List *e)
  *b = List(*e)
  *c = *e
which results in (\x.x o x)(hd) being assigned the type List(List *e)->*e.

So ...
Is conjunctive type inference as good as it seems?
Can we expect a new family of functional languages with conjunctive type
systems to appear?  Can SML (with its module system) and Haskell (with its
type classes) be cleanly extended to use conjunctive types?
-- 
Doug Moen
{mnetor,alias,geac,torsqnt,lsuc}!nixtdc!doug
77 Carlton #1504, Toronto, Ontario, Canada M5B 2J7