Re: [Caml-list] Question about type unification

[Jeremy Yallop <jeremy.yallop@ed.ac.uk>]

Robert Fischer wrote:
> How is the compiler magically getting from the float to a string value?  Can someone break down
> what's actually happening here for me?

Type aliases are analogous to functions.  If you have a variable "f" 
that denotes a pure function and some values u1 ... un and v1 ... vn 
then to determine whether

    f u1 ... un

is equal to

    f v1 ... vn

you call the function (twice) by substituting u1 ... un and v1 ... vn 
for the parameters.  If you have a constant function

    f = fun _ ... _ = v

then any application of the function will give the same result (v) 
regardless of the values of the arguments.  Analogously, if you have a 
type constructor "t" that denotes a type alias and some types s1 ... sn 
and t1 ... tn then to determine whether

    (s1, ... sn) t

is equal to

    (t1, ... tn) t

you "call" the type alias by substituting s1 ... sn and t1 ... tn for 
the type parameters.  If you have a "constant" type alias in which none 
of the type parameters appear on the right hand side of the definition

    type ('a1, ... 'an) t = e            a1...an not in fv(e)

then any application of the type constructor will give the same result 
(e) regardless of the values of the arguments.

Nominal types are analogous to constructors.  (By "nominal" I mean 
record and sum types, or types made abstract using a module signature.) 
  If you have a data constructor "C" and some values u1 ... un and v1 
... vn then to determine whether

    C u1 ... un

is equal to

    C v1 ... vn

you check whether ui is equal to vi for each i.  Analogously, if you 
have a type constructor "s" that denotes a nominal type and some types 
s1 ... sn and t1 ... tn then to determine whether

    (s1, ... sn) s

is equal to

    (t1, ... tn) s

you check whether si is equal to ti for each i.

In Richard's example "t" denotes a type alias.  Thus to determine whether

   unit t

is equal to

   string t

we look at the definition of t:

   type 'a t = float

then replace each 'a that occurs on the right hand side first with 
"unit" and then with "string" and compare the results.  In this case 
"'a" doesn't appear at all on the right hand side of the definition so 
we compare "float" with "float", and find that the two are equal, i.e. 
"unit t" and "string t" denote the same type (float).

Jeremy.