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

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

Would it be fair to say that the main distinction between private types
and abstract types is that with private types, constructors are only
invocable from inside the module, but destructors (e.g., pattern
matching) are available both inside and outside of the module?

y

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