On Monday 20 June 2005 08:20, Damien Bobillot wrote:
> Hello,
>
> Look at the following code :
>
>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end
>
> Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a
> subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b.

It is not relevant. To write this, every 'a -> 'a object must be seeable as a 
'a -> 'b object, which is obviously wrong (otherwise, e.g. func 0 would have 
any type).

> I also try to use the reverse match :
>
>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l
>      end
>
> Where Module.func is of type 'a -> 'b. Ocamlc also give me an error,
> but I completely understand it here : 'a -> 'b is really not a
> subtype of 'a -> 'a.

Again, the explanation is not relevant. Here, func is not of type 'a -> 'b, 
but '_a -> '_b instead, that means that the first usage of func will freeze 
the type (you won't be able to use func 4, then func true). It happens every 
time you use references. Otherwise, you could write e.g. l := [(1,1)]; func 
true.

> In this case I also don't understand why neither " 'a -> 'b is
> included in 'a -> 'a " nor " 'a -> 'a is included in 'a -> 'b " are
> true. To my mind, one should be true.

'a -> 'b is included in 'a -> 'a, but not the contrary (intuitively, functions 
of the first type don't terminate properly, e.g. let f a = raise Exit).


Stephane Glondu.