Re: [Caml-list] signature and 'a generic types

[Michael Alexander Hamburg <hamburg@fas.harvard.edu>]

Quoting Damien Bobillot <damien.bobillot@m4x.org>:

> 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. Nevertheless ocamlc
> give the following error :
>
>      Values do not match:
>        val func : 'a -> 'a
>      is not included in
>        val func : 'a -> 'b
>
> Why ?
>

The module signature requires that the function have type 'a -> 'b for all 'a
and 'b, i.e. the declared type must be a subtype of the actual type, not vice
versa.  Imagine if the compiler let you use that module definition, someone
calling the module would be able to say "hello" ^ Module.func 1, and OCaml
would try to treat 1 as a string because func is declared to have type 'a ->
'b.

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

Ah, but the function you declared is not of type 'a -> 'b but rather of type '_a
-> '_b, because ref [] does not refer to _every_type_ ('a ref), but rather
_one_single_type_ ('_a ref).  This is the infamous "value polymorphism
restriction".  Here's why it's there:

let l = ref [] (* type of l is '_a list ref, not 'a list ref *)
let () = l := ["hello"] (* if there were no VPR, l would still have type 'a list
ref here, but because it has one single type, it is now a string list ref *)
let x = 1+List.head !l (* if there were no VPR, this would be allowed, and try
to compute 1+"hello" *)
let () = l := [7] (* this is also disallowed by the type of l.  You can't get it
back to being an '_a list ref *)

In any case, 'a -> 'a is not a subtype of '_a -> '_b.  If your func had been
Obj.magic, or a -> List.assoc a [], or a -> failwith "Hello world", it would
have worked (I think, I don't have OCaml in front of me).

> 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.
>
> Is it a caml limitation/bug, or am I wrong somewhere ?

Sort of.  First, the VPR is somewhat more restrictive than it has to be for type
safety, but analyzing exactly how restrictive is has to be in a particular case
is hard (very hard in this case; it's hard for the compiler to know that a
particular piece of mutable state will never be mutated anywhere), and would
require extra notation to avoid breaking across module boundaries.  The current
restriction is sort of a happy medium.

Second, in OCaml, polymorphic types are abbreviated.  "'a -> 'a" is an
abbreviation of "for all types 'a, 'a -> 'a", whereas "'_a -> '_a" is an
abbrevation of "for one single arbitrary type 'a, 'a -> 'a".  These
abbreviations are somewhat confusing.  They also assume knowledge of a
restriction of so-called Hindley-Milner types, which is that all the "forall"s
go out in front.  This restriction is required for automatic type detection to
be computable, so it can be lifted only if the user specifies the type.  For
some reason, in OCaml the syntax only allows you to do this in record
declarations, which could probably be considered a "limitation/bug".

Mike Hamburg

> --
> Damien Bobillot
>
>