Re: [Caml-list] Type constraints

[nakata keiko <keiko@kaba.or.jp>]

Damien Doligez wrote:
> On 8 Dec 2004, at 04:30, nakata keiko wrote:
> 
> > This does not answer to me why this works,
> >
> > #type t = { t : 'a. 'a -> 'a}
> >
> > #let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, 
> > v.t true)
> 
> You'll have to ask Jacques about this.  He's the one who added 
> polymorphic
> methods and polymorphic record labels to the language, and I'm not sure
> I understand all the implications.

I have the impression that if the above code is type checked,
then, something like the following code could be type checked.
What is the differences?

> > However, if I can write something like
> >
> > #let v : 'a. 'a -> 'a = let module M = struct let t x = x end in  M.t 
> > in (v 5, v true)
> >
> > then, it would be type checked ?
> 
> I doubt it.  For the moment, a type constraint can only specialize the
> type of an expression.  You're asking for a generalization constraint.
> I have no idea whether that can be implemented, but I think it would
> require some big changes to the typechecker.

Regards,
Keiko.