This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Type constraints
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2004-12-07 (21:04) From: Damien Doligez Subject: Re: [Caml-list] Type constraints
```On 7 Dec 2004, at 19:08, Alain Frisch wrote:

> I still don't understand. Compare:
>
> # module M = struct let v = ref [] end;;
> module M : sig val v : '_a list ref end
> # module M : sig val v : 'a -> 'a end = struct let v x = x end;;
> module M : sig val v : 'a -> 'a end
>
> Of course, the type variable in the first example must not be
> generalized, and it isn't. In the second example, there is no problem.
> We get:
>
> # M.v;;
> - : 'a -> 'a = <fun>
>
> So why not give the same type scheme to:
>
> let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v

The typing algorithm is very simple (really!):

1. Type the module. Generalization occurs and the v field gets a
polymorphic type.
2. Type "M.v".  This takes an instance of the polymorphic type.
3. Can we generalize it?  Look at the syntactic shape of the expression
(in this case, let module ... in ...).  If it is always safe to
generalize such expressions, OK.  If not, do not generalize.

That's the beauty of the Wright criterion: it's very easy to implement
and to understand (because it is syntactic), and works well in almost
all
cases (with a little eta-expansion if needed).

So the answer to your original question is: the type is not generalized
because in some cases the let-module construct is not safely
polymorphic.

Of course, there must be some criteria for generalizing more
expressions.  Check out Xavier's thesis for example.  They are usually
not worth the trouble.

-- Damien

```