From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id MAA29604; Fri, 6 Jun 2003 12:46:33 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id MAA29578 for ; Fri, 6 Jun 2003 12:46:32 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h56AkQH18727; Fri, 6 Jun 2003 12:46:27 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id MAA29569; Fri, 6 Jun 2003 12:46:26 +0200 (MET DST) Date: Fri, 6 Jun 2003 12:46:26 +0200 From: Pierre Weis To: Oleg Trott Cc: John Max Skaller , "caml-list@inria.fr" Subject: Re: easy print and read (was: [Caml-list] Why are arithmetic functions not polymorph?) Message-ID: <20030606124626.A27959@pauillac.inria.fr> References: <3EDC152C.5070906@ozemail.com.au> <200306060308.42724.oleg_trott@columbia.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0i In-Reply-To: <200306060308.42724.oleg_trott@columbia.edu>; from oleg_trott@columbia.edu on Fri, Jun 06, 2003 at 03:08:42AM -0400 X-Spam: no; 0.00; pierre:01 weis:01 caml-list:01 oleg:01 g'caml:01 pervasives:01 extensional:01 strangely:01 inductively:01 run-time:01 generic:01 decidable:01 undecidable:01 furuse:01 thesis:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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