Re: easy print and read (was: [Caml-list] Why are arithmetic functions not polymorph?)

[Pierre Weis <pierre.weis@inria.fr>]

Hi Oleg,

> On Monday 02 June 2003 11:25 pm, John Max Skaller wrote:
> > Another needed overload is 'print' (to print some
> > representation of a value which might be used in
> > a diagnostic).
> 
> I don't think simple overloading will solve the print/read issue to my 
> personal satisfaction. In G'Caml, one will still have to define these 
> functions by hand, right? As someone said, "I object to doing what computers 
> can do".

You're right: simple overloading cannot solve the print/read issue.

You're wrong: in G'Caml, one will not have to define these functions
by hand.

The reason is that, in G'Caml, the underlying theory is not
overloading (neither simple or complex overloading); it is a new
polymorphic typing discipline that supports the definition of a truely
polymorphic print primitive (while maintaining the safety of a
strongly typed discipline). This primitive will not be user's defined
but would have the same ``magic'' status as a lot of other basic
primitives in Pervasives, such as ( + ), open_in, print_string, or ( =
). The read primitive will have the same status.

Interestingly enough, the extensional polymorphism will allow user's
defined extensions of the print primitive to fit specific treatments
for the data types of interest in the program.

The Extensional polymorphism has been described in a 1995 POPL article
(see [1]). I connot resist to cite its abstract since it strangely
seems to be an anticipated answer to the issue you are pointing out
today:

       We present the extensional polymorphism framework, a new kind of
   polymorphism for functions defined inductively on types. As parametric
   polymorphic functions discriminate their argument via structural
   pattern matching on values, extensionally polymorphic functions
   discriminate their argument via structural pattern matching on types.

       Extensional polymorphism is fully compatible with parametric
   polymorphism, and provides a clean way to handle primitives such as
   equality and input and output functions. In particular, our type
   system supports a polymorphic printing procedure that prints any value
   in any context.

       We give a type reconstruction algorithm for extensional
   polymorphism and a translation scheme to a language with run-time
   types. The formalism allows the definition of generic functions as a
   set of clauses, each clause associating an expression to a possible
   type of the function. This leads to a powerful overloading scheme. We
   define a large class of generic functions for which strong typing is
   decidable: a static verification algorithm checks that every generic
   function is called on a type for which it is defined. In addition, we
   prove that this checking problem for unrestricted generic functions is
   undecidable.

Since 1995, we continued to work on this; in particular Jun Furuse
wrote his thesis on the Extensional Polymorphism. He also wrote the
G'Caml extension of Caml as a proof of concept for further integration
into the main stream compiler.

All this hard work needed a long time to mature (1995 -> 2003!) and is
now in a stable and satisfying state. So please, be kind enough to
read our papers and try the system, before stating definitive (and
maybe not so well argued) opinions such has ``overloading is
dangerous'' (or worse ``overloading is useless''), G'Caml cannot solve
polymorphic printing and reading, or even ``generic functions in
G'Caml are too weak and not extensible enough''. I'm sure you would be
astonished by the additive power G'Caml could bring into Caml;
consider also that all that new features is brought to you without
sacrificing the good old strongly typed discipline and static type
inference facility that we all love so much in Caml. I would like you
to be convinced it is worth supporting the experimental introduction of
these marvels into the language!

Best regards,
-- 
Pierre Weis

INRIA, Projet Cristal, http://pauillac.inria.fr/~weis

Bibliography and further readings:
==================================

In addition to a working implementation and integration into a Caml
compiler, the G'Caml system features a lot of enhancements and new
results about the extensional type system.

In particular, the print/read problem has been covered by a detailed
paper [4] (in french) that goes way further by introducing and
discussing value I/Os and their implementation within the extensional
framework. The definition and typechecking of generic functions is
covered by Jun's paper [3].

G'Caml and new results about the type system are described in long into Jun
Furuse's PHD thesis [2].

References:

[1] Extensional polymorphism (POPL 1995)
    ftp://ftp.inria.fr/INRIA/Projects/cristal/Francois.Rouaix/generics.dvi.Z
[2] Extensional polymorphism: Theory and Application
    http://pauillac.inria.fr/~furuse/thesis/
[3] Generic polymorphism in ML
    http://pauillac.inria.fr/~furuse/publications/jfla2001.ps.gz
[4] Entree/Sorties de valeurs en Caml (in french)
    http://pauillac.inria.fr/~furuse/publications/jfla2000.ps.gz

-------------------
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