Re: [Caml-list] Type constraints

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

From: William Lovas <wlovas@stwing.upenn.edu>

> On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
> > 
> > On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> > 
> > >Is this really a counter-example? I don't see any problem with making 
> > >it polymorphic - it evaluates to ref, and ref can happily be 
> > >polymorphic.
> > 
> > Yes, well I simplified it a bit too much.  Try this instead:
> > 
> >   let module M = struct let v = ref [] end in M.v;;
> 
> I'm still not convinced.  Yes, the type variable should not be generalized
> in the above, by analogy with:
> 
>     # ref [];;
>     - : '_a list ref = {contents = []}
> 
> But the `let module' in question -- or one similar in spirit, at least --
> 
>     # let module M = struct let v = fun x -> x end in M.v;;
>     - : '_a -> '_a = <fun>
> 
> is analogous to the expression
> 
>     # fun x -> x
>     - : 'a -> 'a = <fun>
> 
> in which the type variable *is* generalized.

Analogies don't help you here, because the typechecker doesn't work by
analogies, but by explicit rules.
If you're curious, there is a function is_nonexpansive in
typing/typecore.ml. Only expressions for which this function returns
true will be generalized. (This is a direct implementation of the
syntactic value-generalization scheme.)
Now, this function doesn't now about Texp_letmodule, so any use of
this construct will never be generalized. I don't know exactly why
this was omitted, but I see the combination of two possible reasons:
this requires some amount of extra code, and one must assess its
validity. Yet I suppose this could be done.
By the way, the code is already there for immediate objects, so the
alternative approach with polymorphic methods does work (but generates
more code).

# let o = object method v : 'a. 'a -> 'a = fun x -> x end in
  fun x -> o#v x;;
- : 'a -> 'a = <fun>

Jacques Garrigue