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=none autolearn=disabled version=3.1.3 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 69A8EBC69 for ; Thu, 15 Nov 2007 21:28:57 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPs4PEc/0MSzhmdsb2JhbACPAwIBBwUGERY X-IronPort-AV: E=Sophos;i="4.21,421,1188770400"; d="scan'208";a="4540244" Received: from mho-02-bos.mailhop.org ([63.208.196.179]) by mail1-smtp-roc.national.inria.fr with ESMTP; 15 Nov 2007 21:28:52 +0100 Received: from gato.physics.und.nodak.edu ([134.129.186.227] helo=localhost) by mho-02-bos.mailhop.org with esmtpsa (TLSv1:AES256-SHA:256) (Exim 4.68) (envelope-from ) id 1IslKU-000Dh5-R9; Thu, 15 Nov 2007 20:28:51 +0000 X-Mail-Handler: MailHop Outbound by DynDNS X-Originating-IP: 134.129.186.227 X-Report-Abuse-To: abuse@dyndns.com (see http://www.mailhop.org/outbound/abuse.html for abuse reporting information) X-MHO-User: U2FsdGVkX1+Mk0QW+QqUnLd/xCIUo5u2 Date: Thu, 15 Nov 2007 14:28:49 -0600 From: Fernando Alegre To: Edgar Friendly Cc: Pierre Weis , caml-list , Alain Frisch Subject: Re: [Caml-list] Compiler feature - useful or not? Message-ID: <20071115202849.GB6523@gato.physics.und.nodak.edu> References: <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> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <473C81F5.6080808@gmail.com> User-Agent: Mutt/1.5.9i X-Spam: no; 0.00; compiler:01 integers:01 compiler:01 semantics:01 val:01 val:01 enforces:01 semantics:01 statically:01 run-time:01 run-time:01 orthogonal:01 summarize:01 beginner's:01 ocaml:01 The main problem I have with abstract types is that they are heavyweight since they need to be defined inside modules. In that particular, the proposed private types are also heavyweight. I would like to have private types be some kind of lightweight abstract types, as illustrated in the following example with two different injections and two different projections between integers and even numbers. Note that no modules are needed. The only way to get into or out of a private type would be by explicit coercion. Private types defined this way would be sound, as expressions like "half 10" would be forbidden by the compiler. The right expression would be "half (10 :> even)". A programmer may break the semantics of "even" by writing things such as "(11 :> even)", but he better know what he is doing. The current abstract types can be used to make a private type abstract too if that safety is needed. type even = private int let half (x:even) = (x :> int)/2 val half : even -> int let int_of_even (x:even) = (x :> int) val int_of_even : even -> int let dbl (x:int) = (2*x :> even) val dbl : int -> even let even_of_int (x:int) = if x mod 2 = 0 then (x :> even) else invalid_arg "even_of_int" val even_of_int : int -> even There is another less natural way to encode even numbers that enforces automatically the semantics: even number 2*n is encoded as integer n. Then, the example becomes: type even = private int let half (x:even) = (x :> int) let int_of_even (x:even) = 2*(x :> int) let dbl (x:int) = (x :> even) let even_of_int (x:int) = let e = x/2 in if 2*e = x then (e :> even) else invalid_arg "even_of_int" However, this kind of semantics-preserving encoding is just a matter of good luck, and I don't think it can be generalized to many cases, at least statically. You could always have a run-time check, but that misses the point. Although, I don't see a way to avoid the run-time check in the function even_of_int... In summary, in my opinion private types should be completely orthogonal to abstract types, so that both can be used either together or separately. Thanks, Fernando On Thu, Nov 15, 2007 at 11:29:25AM -0600, Edgar Friendly wrote: > Okay, let's see if I can summarize: > > Private types have use because you can expose your implementation while > still having control over construction of values. This is important for > implementing quotient structures. > > 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. > > E. > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs