This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] syntax of private constructors in CVS version
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Yaron M. Minsky Subject: Re: [Caml-list] syntax of private constructors in CVS version
```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"?
>
> 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

```