Re: [Caml-list] polymorphic method.

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

Jacques Garrigue a écrit :
> 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

fold would here have type 'a 'b. 'b -> 'a -> 'a with the proposed use of 
the polymorphic keyword.

> class nil : object
>   method fold : 'a 'b. 'a -> 'b -> 'b
> end

OK. Same type.

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

fold would have type 'c. ('a -> 'c -> 'c) -> 'b -> 'c

And if you take into account the nil construct, then you would have 'b = 
'c. But that's not the case here.

> class  ['a] cons : 'a -> 'b -> object ('b)
>   method fold : 'c. ('a -> 'c -> 'c) -> 'c -> 'c
> end

Yes, we broadly agree here.

> 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

I perfectly agree that one needs to be fully explicit to get the right 
types. Or what would perhaps be best, use a class type.

But, without wanting to offend you, this is rather theoretical. I do not 
say that it is not important, far from it. But you're showing the use of 
two different interacting classes and showing me that using the 
polymorphic keyword, I might not get what I want. From a practical point 
of view, I'm using (now) only one class with lots of methods, and lots 
of parameters. Which is a rather common situation. So we're not here in 
the exact same situation.

If I do not use the polymorphic keyword, I would still get the problem 
of having to type explicitely the fold method of the nil element. Using 
the polymorphic keyword, I still would. I do not see any improvement or 
any disadvantage from this point of view when it comes to the 
'polymorphic' keyword.

class ['a] nil = object
   polymorphic method fold (f : 'a -> 'b -> 'b) x = x : 'b
end

would be perfectly fine for me. At least better than

class ['a] nil = object
   method fold : 'b. (('a -> 'b -> 'b) -> 'b -> 'b) = fun f x -> x
end

The polymorphic keyword's only purpose would to avoid having to manually 
set types when developing methods incrementally, like adding arguments, 
erasing the only occurence of an argument in the method's code. Without 
a polymorphic keyword, these are a pain.

The former is neater when it comes to developing OO code. The latter is 
a pain because you have to mentally disconstruct the method type, match 
the right argument, et ceterae.

Of course, like any other thing, (seesaws, teddy bears, demineralised 
watter), wrong usage might lead to adverse consequences. The 
'polymorphic' keyword wouldn't be a typing miracle, just a mere 
convenience for OO development.

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

I'll have to slowly swallow this one.

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

Well if the most polymorphic one is well defined, I'd rather have this 
one than anything else. Remember that if you want to bound a type to the 
class, you always can:

class ['a] myobject = object
   polymorphic method (x : 'a) y = ([x], y)
end

would have type

class ['a] myobject = object
   method : 'b. ('a -> 'b -> 'a list * 'b)
end

In essence, in the current setting, you try to bind as monomorphic as 
possible when it comes to keywords. With a polymorphic keyword, you 
would try to be as polymorphic as possible.

These are two possible extremes. So I'd rather, as a programmer, have 
the option of choosing 'polymorphic' over having no option. If I have to 
tweak the typing to get the 'polymorphic' keyword to choose the right 
polymorphic type, well, anyway, it's not worse than it is today.

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

In fact, I believe that these interactions would be beneficial. It's 
always a pleasure to see that a tiny modification in the code moves the 
type system all around. It's what makes OCaml a pleasure to work with 
when heavily modifying code. Once we get used to the implications of 
using a 'polymorphic' keyword, I believe it to be as beneficial.

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

I believe that this is what I would want. Yes.

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

I'd love to see this keyword. However, I'd also love to hear other 
opinions about this.

Concerning beginners, I'm not sure we should advertise that much to 
beginners. What I'm concerned, when it comes to beginners, is that it 
will hide polymorphic typing for too long. They'd get used to the 
'polymorphic' keyword, and would be bewildered by an explicitly 
polymorphic type.

By the way, what's the big deal with principal vs. correct?

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

I won't hold my breath. But thanks.

> 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 strongly disagree on this one. I'm currently trying to generate OCaml 
code for a Swig module, and I'd be so glad not to have to write more 
generated code.

More seriously, I think that the current situation is quite lean. You 
just have to wrap your head around the OO type system once or twice, and 
you're done with it. And the type inference for objects is as useful as 
the type inference if for 'regular' OCaml.

I'd rather have a 'polymorphic' keyword to smoothen type inference than 
no type inference (and only type checking) for objects and classes.

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