Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!mcsun!hp4nl!utrcu1!infnews!infnews!joosten
From: joosten@cs.utwente.nl (Stef Joosten)
Newsgroups: comp.lang.functional
Subject: Re: Type Inference in ML (LML, actually)
Message-ID: <1991Jan23.101919@cs.utwente.nl>
Date: 23 Jan 91 09:19:19 GMT
References: <4353@undis.cs.chalmers.se> <6784@uqcspe.cs.uq.oz.au> <3603@bruce.cs.monash.OZ.AU> <1991Jan18.183953.24158@zip.eecs.umich.edu>
Sender: usenet@cs.utwente.nl
Reply-To: joosten@cs.utwente.nl (Stef Joosten)
Organization: University of Twente, Dept. of Computer Science
Lines: 27


  mmcg@bruce.cs.monash.OZ.AU (Mike McGaughey) writes:

>	can anyone point me to an algorithm or paper
>	describing a polymorphic type system which does not share this
>	anomaly?

A very nice solution is offered in the thesis of Mirjam Gerritsen:

   M. Gerritsen
   Type Assignment Functions
   PhD thesis, University of Twente, Comp. Sc., the Netherlands, 1988.

postal address:
   Functional Programming Group, Comp. Sc.
   University of Twente,
   postbus 217
   7500 AE  ENSCHEDE
   the Netherlands

In this thesis Mirjam Gerritsen gives a typing algorithm (proof included),
and shows that Mike's problem is covered, and also proves that
Milner/Hindley typing is still completely covered.
Furthermore, she shows how to build an efficient implementation.

Good luck to all of you.
Stef Joosten