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 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id B9EE7BC0A for ; Thu, 18 Jan 2007 07:20:43 +0100 (CET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0I6KfLN010499 for ; Thu, 18 Jan 2007 07:20:42 +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 l0I6KPTc002047; Thu, 18 Jan 2007 15:20:26 +0900 (JST) Date: Thu, 18 Jan 2007 15:20:23 +0900 (JST) Message-Id: <20070118.152023.36917506.garrigue@math.nagoya-u.ac.jp> To: skaller@users.sourceforge.net Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic Variants From: Jacques Garrigue In-Reply-To: <1169093137.5327.33.camel@rosella.wigram> References: <20070118.102808.108741650.garrigue@math.nagoya-u.ac.jp> <1169093137.5327.33.camel@rosella.wigram> 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 concorde with ID 45AF11B9.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 semantics:01 overloading:01 semantics:01 overloading:01 haskell:01 inference:01 annotations:01 deduced:01 subtyping:01 ocaml:01 annotations:01 inference:01 variants:01 annotation:01 From: skaller > > 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. > > Can you explain this more? The kind of overloading I'm used > to is a matter of lookup not semantics, i.e. its just syntactic > sugar to save the human reader's memory. Because you're doing some partial evaluation :-) Namely you can view an overloaded function as a function taking extra hidden parameters: the types of its arguments. If these types are monomorphic, then you can immediately partially evaluate your function to choose the right implementation. But if they are polymorphic, you need to pass extra information around. This is what is done in Haskell for instance, passing dictionnaries for type classes. So an alternative view is that overloading is a type dependent translation from the source code to an explicit version. You can only drop the types after this translation. So this means that you cannot understand the source code locally: you need to be aware of the type information around it. > > 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. > > Felix makes this tradeoff. Types are deduced bottom up (s-attributes), > so variables and function return types are calculated, but function > parameters must be explicitly typed. This works if you don't add either subtyping or return-type overloading to the mix. Then you must also know the type of variables and the return type of functions. > Even in Ocaml it is necessary to write some annotations > in two cases: > > (a) hard to understand error messages from type inference > > (b) polymorphic variants This is not exactly the same thing, as these annotations have no impact on the semantics. Of course, one could say: if we have the annotation, why not use it for the semantics? But this is another story, with different implications. > On the other hand some code would just be impossible > without overloading. For example C has > > char, short, int, long, long long > unsigned versions > float, double, long double > > which is 13 distinct 'number' types, and I would hate > to have to write: > > 1 int_add 2 > 1L long_add 2L Actually this is not only overloading that is used here, but also automatic conversions. When writing numeric computations in ocaml, I find it just as painful to have to add float_of_int, as to add the dot after all operators. (In number of characters, float_of_int might be the biggest...) For overloading alone, the module system could help. If we had the operators defined with different types in each of the numeric type modules, then one could just choose the numeric type used with "open Mynumtype". This is one of the reasons I pushed for having a local "let open" construct... which can be simulated by "let module", at a slight cost. > So in some cases with inference and without overloading, > *you need the annotations anyhow*, they just go into the > function names in an unprincipled manner, instead of going > into the function parameter types in a principled -- > and indeed syntactically enforced -- manner. I believe this is the strongest argument for overloading: that it allows using types in a principled way. Of course, whether this is really principled depends on the code you write... Jacques Garrigue