Re: [Caml-list] polymorphic method.

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

From: Guillaume Yziquel <guillaume.yziquel@citycable.ch>

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

This is indeed what you are proposing. But from my point of view the
distinction is not really relevant: one can easily build examples
where methods should be polymorphic, but not maximally.
A typical example is fold:

class nil = object
  polymorphic method fold f x = x
end
class nil : object
  method fold : 'a 'b. 'a -> 'b -> 'b
end

class ['a] cons (h:'a) (t : 'self) = object (self : 'self)
  polymorphic method fold f x = f h (t#fold f x)
end
class  ['a] cons : 'a -> 'b -> object ('b)
  method fold : 'c. ('a -> 'c -> 'c) -> 'c -> 'c
end

As you can see, the right type is going to be inferred for cons (and a
polymorphic one!), but again the type for nil is wrong.
In order to obtain the right one, you must be fully explicit:
class ['a] nil = object
  polymorphic method fold (f : 'a -> 'b -> 'b) (x : 'b)  = x
end

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

This doesn't work because of raise, but because I used an immediate
object rather than a class. Immediate objects may have implicit
polymorphism at the object level (not at the method level), while
everything must be explicit in classes (because classes define types also).

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

The most polymorphic one is properly defined, as a function of the
current type system (which may always be improved). But the most
polymorphic one is not necessarily the one you want, as my example
with nil shows. And once you have a polymorphic type, there exists an
infinity of other valid polymorphic types for the same method
(obtained by instantiating repeatedly type variables with ['a option]
for instance).

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

Since type inference is properly defined, it is properly defined.
Unfortunately the rules are not available on paper, while this could
be done. It would still be a rather big definition, and the property
is, with lots of interactions, which is why I added the 'I hope I
understand'. Yet, I'm not too afraid of this part.

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

I'm not sure what you mean by that. If the class definition has type
parameters, you could always choose to bind the remaining free type
variables to those type parameters, and be done with it. Of course
this is completely arbitrary, an probably not what you expect.

But this is not really a problem, because the approach I gave in my
previous mail could do the job correctly. In more detail:
* First infer monomorphic types for all methods (with eventually some
  type variables remaining), just like you would do for mutually
  recursive let-definitions. Only methods with explicit polymorphic
  types can be used polymorphically at this point.
* Mark all type variables that appear either in class parameters,
  class arguments, value fields or global references, as
  non-generalizable.
* In methods marked as polymorphic, generalize the remaining type
  variables to obtain the resulting type of the method.
* In public methods, remaining type variables that are not bound
  neither at the class or method level are an error for class
  definitions (but not for immediate objects).

This is a correct behaviour, and I believe it should do exactly what
you expect.  Thanks to the introduction of a new keyword for
polymorphic inference, it is also compatible with the current
behaviour for immediate objects.  But, as mentioned before, what it
provides is the most polymorphic type, not the principal type (a type
that would subsume all the possible ones), as there is no subsumption
on polymorphic method types.

So, should I go forward I implement it?
This would be nice to give it a try, but:
* type inference for classes is rather hairy, so I'm afraid it will
  not be easy to implement
* it is correct but not principal, and we don't like it very much in
  ocaml
* while it avoids having to write the method types by hand, you still
  need to know which methods will be polymorphic, so I'm not sure it
  will help beginners
* adding yet another keyword is not that great...

So if find time with nothing else to do I might try with a prototype,
but don't hold your breath.

At times I even think that all class definitions should be accompanied
by a class interface, with explicit types for all public methods.
This would certainly avoid all these ambiguities with variable binding
in types.

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

The keyword, yes; the behaviour, no.
And this goes much farther than the fact you have no access to types
in camlp4. Implementing it requires lots of changes to the type
inference itself.

Jacques Garrigue