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 DE2ECBC0A for ; Wed, 28 Feb 2007 05:01:25 +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 l1S41Nox019726 for ; Wed, 28 Feb 2007 05:01:25 +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 l1S41G67002282; Wed, 28 Feb 2007 13:01:17 +0900 (JST) Date: Wed, 28 Feb 2007 13:01:15 +0900 (JST) Message-Id: <20070228.130115.35466734.garrigue@math.nagoya-u.ac.jp> To: daniel.buenzli@epfl.ch Cc: caml-list@inria.fr Subject: Re: [Caml-list] Fwd: "ocaml_beginners"::[] Trouble combining polymorphic classes and polymorphic methods From: Jacques Garrigue In-Reply-To: <8DF1B76F-AE3B-43F2-9034-7CF47277EE7B@epfl.ch> References: <20070228.103403.105433774.garrigue@math.nagoya-u.ac.jp> <1172627876.19033.85.camel@rosella.wigram> <8DF1B76F-AE3B-43F2-9034-7CF47277EE7B@epfl.ch> X-Mailer: Mew version 4.2 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Miltered: at concorde with ID 45E4FE93.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 bunzli:01 buenzli:01 explicitely:01 invariants:01 semantics:01 undecidable:01 structurally:01 semantics:01 variants:01 lablgl:01 runtime:01 fulfilled:98 polymorphic:01 polymorphic:01 From: Daniel B=FCnzli > Le 28 f=E9vr. 07 =E0 02:57, skaller a =E9crit : > = > > After all a nominal type is just a structural type with > > a unique tag representing its unique name. > = > What you miss here is the _process_ behind nominal types. > = > (paraphrasing Jacques) Types are not precise enough to define the = > semantic of a function, multiplication and addition have the same = > type but in many cases you cannot exchange one for the other. With = > that respect structural typing is a fallacy, it is not because types = = > match that you can replace a function by another. > = > With a nominal type the programmer signals explicitely its intent to = = > support a semantic. Notably you cannot use a function in a given = > context if it was not designed for that purpose which sounds = > fascistic but makes sense from a software development point of view. > = > Structural typing would make sense if it involved the weakest = > invariants a function. But for now, because of the poor information = > types give about semantics, structural typing is just bureaucratic = > compliance whereas nominal typing is a semantic contract --- whether = = > actually fulfilled or not is another (undecidable) question. Wow, here is a strong statement. Basically, you seem to be saying that types are useless for safety if they don't ensure full correctness, and that in the absence of safety they need to be nominal in order to declare any intent? I personally would contradict you on both counts. The first point is that type safety is already an important form of safety. Even if it is purely bureaucratic, at least it ensures that there is no contradiction _at the level of types_. If you are an ML programmer, you must know that this is useful. The second point is on the extra semantic advantage of using nominal types. I think there is some mixing up here. You can perfectly put a name on a value without using a nominal type. Using good function names, labelled arguments, etc... And writing (`Metre 3) gives you exactly the same information as (Metre 3). By naming things, even structurally, you can express informal contracts. The theoretical problem with structural types is more about very bad luck: you may be using two libraries, which seem to be using the same type (same constructor or method names), but actually have different semantics. And you might end up mixing data from the two libraries by error. The probability of this happening is so incredibly low that I often wonder why people see this as a real problem, but this reflects the lack of proper identity in structural types. This lack of identity may become a problem when you want to use identity for other things, like privacy. But it is not really relevant for normal public types, since you may easily deconstruct and reconstruct them. On the other hand, if you (rightly) decide to use abstract types in an API, whether they are internally nominal or structural is not relevant. If I may add a 3rd point, I believe that structural types sometimes allow you to give more precise specifications of functions, that would be hard to obtain with nominal types. See the use of polymorphic variants in lablGL for instance. This is certainly not a complete specification, all the less as the API is imperative. But this information can work as documentation, and removes an important category of runtime errors. Jacques Garrigue