[Camllist] syntax of private constructors in CVS version
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Yaron M. Minsky <yminsky@c...> 
Subject:  Re: [Camllist] syntax of private constructors in CVS version 
A couple of thoughts: * First, this seem On Mon, 20030630 at 14:39, Pierre Weis wrote: > Hi Brian & all, > > [Sketching the semantics of private types, this message is long.] > > > Private only works with new record types and sum types that you declared. > > Think about it. What would it mean to declare some set of polymorphic variant > > tags as "private"? > > You're absolutely right on your comments and explanation. However, I > think we also need to explain the ideas beneath private types and > their intended uses. > > As you should already know, usual sum and product types in Caml > correspond to the mathematical notion of free algebraic data > structures. This is fairly useful and allows the modelization of a lot > of common data structures in practical programming > situations. However, besides the free algebra structures, > mathematicians use a lot of nonfree algebras (socalled structures > defined via generators and relations). Private types aim at giving a > way to modelize those nonfree structures. Equivalenetly, you can > think of private types as providing a way to implement types equipped > with invariants, quotient structures (i.e. sets of equivalence classes > for some equivalence relation on a free algebra), or data types with > canonical normal forms. > > As an example, consider a simple modelization of natural integers in > unary notation: > > type nat = >  Zero >  Succ of nat;; > > The nat type is a regular sum type; a value of the nat type is either > the constant constructor Zero (modelizing the integer 0) or > constructed with any application of the constructor Succ to a nat > value (Succ n modelizing the successor of n or n + 1). Hence, the nat > type is adequate in the sense that it exactly modelizes the unary > representation of positive integers. Nothing new here, and we can > easily write a test to 0 as: > > let is_zero = function >  Zero > true >  _ > false;; > > Now, let's go one step further and imagine we modelize integers > (either positive or negative). Even if a complex (adequate) > modelization of those numbers using a regular Caml data type is not > very complex, let's take, for the sake of explanation, a simple > approach by generalizing the nat type; we simply add an extra Pred > constructor to modelize negative integers: Pred n is the predecessor > of n or n  1: > > type integer = >  Zero >  Succ of integer >  Pred of integer;; > > Now, we can modelize all integers in unary notation but the integer > type is no more adequate, in the sense that we have a problem of > unicity of representation: a given number can be modelized by > (infinitely) many distinct values of the integer data type. For > instance, the terms Succ (Pred Zero) and Zero all represent the number > 0. You may think that this is not a big problem but in fact it is very > ennoying, because when writing a function over values of type integer, > you must now pattern match a lot of patterns instead of the only one > that canonically represents a given integer. For instance > > let is_zero = function >  Zero > true >  _ > false;; > > is no more the expected predicate. We must write something much more > complex, for instance > > let rec is_zero = function >  Zero > true >  Succ (Pred n) > is_zero n >  Pred (Succ n) > is_zero n >  n > false;; > > (BTW: is this code now correct ?) > > A private type will solve this problem. We define a module Integer > whose interface defines the integer type as a private type equipped > with functions that construct values in the different summands of the > type: > > type integer = private >  Zero >  Succ of integer >  Pred of integer;; > > value zero : unit > integer > value succ : integer > integer > value pred : integer > integer > > In the implementation of the module, we keep the definition of the > type as regular (say ``public'', if you want) and implement the > constructing functions such that they ensure the unicity of > representation of integers: > > let zero () = Zero;; > > let succ = function >  Pred n > n >  n > Succ n;; > > let pred = function >  Succ n > n >  n > Succ n;; > > It is now easy to prove that all the integers built with applications > of functions pred and succ have a unique representation (or > equivalently that no tree of type integer obtained by composing those > functions can have an occurrence of the redexes (Pred (Succ ...)) or > (Succ (Pred ...))). > > Now, since all the clients of the Integer module cannot construct > values of type integer by directly applying the constructors and must > use the constructing functions instead, we know for sure that the > unicity property holds. Hence, the naive (and natural) version of > is_zero is correct again. > > In conclusion: private types serve to modelize types with arbitrary > algebraic invariants (no miracle here: you must program those > invariants in the definition of the constructing functions). > > In contrast with abstract data types, the private types still maintain > the elegant pattern matching facility of ML outside the module that > defines the type. > > Hope this helps. > > Pierre Weis > > INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis/ > > >  > To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr > Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners  / Yaron M. Minsky \ \ http://www.cs.cornell.edu/home/yminsky/ / Open PGP  KeyID B1FFD916 (new key as of Dec 4th) Fingerprint: 5BF6 83E1 0CE3 1043 95D8 F8D5 9F12 B3A9 B1FF D916  To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners