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.0 required=5.0 tests=AWL 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 24A4ABC0B for ; Thu, 18 Jan 2007 05:05:48 +0100 (CET) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l0I45jX1021726 for ; Thu, 18 Jan 2007 05:05:47 +0100 Received: from ppp27-234.lns1.syd6.internode.on.net (HELO rosella) ([59.167.27.234]) by ipmail01.adl2.internode.on.net with ESMTP; 18 Jan 2007 14:35:41 +1030 X-IronPort-AV: i="4.13,201,1167571800"; d="scan'208"; a="75434352:sNHT23878337" Subject: Re: [Caml-list] Polymorphic Variants From: skaller To: Jacques Garrigue Cc: tom.primozic@gmail.com, caml-list@yquem.inria.fr In-Reply-To: <20070118.102808.108741650.garrigue@math.nagoya-u.ac.jp> References: <20070117.111927.2004173151.garrigue@math.nagoya-u.ac.jp> <20070118.102808.108741650.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain Date: Thu, 18 Jan 2007 15:05:37 +1100 Message-Id: <1169093137.5327.33.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.6.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 45AEF219.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; variants:01 overloading:01 ocaml:01 overloading:01 semantics:01 semantics:01 inference:01 annotations:01 deduced:01 ocaml:01 annotations:01 inference:01 variants:01 coercions:01 overload:01 On Thu, 2007-01-18 at 10:28 +0900, Jacques Garrigue wrote: > From: Tom > > > * 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. 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. > 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. 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 On point (a) I admit I often *remove* the annotations after writing them (which I can't do in Felix). The need for (b) is limited and quite acceptable IMHO, it just takes a bit more experience than I have to pick when you need annotations or explicit coercions. 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 Similarly I have had a 'pretty printer' program which prints terms of an AST (the Felix grammar actually) and the fact I could overload fun str : t -> string meant I could usually forget what type it was I was converting to a string. (There are something like 50 AST node types involved I think). 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. Overall Felix library function declarations are considerably more verbose than Ocaml .. but the implementation is about the same complexity. BTW: of course in Ocaml you can add annotations for documentation purposes or to enforce a constraint. > By the way, this all looks likes the "used this feature in C++" > syndrome. Actually for Felix this is a legitimate reason :) > Sure C++ is incredibly powerful. But it is built on rather > shaky theoretical fundations. What? C++ has theoretical foundations? -- John Skaller Felix, successor to C++: http://felix.sf.net