Re: [Caml-list] Equality between abstract type definitions

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

2013/10/25 7:57、Peter Frey <pjfrey@sympatico.ca> のメール：

> Please consider the following two definitions of map which I would have
> considered equal.  
> 
>  exception Empty
> 
>  type 'a t = Cons of 'a * (int -> 'a t) * int
> 
>  let null = Cons( Obj.magic None, (fun _ -> assert false), max_int ) 
> 
>  let map (f: 'a -> 'b) (t: 'a t) : 'b t =
>      if t == null then null else match t with (Cons( h, fn, p )) ->
>      let rec aux h1 p1 =
>      try match fn p1 with (Cons (h2,_, p2)) -> 
>         (Cons(f h1, aux h2, p2 ))
>      with Empty                             -> (Cons(f h1, fn, p1)) in
>      aux h p
> 
>  let map : 'a 'b. ( 'a -> 'b ) -> 'a t -> 'b t = fun f t -> 
>    if t == null then null else match t with (Cons( h, fn, p )) ->
>    let rec aux h1 p1 =
>      try match fn p1 with (Cons (h2,_, p2)) -> (Cons(f h1, aux h2, 2 ))
>    with Empty                               -> (Cons(f h1, fn, p1)) in
>    aux h p
> 
> The second one gives the error below; no surprise.
> 
> Error: This definition has type 'b. ('b -> 'b) -> 'b t -> 'b t
>       which is less general than 'a 'b. ('a -> 'b) -> 'a t -> 'b t
> 
> Why is the first definition accepted?  

Here is the type inferred for the first definition:
val map : ('b -> 'b) -> 'b t -> 'b t = <fun>

As you can see, types for ‘a and ‘b are merged.
In OCaml, type variables used in type annotations are just unification variables:
the type checker is allowed to merge them or instantiate them.
This is useful when you want to indicate that two things have the same type,
without writing the type by hand.
In the second example you use an explicit polymorphic type, which does not
allow instantiating ‘a and ‘b, so you get an error.

Jacques Garrigue