Re: polymorphic method.

Re: polymorphic method.

[Guillaume Yziquel]

Hello.

When developing with objects in OCaml, I'm quite often faced with 
polymorphic methods.

Such as:

class myobject = object
   method id x = x
end

Sometimes you have many methods that you're tinkling with, and the 
compiler keeps saying to you that 'a is inbound in this class declaration.

I'm therefore wondering if it would be a good idea to have a keyword 
'polymorphic', and one would write

class myobject = object
   polymorphic method id x = x
end

The polymorphic keyword would be a hint that the method is polymorphic 
and that there is no need to look at the class' type parameters.

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

polymorphic method.

[Guillaume Yziquel]

Hello.

When developing with objects in OCaml, I'm quite often faced with 
polymorphic methods.

Such as:

class myobject = object
   method id x = x
end

Sometimes you have many methods that you're tinkling with, and the 
compiler keeps saying to you that 'a is inbound in this class declaration.

I'm therefore wondering if it would be a good idea to have a keyword 
'polymorphic', and one would write

class myobject = object
   polymorphic method id x = x
end

The polymorphic keyword would be a hint that the method is polymorphic 
and that there is no need to look at the class' type parameters.

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

Re: [Caml-list] polymorphic method.

[Jacques Garrigue]

There are already polymorphic methods in ocaml.
The syntax for your example would be:

class myobject = object
  method id : 'a. 'a -> 'a = fun x -> x
end

A "polymorphic" keyword might seem simpler, but it would be complex to
handle the case where a polymorphic method type contains also class
parameters:

class ['a] cell (x : 'a) = object
  method pair : 'b. 'b -> 'a * 'b = fun y -> (x,y)
end

More generally, you might end up with types more polymorphic than you
expected, and since differently instantiated polymorphic method types
are incompatible, this would be a problem.

Jacques Garrigue

From: Guillaume Yziquel <guillaume.yziquel@citycable.ch>
> When developing with objects in OCaml, I'm quite often faced with
> polymorphic methods.
> 
> Such as:
> 
> class myobject = object
>   method id x = x
> end
> 
> Sometimes you have many methods that you're tinkling with, and the
> compiler keeps saying to you that 'a is inbound in this class
> declaration.
> 
> I'm therefore wondering if it would be a good idea to have a keyword
> 'polymorphic', and one would write
> 
> class myobject = object
>   polymorphic method id x = x
> end
> 
> The polymorphic keyword would be a hint that the method is polymorphic
> and that there is no need to look at the class' type parameters.
> 
> -- 
>      Guillaume Yziquel
> http://yziquel.homelinux.org/

Re: [Caml-list] polymorphic method.

[Guillaume Yziquel]

Jacques Garrigue a écrit :
> There are already polymorphic methods in ocaml.
> The syntax for your example would be:
> 
> class myobject = object
>   method id : 'a. 'a -> 'a = fun x -> x
> end

Yes, I know that there are already polymorphic methods in ocaml.

> A "polymorphic" keyword might seem simpler, but it would be complex to
> handle the case where a polymorphic method type contains also class
> parameters:
> 
> class ['a] cell (x : 'a) = object
>   method pair : 'b. 'b -> 'a * 'b = fun y -> (x,y)
> end

Indeed. But you could also write:

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

The polymorphic keyword would only bind what can be bind. Since x is 
already of type 'a, it would escape the scope of the 'polymorphic' 
keyword. But y would not escape the scope of the polymorphic keyword.

> More generally, you might end up with types more polymorphic than you
> expected, and since differently instantiated polymorphic method types
> are incompatible, this would be a problem.

Well, for now, when I write methods, my methods tend to be not 
polymorphic enough. One could keep the default behaviour without the 
keyword, and also use the keyword polymorphic to bind only what can be 
bound (i.e. not 'x' in your example).

The problem I am facing now is cumbersome: writing types for methods 
arguments everywhere... That's not what people would expect for type 
inference, unfortunately. The 'polymorphic' keyword would only be a hint 
as to how type inference would be done. This way I wouldn't have to keep 
the typing of the method arguments in sync with the code of the method 
(or at least, much less).

By the way, I do not exactly understand the "you might end up with types 
more polymorphic than you expected" part.

> Jacques Garrigue

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

Re: [Caml-list] polymorphic method.

[Jacques Garrigue]

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

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.

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>

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

Jacques Garrigue

Re: [Caml-list] polymorphic method.

[Guillaume Yziquel]

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/

Re: [Caml-list] polymorphic method.

[blue storm]

On Thu, Sep 10, 2009 at 9:14 PM, Guillaume Yziquel
<guillaume.yziquel@citycable.ch> wrote:
> I'm not really familiar with syntax extensions. Can this 'polymorphic'
> keyword be implemented with a syntax extension?

No, it can't. If you're talking about camlp4 syntax extensions,
they're converted to regular OCaml programs at camlp4-time, wich is
*before* the compiler see the program. It thus can't access any type
information : you can have syntax extensions that send type
information to the typer, but not the other way around : only purely
syntaxic transformations are expressible.
With a camlp4 extension, you could inspect the (syntaxically explicit)
parameters of you method, and (syntaxically) generate a polymorphic
type for each one : "polymorphic method foo bar baz = ..." would be
translated into "method foo : 'a 'b . 'a -> 'b -> 'c = fun (bar : 'a)
(baz : 'b) -> ...".
This is probably not what you want. You could further enrich your
extension with a "param" keyword that would not generate polymorphic
types for some of the parameters "method foo bar (param baz) = ..", or
have the "poly" keyword be parameter-specific "method foo (poly bar)
baz = ...", but my general advice is not to try to much to do
type-level transformation by syntaxic transformations : they tend to
get flawed in ways you don't expect, and this is just not the right
tool for the job.

Re: [Caml-list] polymorphic method.

[Jacques Garrigue]

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

Re: [Caml-list] polymorphic method.

[Guillaume Yziquel]

blue storm a écrit :
>
> With a camlp4 extension, you could inspect the (syntaxically explicit)
> parameters of you method, and (syntaxically) generate a polymorphic
> type for each one : "polymorphic method foo bar baz = ..." would be
> translated into "method foo : 'a 'b . 'a -> 'b -> 'c = fun (bar : 'a)
> (baz : 'b) -> ...".
> This is probably not what you want.

Indeed, it's not what I want.

> but my general advice is not to try to much to do
> type-level transformation by syntaxic transformations : they tend to
> get flawed in ways you don't expect, and this is just not the right
> tool for the job.

Too bad there's no "type checking extension" in Objective Caml. That 
would be huge fun.

Thanks.

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

Re: [Caml-list] polymorphic method.

[Guillaume Yziquel]

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/