Re: [Caml-list] polymorphic method.

[Guillaume Yziquel <guillaume.yziquel@citycable.ch>]

Jacques Garrigue a écrit :
> From: Guillaume Yziquel <guillaume.yziquel@citycable.ch>
>
>> By the way, I do not exactly understand the "you might end up with
>> types more polymorphic than you expected" part.
> 
> This is actually the main problem.
> At some point, I actually considered generating automatically
> polymorphic method types where possible.
> The idea would be simply to first give all the methods in a class
> monomorphic types (to avoid the undecidability of polymorphic recursion), 
> and then generalize all type variables that do not "escape": i.e. do
> not appear in class parameters, value fields, or global references.
> Technically this is perfectly doable.

Yes, I figured that out.

> Theoretically, there are problems with principality, as there is no
> most generic type for a polymorphic method (all types are incompatible
> with each other).
> It is easier to see that on a practical example.
> Say that I defined lists:
> 
> class ['a] cons x l = object (_ : 'self)
>   method hd : 'a = x
>   method tl : 'self = l
> end
> 
> class nil = object
>   method hd = raise Empty
>   method tl = raise Empty
> end

Cute way of defining lists.

> Now, both cons and nil would be typable (cons is already typable), and
> the inferred types would be:
> class ['a] cons : 'a -> 'b ->
>   object ('b) method hd : 'a method tl : 'b end
> 
> class nil : object
>   method hd : 'a
>   method tl : 'b
> end
> 
> At first glance, it seems that the type of nil being completely
> polymorphic, we could pass it as second argument to cons.
> However, it is not the case. cons has two monomorphic methods, while
> nil has two polymorhic methods, and their types are incomparable.
> If we look at object types,
> 
> type 'a cons = < hd : 'a; tl : 'b > as 'b
> type nil = < hd : 'a.'a ; tl : 'b.'b >
> 
> Of course, you could argue that what is wrong is the definition of
> nil. But basically there is no way to decide what is the right type
> for nil as soon as we allow inferring polymorphic methods.

To continue on the example of nil: the current definition of nil (i.e. 
the one with type <hd : 'a.'a ; tl : 'b.'b>) would be written as

> class nil : object
>   polymorphic method hd = raise Empty
>   polymorphic method tl = raise Empty
> end

and the definition

> class nil : object
>   method hd = raise Empty
>   method tl = raise Empty
> end

would not compile since the 'a and the 'b would not be bound in the 
definition of class nil.

Just to be sure we are talking about the same thing.

> Interestingly, currently you can define nil as an immediate object
> and have immediately the right type without any annotation:
> 
> exception Empty
> let nil = object
>   method hd = raise Empty
>   method tl = raise Empty
> end ;;
> val nil : < hd : 'a; tl : 'b > = <obj>

So you're saying that what I proposed up there, saying that it would not 
compile properly, indeed works out fine in the current setting?

Isn't that inconsistent to allow 'a coming from exceptions to get bound, 
while not doing so for some other 'a? (Sorry if I'm being unclear and 
using approximative terminology).

> let l = new cons 3 nil ;;
> val l : int cons = <obj>
> 
> So, the current approach is to privilege the monomorphic case,
> requiring type annotations for the polymorphic case. Your suggestion
> of allowing to give a hint that you want a polymorphic type makes
> sense, but it does not say which polymorphic type: there might be
> several, with different levels of polymorphism, with no way to choose
> between them. Probably it would be ok to choose the most polymorphic
> one, but one can always find counter-examples.

Humm... I still do not see why there would be ambiguity in choosing 'the 
most general' polymorphic type... Can't 'the most polymorphic one' be 
properly defined?

> So the meaning of your
> "polymorphic" keyword would be: "give me the most polymorphic type for
> this method, I hope I understand what it will be, but if I'm wrong and
> it breaks my program I won't complain". This may be practically ok,

Yes. For me, it would be OK. Even more if 'the most polymorphic one' is 
properly defined. I wouldn't worry too much about the 'I hope I 
understand what it will be' in this case.

> but this is a hard sell as a language feature. Particularly when you
> think that future versions of the compiler may be able to infer more
> polymorphic types, thanks to improvements in type inference, and
> suddenly break your program.

I'd like to suggest something naïve: for each 'a type, try to bind it to 
the class definition (what you call monomorphic I think), and if you 
can't, then bind it to the method definition (what you call 
polymorphic). (This, of course, in the presence of the 'polymorphic' 
keyword).

This seems, at least naïvely, properly defined behaviour. And from a 
practical point of view, this is what I'd be looking for.

Of course, that doesn't deal with improvements in the type inference 
system, but I think it would be neat.

I'm not really familiar with syntax extensions. Can this 'polymorphic' 
keyword be implemented with a syntax extension?

All the best,

-- 
      Guillaume Yziquel
http://yziquel.homelinux.org/