Le vendredi, 21 fév 2003, à 04:30 Europe/Paris, John Max Skaller a 
écrit :

> BTW: I've always been baffled by the seeminly wrong nomenclature
> 'generalisation' when in fact unification involves *specialising*
> types/type variables. Does it refer to the seeking of the
> 'most general' unifier -- that is, the most general specialisation?
>
> Error messages like
>
> "The type of this expression, ('_a, `_b) Hashtbl.t,
> contains type variables that cannot be generalized"
>
> seem counterintuitive when in fact the problem is
> that variables can't be made specific enough.

Generalisation refers to transforming a free type variable into a 
universally quantified type
variable. Hindley-Milner polymorphism is more than first order 
unification, it allows
instantiation of a variable by types mutually incompatible. This is why 
ML allows
let i x = x in (i "a",i 0) c
because i has a truly polymorphic type a -> a, which get instantiated 
in string -> string
and int -> int, even though string and int are not unifiable.
Or even better :
  let i x = x in (i i);;
  - : '_a -> '_a = <fun>
and indeed :
let foo = let i x = x in (i i) in (foo foo);;
This expression has type 'a -> 'a but is here used with type 'a

The trick is that "let x=M in N" is treated differently from the redex 
(fun x->N)M,
and rather like M[x<-N] where the various occurrences of x may receive 
different type
assignments

GH



-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners