[LONG] Re: Overloading

From: Francois Rouaix (Francois.Rouaix@inria.fr)
Date: Fri Mar 13 1998 - 09:56:49 MET


Message-Id: <199803130856.JAA04394@madiran.inria.fr>
From: Francois Rouaix <Francois.Rouaix@inria.fr>
To: caml-list@inria.fr
Subject: [LONG] Re: Overloading
Date: Fri, 13 Mar 1998 09:56:49 +0100

As it's been said in this thread, we've been working on overloading for
quite a long time. This is a (not so) short summary prepared with Pierre:

 [1988-1990]
 - Pierre Weis put some overloading in Caml (Classic Caml as we now call it).
 It supported static overloading of polymorphic function. This means that you
 could overload arithmetic operators (such as +), but polymorphic functions
 as well (such as map on lists, arrays, etc...). The compiler would replace
 overloaded symbols at compile-time with their appropriate instance, and
 reject the program if there was any ambiguity. This approach was not
 pursued because its interaction with the type-checker was considered too
 tricky. Also, while you could overload "print" (as you can expect),
 let print_list l = List.iter print l
 would not behave as expected (it would print any list as
 <poly> <poly> <poly> ....).
 This prompted the study of type-systems where type information (computed
 statically) is passed at run-time to select correct instances of overloaded
 symbols.

 [1988-1992]
 - I worked on Alcool for my thesis. To make a long story short, it was the
 same kind of overloading as in Haskell, except that you needn't define
 classes, since the type system was using a type algebra with extensible
 records, based on Didier Remy's work of 1989. The Alcool type system had
 some cool aspects, but produced "unfriendly types", to say the least. Those
 of you who are familiar with object types in OCaml (and especially type
 errors with objects) known what I mean (check the POPL'90 paper for the
 details).

 [1990-1995]
 - Pierre, Catherine Dubois and later myself worked on "generics", also named
 "Extensional polymorphism", which is closer in spirit to CLOS than to
 Alcool/Haskell polymorphism. I actually implemented this system on top
 of Caml Light, so to the easiest way to explain the system is to give some
 short examples (check the POPL'95 paper if you want the formal system):

generic add = case #a -> #b -> #c of
   << int -> int -> int >> -> add_int
 | << float -> float -> float >> -> add_float
 | << int -> float -> float >> ->
       (fun x y -> add_float (float_of_int x) y)
 | << float -> int -> float >> ->
       (fun x y -> add_float x (float_of_int y))
;;

generic is a modified "let", which defines an ad-hoc polymorphic value
by pattern-matching on types. It's compiled as a function taking a type
parameter and returning a normal value. At occurrences of a generic-defined
symbol, the instance type is passed to the function.

You can then write: "add 1 1", "add 1 1.3", etc..., but also
let double x = add x x in double 1, double 1.3
which shows that this ad-hoc polymorphism mixes well with traditionnal
polymorphism.

This other example:
generic length =
case #a -> int of
   << string -> int >> -> string_length
| << #ty vect -> int >> -> vect_length
| << 'a list -> int >> ->
          (fun _ -> print_string "'a list !"; 0)
| << #ty list -> int >> -> list_length
;;

shows that you can overload on polymorphic functions, and that you don't
have the Haskell restriction on the arity of types on which you overload
(e.g. here, we overload on "string" and "'a list").

Then, the fun begins when you realize that you can write functions that
mix computations on values and types, as in the tautology checker

generic rec taut =
  case #a -> bool of
    <<bool -> bool>> ->
        (fun x -> x)
 | <<(bool -> #ty) -> bool >> ->
        fun f -> taut (f true) & taut (f false)
;;

taut is defined on a whole family of functions with different types, such as:

taut (fun x -> x or true)
or
taut (fun x y z -> (x or y) or (not x or z))

Finally, a really tricky example:

generic rec curryn =
  case #a -> #b of
   << (#ty1 * #ty2 -> #ty3) -> #ty1 -> #ty >> ->
        (fun f x -> curryn (fun y -> f (x,y)))

 | << (#ty -> #ty') -> (#ty -> #ty') >> -> (fun f -> f)

 | << (#ty -> #ty') -> (#ty -> #ty'') >> ->
        (fun f x -> curryn (f x))
;;

which curryfies any function with some tuple in some parameter, e.g.
let add2 (x,y) = x+y;;
print (curryn add2 1 2: int);;

let add3 (x,(y,z)) = x+y+z;;
print (curryn add3 1 2 3: int);;

let add4 (x,(y,(z,t))) = x+y+z+t;;
print (curryn add4 1 2 3 4 : int);;

let addIP x (y,z) = x+y+z;;
print (curryn addIP 1 1 1 : int);;

let addPP (x,y) (z,t) = x+y+z+t;;
print (curryn addPP 1 1 1 1 : int);;

let addIIP x y (z,t) = x+y+z+t;;
print (curryn addIIP 1 1 1 1 : int);;

let addIPIP x (y,z) t (u,v) = x+y+z+t+u+v;;
print (curryn addIPIP 1 1 1 1 1 1 : int);;

In this type system, we still have static type-checking and inference,
but there are some practical problems: coherence (as always when you do
powerful overloading), true separate compilation, but more significantly,
you have to define all "instances" of an overloaded function in a single
"generic" definition. In most cases, this is not what the user wants.

  [1997-...]
  Jun Furuse is now tackling this problem.

A big problem with overloading is that it requires sophisticated type systems,
whereas the user expects a "do-what-I-mean" behavior from the type-checker.
As you've seen when objects were introduced in Caml, it's difficult to hide
a complex type system from the user, especially when there are type errors.

--f



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:14 MET