From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE autolearn=disabled version=3.1.3 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id ABD67BC0B for ; Thu, 18 Jan 2007 02:28:17 +0100 (CET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0I1SFVt023885 for ; Thu, 18 Jan 2007 02:28:16 +0100 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.7/8.13.7) with ESMTP id l0I1SBQU018362; Thu, 18 Jan 2007 10:28:11 +0900 (JST) Date: Thu, 18 Jan 2007 10:28:08 +0900 (JST) Message-Id: <20070118.102808.108741650.garrigue@math.nagoya-u.ac.jp> To: tom.primozic@gmail.com Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic Variants From: Jacques Garrigue In-Reply-To: References: <20070117.111927.2004173151.garrigue@math.nagoya-u.ac.jp> X-Mailer: Mew version 4.2 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 45AECD2F.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 variants:01 labltk:01 overloading:01 ocaml:01 overloading:01 semantics:01 semantics:01 inference:01 compiler:01 haskell's:01 haskell:01 runtime:01 ocaml:01 subtyping:01 From: Tom > On 17/01/07, Jacques GARRIGUE wrote: > > From: Tom > > > So... why actually are polymorphic variants useful? Why can't they > > simply be > > > implemented as normal, concrete (or how would you call them? ...) > > variants? > > > > The original motivation was for the LablTk library, where some types > > (index for instance) have lots of small variations. At that point > > there where several options > > * overloading (but ocaml loathes overloading, you could say that the > > total absence of overloading is essential to the language) > > Is there a reason for that? Is it only hard to implement or are there any > conceptual / strategical / theoretical reasons? There are two kinds of theoretical reasons. The most theoretical one is about semantics: with generic overloading, all your semantics must take types into account. This is a problem as most theoretical studies of lambda-calculus are based on so-called erasure semantics, where types are discarded at execution. So this means you must design your own, more complex semantics. Not that this reason may not apply to constructor or record overloading, if you do not allow the semantics to change according to the type. The other one is about type inference. Basically, overloading has a huge impact on overloading. The direct way to handle it, using types alone, is deeply disruptive, as it means that some programs will be refused for lack of type information. It is very hard to define a clear criterion on which programs should be refused, notwithstanding internal details of the compiler. This also applies to record and constructor overaloading. There are other approach the problem, with constrained type variables (either Haskell's type classes or G'Caml's generic type variables,) but of course they add complexity to the type system. And it is not clear that they solve the problem for constructor and record overloading: in Haskell, records fields are not overloaded, and constructor overloading has to be done by hand for each type, through an explicit encoding into type classes. Both reasons have practical impact. For the first one, using erasure semantics means that the programmer also can discard types when understanding the runtime behaviour of a program. For the second one, you can write code that is maximally polymorphic, without too much fear about the impact of performance (equality is overloaded, so it still matters...) or strange ambiguity-related error messages. So for the time being ocaml keeps to no overloading at all. > > OCaml does not, as far as I know, have any structural typing for > > records.. Not for records, but for objects. From a type-theoretic point of view they are just equivalent. > Hm... Actually, what I had in mind is nominal subtyping... similar to > objects, in fact, objects in C++-like languages, just that they have no > class methods. Reading the description below, this all looks nice, independently of the semantics limitation described above. However, you can kiss farewell to type inference. With such an extensive overloading, you would need type annotations all over the place. By the way, this all looks likes the "used this feature in C++" syndrome. Sure C++ is incredibly powerful. But it is built on rather shaky theoretical fundations. So you can't expect to bring everything from C++ to a new language. Why not think about new ways to solve problems :-) (To be completely honest, this also looks a bit like ML2000, and the Moby language, which has a sound theoretical fundation, but never really took off. You might want to go see for yourself.) Jacques Garrigue > Now... close your eyes (but try to continue reading this ;) ) and imagine > you're in a dreamworld. You are programming in a language that has > * function overloading that allows you to have > length "abcd" + length [1; 2; 3] > * Constructor overloading, eliminating the need of > type parse_expression = > Pexp_name of string > | Pexp_constant of constant > | Pexp_let of (pattern * parse_expression) * parse_expression > | Pexp_apply of parse_expression * parse_expression list > | Pexp_try of parse_expression * (pattern * parse_expression) list > > type typed_expression = > Texp_ident of ident > | Texp_constant of constant > | Texp_let of (pattern * typed_expression) * typed_expression > | Texp_apply of typed_expression * typed_expression list > | Texp_try of typed_expression * (pattern * typed_expression) list > as it can be coded as > type parse_expression = > Name of string > | Constant of constant > | ... > > type typed_expression = > Ident of ident > | Constant of constant > | ... > > * nominal subtyping of records, with overloaded field names: > type widget = {x : float; y : float; width: float; height: float} (* > top-level type *) > type button = {widget | text : string } > type checkbox = {button | checked : bool} > type image = {widget | url : string} > > type vector = {x : float; y : float} > type document {url : url} > > so subtypes could be applied to a function > fun move : widget -> (float * float) -> unit > > let chk = {x = 0.0; y = 0.0; width = 10.0; height = 12.0; text = > "Check me!"; checked = false} > move chk (3.0, 3.0) > and types could be "discovered" at runtime: > let draw widget = > typematch widget with > w : widget -> draw_box (w.x, w.y, w.height, w.width) > | b : button -> draw_box (b.x, b.y, b.height, b.width); draw_text > b.text > | i : image -> draw_image i.url (i.x, i.y) > | ... > > Do you think you would be "satisfied" even without polymorphic variants? > > I am not saying this just for fun... I want to create a language with > overloading, but I kinda don't really like polymorphic variants... thou if > they turn out to be really useful, I would probably start to like them. > > Any comments? > > - Tom