Path: utzoo!censor!geac!torsqnt!lethe!yunexus!ists!helios.physics.utoronto.ca!news-server.csri.toronto.edu!bonnie.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!usc!samsung!munnari.oz.au!bruce!mmcg
From: mmcg@bruce.cs.monash.OZ.AU (Mike McGaughey)
Newsgroups: comp.lang.functional
Subject: Re: Type Inference in ML (LML, actually)
Message-ID: <3603@bruce.cs.monash.OZ.AU>
Date: 16 Jan 91 19:21:47 GMT
References: <54161@eerie.acsu.Buffalo.EDU> <4353@undis.cs.chalmers.se> <6784@uqcspe.cs.uq.oz.au>
Organization: Monash Uni. Computer Science, Australia
Lines: 33

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.
-- 
Mike McGaughey			ACSNET:	mmcg@bruce.cs.monash.oz

"His state is kingly; thousands at his bidding speed,
 And post o'er land and ocean without rest."		- Milton.