Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!umich!umeecs!dip.eecs.umich.edu!kfr
From: kfr@dip.eecs.umich.edu (K. Fritz Ruehr)
Newsgroups: comp.lang.functional
Subject: Re: Type Inference in ML (LML, actually)
Message-ID: <1991Jan18.183953.24158@zip.eecs.umich.edu>
Date: 18 Jan 91 18:39:53 GMT
References: <4353@undis.cs.chalmers.se> <6784@uqcspe.cs.uq.oz.au> <3603@bruce.cs.monash.OZ.AU>
Sender: news@zip.eecs.umich.edu
Organization: University of Michigan EECS Dept.
Lines: 29


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

>	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

  I don't know if he has implemented the type system for a programming
language, but a system of conjuctive types devised by R. Ghosh-Roy at Essex
attempts to resolve just the problem you describe.  The system is written up
in:

  "Conjunction-Type Standard ML Polymorphism", R. Ghosh-Roy.
  LISP and Symbolic Computation: An International Journal, 3, 381-409, 1990.
  Kluwer Academic Publishers.

His address is given at the front of the paper as:

  R. Ghosh-Roy  (ghosr@essex.ac.uk)
  Room Number 4B.526, Department of Computer Science
  University of Essex, Wivenhoe Park
  Colchester, CO4 3SQ, Essex, England, UK

He claims the following results for his system: decidability (of well-typing),
semantic soundness for all types, semantic soundness and completeness for 
basic types.

  --  Fritz Ruehr
      kfr@dip.eecs.umich.edu