Mark Shinwell wrote:
Is there any theoretical reason why the compiler couldn't just deem
applications of the form given by the original poster as total, even though
it results in the loss of some expressibility? Perhaps it would be easier
to improve the error messages in that case... or perhaps it just results in
too little expressibility for some reason.
You'd have to distinguish between terms which refer to polymorphic
functions and terms whose type is only partially known. I suspect it
might be quite difficult to do that in a way that interacts
satisfactorily with type inference. Even the current design has a
rather unfortunate dependence on the particular order of execution of
the type inference algorithm. For example, given a definition
let h = fun ~x:() () -> ()
the following program is allowed
let g f x = ([f; h], f x)
whereas the following rather similar program is not
let g f x = (f x, [f; h])
If the type inference algorithm sees `[f; h]' first then it gives f a
fully-known labeled type and allows it to be applied without a label
when it subsequently encounters `f x'. If it sees `f x' first then it
assigns an unlabeled type to f, which subsequently fails to unify with
the type of h.
I agree that the current behaviour is surprising, but I'm not sure that
it's easy to make it much less surprising, even if you're willing to
give up some expressiveness.
Jeremy.
_______________________________________________
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
