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

[Pierre Weis <pierre.weis@inria.fr>]

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