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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 19705BC69 for ; Fri, 16 Nov 2007 10:23:59 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAAjwPEdQDPIblmdsb2JhbACPCgEBAQEHBAYiB4EP X-IronPort-AV: E=Sophos;i="4.21,425,1188770400"; d="scan'208";a="5882558" Received: from smtp20.orange.fr ([80.12.242.27]) by mail3-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 10:23:58 +0100 Received: from me-wanadoo.net (localhost [127.0.0.1]) by mwinf2011.orange.fr (SMTP Server) with ESMTP id 72AB71C0009D for ; Fri, 16 Nov 2007 10:23:58 +0100 (CET) Received: from [192.168.1.59] (APuteaux-154-1-12-161.w83-199.abo.wanadoo.fr [83.199.69.161]) by mwinf2011.orange.fr (SMTP Server) with ESMTP id 504EE1C0005C for ; Fri, 16 Nov 2007 10:23:58 +0100 (CET) X-ME-UUID: 20071116092358329.504EE1C0005C@mwinf2011.orange.fr Message-ID: <473D61A3.9090708@frisch.fr> Date: Fri, 16 Nov 2007 10:23:47 +0100 From: Alain Frisch User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: caml-list Subject: Re: [Caml-list] Compiler feature - useful or not? References: <473A363F.2080301@gmail.com> <891bd3390711131608g48b584a4n6b0ccab95d7de3f3@mail.gmail.com> <20071114075827.GA24058@yquem.inria.fr> <473AEC04.3030303@frisch.fr> <20071114143524.GA4423@yquem.inria.fr> <473B249D.9040703@frisch.fr> <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> <891bd3390711151630x238b8eddod5b7462d0fa1c735@mail.gmail.com> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; frisch:01 frisch:01 compiler:01 ocaml's:01 cvs:01 ocaml:01 integers:01 algebra:01 well-typed:01 ill-typed:01 type-based:01 subtyping:01 abbreviation:01 implements:01 wrote:01 Martin Jambon wrote: > You can write > match (x : Priv_int.t) with 0 -> true | _ -> false Actually, you cannot do that, at least with private types as implemented in OCaml's CVS. And this is to be expected given the lack of implicit subsumption in OCaml. If you were able to do such a thing, what type schema would you give to: let f = function 0 -> true | _ -> false ? This function should work on integers as well as on values of type Priv_int.t, but the type algebra cannot express that. My understanding (Pierre will correct me if I'm wrong) is that private type abbreviations, as they are currently implemented, can always be replaced by abstract types without turning a well-typed program into an ill-typed one. Doing so will prevent some type-based optimizations to happen, though. But the really interesting thing is that the new feature opens the door to extending the subtyping operator :> to take into account the natural (identity) injection from a private abbreviation to the underlying type. This is especially useful when the value of the private type appears deeply nested in a structure. With a normal function that implements the injection, you need to lift it to the whole structure which forces useless copies (and worse: the manual lifting may not be possible if some module declares a covariant type without a corresponding map function). For instance: (l : (Priv_int.t * Priv_int.t) list :> (int * int) list) instead of List.map (fun (x, y) -> (Priv_int.to_int x, Priv_int.to_int y)) l -- Alain