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.6 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, MAILTO_TO_SPAM_ADDR autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 38324BC69 for ; Thu, 15 Nov 2007 23:32:38 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAHJXPEfUGyojimdsb2JhbACBXY0nAgEIAggREQc X-IronPort-AV: E=Sophos;i="4.21,422,1188770400"; d="scan'208";a="19359429" Received: from smtp5-g19.free.fr ([212.27.42.35]) by mail4-smtp-sop.national.inria.fr with ESMTP; 15 Nov 2007 23:32:38 +0100 Received: from smtp5-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp5-g19.free.fr (Postfix) with ESMTP id BD2F63F6163; Thu, 15 Nov 2007 23:32:37 +0100 (CET) Received: from Llea.celt.neu (ron34-3-82-236-236-194.fbx.proxad.net [82.236.236.194]) by smtp5-g19.free.fr (Postfix) with ESMTP id 8B60F3F615F; Thu, 15 Nov 2007 23:32:37 +0100 (CET) Received: from Llea.celt.neu (localhost [127.0.0.1]) by Llea.celt.neu (8.14.1/8.13.8) with ESMTP id lAFMblH6001615; Thu, 15 Nov 2007 23:37:48 +0100 (CET) (envelope-from michael.le_barbier@laposte.net) Received: (from michael@localhost) by Llea.celt.neu (8.14.1/8.13.8/Submit) id lAFMblTl001614; Thu, 15 Nov 2007 23:37:47 +0100 (CET) (envelope-from michael.le_barbier@laposte.net) X-Authentication-Warning: Llea.celt.neu: michael set sender to michael.le_barbier@laposte.net using -f To: Edgar Friendly Cc: Pierre Weis , caml-list , Alain Frisch 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> <473C81F5.6080808@gmail.com> From: michael.le_barbier@laposte.net (=?iso-8859-15?Q?Micha=EBl?= Le Barbier) Date: Thu, 15 Nov 2007 23:37:47 +0100 In-Reply-To: <473C81F5.6080808@gmail.com> (Edgar Friendly's message of "Thu\, 15 Nov 2007 11\:29\:25 -0600") Message-ID: <86sl37879g.fsf@Llea.celt.neu> User-Agent: Gnus/5.11 (Gnus v5.11) Emacs/22.1 (berkeley-unix) MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; compiler:01 val:01 invariants:01 ill-formed:01 cheers:01 edgar:98 abstract:01 abstract:01 rec:01 caml-list:01 int:01 int:01 writes:01 data:02 represented:02 Edgar Friendly writes: > After reading everything about quotient types and the need for private > types, I have to ask "why not just completely abstract the type"? What > you seem to want from private types, you seem to gain pretty easily > through abstract types. I think you have overlooked the following example in Pierre's article: - Projection is automatic # let rec int_of_peano =3D function | Zero -> 0 | Succ n -> 1 + int_of_peano n | Plus (n, p) -> int_of_peano n + int_of_peano p ;; val int_of_peano : M.peano -> int =3D # int_of_peano three;; - : int =3D 3 Since we have access to the representation of the value we can filter values (just like in the example) and since we are unable to create ill-shaped values, we can assume that good invariants are true in the values we are examining. If we want to do the same with abstract data types, we would have two types involved instead of one: * the abstract type peano already described; * a second type `good_representation' and an explicit application `projection: peano -> good_representation' Let's say that sets manipulated through the `Set' module are represented by balanced trees. If the type set had been private instead of abstract, we could investigate the representation of a value of the type but could not produce an ill-formed value (an `unbalenced tree'). (I also may be totally wrong :) ) --=20 Cheers, Micha=EBl