Path: utzoo!censor!geac!torsqnt!lethe!yunexus!ists!helios.physics.utoronto.ca!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!kh
From: kh@cs.glasgow.ac.uk (Kevin Hammond)
Newsgroups: comp.lang.functional
Subject: Re: Type Inference in ML (LML, actually)
Message-ID: <7462@vanuata.cs.glasgow.ac.uk>
Date: 17 Jan 91 13:59:03 GMT
References: <54161@eerie.acsu.Buffalo.EDU> <4353@undis.cs.chalmers.se> <6784@uqcspe.cs.uq.oz.au> <3603@bruce.cs.monash.OZ.AU>
Reply-To: kh@cs.glasgow.ac.uk (Kevin Hammond)
Organization: Comp Sci, Glasgow Univ, Scotland
Lines: 31

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.  

NO, LML is doing the "right thing".  This is not a problem with LML,
it's a problem with Hindley/Milner polymorphic type inference.
let-bound definitions are polymorphic (ignore letrec, which is a
special case), whereas lambda-bound definitions are monomorphic.

The people at Nijmegen (Eric Nocker/Sjaak Smetsers if my memory's
correct) have a more permissive type system implemented for the Clean
GRS (based on "intersection types"), but it has a few vices of its
own...  [try rinus@cs.kun.nl -- Rinus Plasmeijer -- I don't have
Eric's address handy].

Maybe you should be using an untyped language (LML with typechecking
off?).

Kevin
-- 
This Signature Intentionally Left Blank.	E-mail: kh@cs.glasgow.ac.uk