🚀 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).
|>

This is NOT erroneous. It is quite normal Hindley/Milner typing, and
other functional languages behave the same way. It is usually expressed
by saying that the type variables associated with lambda-bound variables
are non-generic.

Indeed it is the reason why functional languages need the let (or where)
syntax. In all respects other than type inference, let a = b in c is
equivalent to (\a.c)b. If you want the type behaviour of the let form,
use it.

The type given to \x.x o x  is Forall t. (t -> t) -> (t -> t), but it
would appear that a more general type is  Forall T,t. (T t -> t) -> (T(T
t) -> t), where T is a type constructor variable, e.g T could
instantiate to List or Tree. etc. Unfortunately, quantification over
type constructors is second order, and undecidable.

--brian
-- 
Internet: brian@comp.vuw.ac.nz
Postal: Brian Boutel, Computer Science Dept, Victoria University of Wellington,
        PO Box 600, Wellington, New Zealand
Phone: +64 4 721000