Re: [Caml-list] syntax of private constructors in CVS version

["Yaron M. Minsky" <yminsky@cs.cornell.edu>]

A couple of thoughts:

      * First, this seem

On Mon, 2003-06-30 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 non-free algebras (so-called structures
> defined via generators and relations). Private types aim at giving a
> way to modelize those non-free 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 caml-list-request@inria.fr Archives: http://caml.inria.fr
> Bug reports: http://caml.inria.fr/bin/caml-bugs 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 caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners