🚀 go-pugleaf

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).
|> 
|> I have three questions: can anyone point me to an algorithm or paper
|> describing a polymorphic type system which does not share this
|> anomaly?  Are there any readily available lazy functional languages
|> which use this system?  Has anyone modified the LML compiler to do
|> this? (looks around hopefully... :-)
|> 
|> Cheers,
|> 
|>     Mike.

Read the PhD thesis "M. Gerritsen, Type Assignment Functions" 1988.
University of Twente

She built a type inference algorithm where the occurrences of variables
not necessarily have the same type.
Instead she uses `conjuction types': *a & *b .
(\x.x o x) has the type ((*b->*c)&(*a->*b))->*a->*c which sais that x
must be
instantiatable as *a->*b and as *b->*c .
Application of (\x.x o x) to hd yields the equations:
	*a->*b = List *d->*d  (and so: *a=List *d,   *b=*d)
	*b->*c = List *e->*e  (and so: *b=List *e,   *c=*e)
The two occurrences of x have types List *d->*d and List *e->*e
respectively.
Solving the equations yields:
	*a=List (List *e)
	*b=List *e
	*c=*e
	*d=List *e
and so
	(\x.x o x) hd::*a->*c = List (List *e)->*e

In this type inference system there is no more need for an explicit
let-construct.
All Milner-typable expressions are also typable in this scheme, but
some
non Milner-typable expressions too.
Try `twice twice k' where
	twice f x = f (f x)
	k x y = x

Mark Ramaer