Jacques Garrigue a écrit :
From: Guillaume Yziquel <[email protected]>
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/
_______________________________________________
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
