Re: [Caml-list] Understanding why Ocaml doesn't support operator overloading.

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

Pierre Weis wrote:

 >
 > Yes: I suspect a really nasty corner in this area. As far as I
 > remember, the kind of types you suggest is known as ``intersection
 > types'', and the type reconstruction problem for languages featuring
 > those types is just undecidable. The big problem with this kind of
 > stuff is to restrict the type schemes allowed in your type system such
 > that you do not fall into the undecidable general case, while still
 > maintaining a powerful enough type system to properly typecheck the
 > function double (fun x -> x + x).
 >

This is not the only solution: another solution is to keep the simple (in the
definition) type system with an incomplete algorithm that will always succeed
if enough type information. This works for instance for Mitchell's system F
with subtyping (see my normaliser:
<http://lama-d134.univ-savoie.fr/~raffalli/normaliser.html>)

The diffculty is that you need to have a very good way of printing typing error
message so that the user can easily guess where to add type information until
it works or a real error in the code is detected. Recent work (in a simple
setting) by Christian Haack, and Joe Wells
<http://www.cee.hw.ac.uk/ultra/compositional-analysis/type-error-slicing> let
me think that there may be a (non trivial) solution.

The big advantage, is that there are (undecidable) type systems that can
unifies typing of record, modules and object; functor and functions. Then, you
have a simpler type system definition which is easier to extend (with operator
overloading, for instance).

Remark: it does not change much the picture, because you have to find a
subsystem of the simple undecidable system. The difference, is that you can
define the subsystem by some limit to the typing complexity in the undecidable
system ... This is still far from trivial, but there is a lot of freedom (so
place for research :-).

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners