Jacques Garrigue a écrit :
From: Guillaume Yziquel <guillaume.yziq...@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/
_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
