From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: ** X-Spam-Status: No, score=2.3 required=5.0 tests=AWL,HTML_10_20,HTML_MESSAGE, ML_MARKETING,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 353A0BC6C for ; Fri, 16 Nov 2007 01:30:25 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CAFtzPEdIDsq1dGdsb2JhbACCd4wOCgUFEhaBEQ X-IronPort-AV: E=Sophos;i="4.21,422,1188770400"; d="scan'208";a="19363186" Received: from ro-out-1112.google.com ([72.14.202.181]) by mail4-smtp-sop.national.inria.fr with ESMTP; 16 Nov 2007 01:30:23 +0100 Received: by ro-out-1112.google.com with SMTP id m6so880274roe for ; Thu, 15 Nov 2007 16:30:21 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:references:x-google-sender-auth; bh=eY2GYwiTzz1fQWpfhkx+QYIh25V4uTCS0EKZSrMi5KY=; b=qoOoRS2k7IXfGeFV2Mb2/o1b5yBhoM4sTWfWKOXDrnd6oRDCXpUT7QqDZxi3BjUQi83XeuApdlLxcsBbkU435DFMvy2Quork+MB4MbHhP8z/1moAMq2A2ktVHR6+iux2PBrahS9BrGs/0nLnRJiLyp8CbRkQF0c6C8u+HaMP0LQ= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:references:x-google-sender-auth; b=Dkn4AZEmSRMUVBaLPSFy3LW/ExlfuMvtQwVNZayRoET/rWnPsZrlv+oh7zFkHMQhxP7+Yca2+AZLLNxwjbIodK01fnSWIeIbcHe3vY5cNO3rvOY7QclPqSqeZGJh7alddPluMPsIufzu0R6OAR/s94a4tcim6i41FJT7RawY14Q= Received: by 10.142.165.9 with SMTP id n9mr479351wfe.1195173018332; Thu, 15 Nov 2007 16:30:18 -0800 (PST) Received: by 10.142.200.14 with HTTP; Thu, 15 Nov 2007 16:30:18 -0800 (PST) Message-ID: <891bd3390711151630x238b8eddod5b7462d0fa1c735@mail.gmail.com> Date: Thu, 15 Nov 2007 19:30:18 -0500 From: "Yaron Minsky" Sender: yminsky@gmail.com To: "Pierre Weis" Subject: Re: [Caml-list] Compiler feature - useful or not? Cc: "Alain Frisch" , caml-list In-Reply-To: <20071115132649.GB15754@yquem.inria.fr> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_6215_2261711.1195173018344" References: <473A363F.2080301@gmail.com> <891bd3390711131608g48b584a4n6b0ccab95d7de3f3@mail.gmail.com> <20071114075827.GA24058@yquem.inria.fr> <473AEC04.3030303@frisch.fr> <20071114143524.GA4423@yquem.inria.fr> <473B249D.9040703@frisch.fr> <20071114184352.GB28796@yquem.inria.fr> <473BE750.9060301@frisch.fr> <20071115132649.GB15754@yquem.inria.fr> X-Google-Sender-Auth: 9de38b6241ddc59e X-Spam: no; 0.00; yaron:01 minsky:01 yminsky:01 compiler:01 trivial:01 struct:01 sig:01 val:01 val:01 sig:01 weis:01 weis:01 well-typed:01 ill-typed:01 subtypes:01 ------=_Part_6215_2261711.1195173018344 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline Most of what you said about quotient types made sense to me, but I must admit to being deeply confused about the nature of the change to the language. Consider the following trivial module and two possible interfaces. module Int =3D struct type t =3D int let of_int x =3D x let to_int x =3D x end module type Abs_int =3D sig type t val of_int : int -> t val to_int : t -> int end module type Priv_int =3D sig type t =3D private int val of_int : int -> t val to_int : t -> int end So, what is the difference between (Int : Abs_int) and (Int : Priv_int)? For instance, can I write (Priv_int.of_int 3) + (Priv_int.of_int 5)? Can you point to anything concrete I can do with the private version that I can't do with the abstract version? Is there any expression that is legal for one but not for the other? y On Nov 15, 2007 8:26 AM, Pierre Weis wrote: > > >- a value of type row is in fact a concrete integer (it is not hidden > in > > >any way), > > > > But you cannot apply integer operations to it, so it is not a normal > > concrete integer, right? > > Right: a value of type row has type row ... not type int! > > > Can you show an example where replacing all "type t =3D private ..." > > definitions by "type t" changes a well-typed program into an ill-typed > > one? I understand that if private types create real subtypes (w.r.t. > > :>) then they are different than abstract types, but otherwise, I don't > > see the difference for the type-checker. > > May be, I must recall what are private types in the first place: private > types has been designed to implement quotient data structure. > > (*** Warning. > > Wao: after re-reading this message I realize that it is really long. > > You can skip it, if you already know something about mathematical quotien= t > structures, private types for record and variant, relational types and th= e > mocac compiler! > > ***) > > What is a quotient ? > -------------------- > > Here quotient has to be understood in the mathematical sense of the term= : > given a set S and an equivalence relation R, you consider the set S/R of > the > equivalence classes modulo the relation R. S/R is named the quotient > structure of S by R. Quotient structures are fundamental in mathematics > and > there properties have been largely studied, in particular to find the > relationship between operations defined on S and operations on S/R: which > operations on S can be extended to operations on S/R ? Which properties o= f > operations on S are still valid for there extension on S/R ? and so on. > > Simple examples of quotient structures can be found everywhere in maths, > for > instance consider the equivalence relation R on pairs of integer values > defined as > > z_1 equiv z_2 if and only if z_1 and z_2 are both odd or are both even > (in Caml terms > z_1 equiv z_2 if and only if (z_1 mod 2) =3D (z_2 mod 2)) > > The set Z/R is named Z/2Z and it inherits properties of operations on Z: > it > is an abelian group (and more). > > A wonderful example of such inheritance of interesting properties by > inheritance of operations thanks to a definition by a quotient structure > is > the hierarchy of sets of numbers: starting with N (the set of natural > numbers) we define Z (the set of relative integer numbers) as a quotient > of > NxN), then Q (the rational numbers) as a quotient of ZxZ*, R (the set of > real > numbers) as a quotient of Q^N (the sets of sequences of rational numbers)= , > C > (the set of complex numbers) as a quotient of R[X] (the set of polynomial= s > with one unknown and real coefficients). Note here that at each step of > the > hierarchy the quotient structure is richer (has more properties and/or > more > elements) than the original structure: first we have a monoide, then a > group > and a ring, then a field, then a complete field and so on. > > Why quotient structures ? > ------------------------- > > So quotient structures are a fundamental tool to express mathematical > structures and properties. Exactly as mathematical functions, relations > and > sets. As you may have noticed, programming languages are extremely relate= d > to > maths (due to their purely logical bases) even if, in some cases, the > zealots > of the language at hand try to hide the mathematical fundation into a > strange > anthropomorphic discurse to describe their favorite language features. > > In the end, the computer programing languages try hard to incorporate > powerful features from mathematics, because these features have been > polished > by mathematicians for centuries. As a consequence of this work, we know > facts, properties and theorems about the mathematical features and this i= s > an > extremely valuable benefit. > > Now, what is the next frontier ? What can we steal more to mathematics fo= r > the > benefit of our favorite programming language ? > > If we review the most powerful tools of mathematicians, we found that > functions have been borrowed (hello functional programming, > lambda-calculus > and friends :)), relations have been borrowed (data bases, hash tables, > association lists), sets have been more or less borrowed (hello setle, > pascal, and set definition facilities from various libraries of various > languages...). More or less, we have all those basic features. > > >From the mathematical set construction tools, we have got in Caml: > > - the cartesian product of sets (the * binary type constructor, the recor= d > type definitions), > - the disjunct union of sets (the | of polymorphic variants, the sum (or > variant) type definitions). > > Unfortunately, we have no powerful way to define a quotient data > structure. That what private type definitions have been designed to do. > > What do we need for a quotient data structure ? > ----------------------------------------------- > > In the first place, we need the ``true'' thing, the real feature that is > indeed used in maths. Roughly speaking this means to assimilate the > quotient > set S/R to a subset of S. > > In the previous definition of quotient structures, there is a careful > distinction between the base set S and the quotient set S/R. In fact, > there > always exists a canonical injection from S to S/R, and if we choose a > canonical representant in each equivalence class of S/R, we get another > canonical injection from S/R to S, so that S/R can be considered as a > subset > of S (the story is a bit more complex but that's the idea). This > injection/projection trickery is intensively used in maths; for instance, > in > the hierarchy of number sets, we say and consider that N is a subset of Z > that itself is a subset of Q, a subset of R, a subset of C. Rigourously, > we > should say for instance, there is a subset of Z that is canonically > isomorphic to N; in fact, we abusively assimilate N to this subset of Z; > hence, we say that N is ``included'' in Z, when we should say ``the image > of > N by the canonical isomorphism from N to Z'' is included in Z; then, we g= o > one step further in the assimilation of N to a subset of Z, by denoting > the > same, the elements of N and there image in Z; for instance, ``the neutral > element of the multiplication in Z'' and the successor of 0 in N is > denoted > ``1''; and we now can say that 1 belongs to Z. Note here that, in the > first > place, ``the neutral element of the multiplication in Z'' is an > equivalence > class (as all elements in Z are). So it is a set. More exactly, the > ``neutral > element of the multiplication in Z'' is the infinite set of pairs of > natural > numbers (n, m) such that n - m =3D 1 (here ``-'' is an operation in N and > ``1'' > is the successor of the natural number ``0'', so that n - m =3D 1 is a > shorthand for n =3D succ m). The assimilation between N and its isomorphi= c > image allows to use 1 as the denotation of this infinite set of pairs of > natural numbers. > > We understand why the mathematicians always write after having designed a > quotient structure: ``thanks to this isomorphism, and if no confusion may > arise, we always assimilate S to its canonical injection in S/R''. > > This assimilation is what private type definitions allow. > > How do we define a quotient data structure ? > -------------------------------------------- > > The mathematical problem: > - we have a set S and an equivalence relation R on SxS, > - we construct the quotient S/R. > - we state afterwards: > ``if no confusion may arise, we always assimilate S to its canonical > injection in S/R''. > > The programming problem: > - we have a data structure S (defined by a type s) and a relation R on Sx= S > (defined by a function r from s * s to bool). > - we construct a data structure that represents S/R. > - we have afterwards: > ``No confusion may arise, we always assimilate S to its canonical > injection > in S/R''. > > The private data type solution: > - the data structure S is defined as any Caml data structure and the > relation R is implemented by the canonical injection(s) from S to S/R. > - the canonical projection from S/R to S is automatic. > - S (defined by s) is assimilated to S/R (which is then also s!). > > We defined S/R as a subset of S, the set of canonical representants of > equivalence classes of S/R. > > More exactly, the canonical injection from S to S/R maps each element of = S > to > its equivalent class in S/R; if we assimilate each equivalence class to > its > canonical representant (an element of S), the canonical injection maps > each > element of S to the canonical representant of its equivalence class. Henc= e > the canonical injection has type S -> S. > > An example treated without private types: > ----------------------------------------- > > Let's take a simple example: > > S is the following data structure that implements a mathematical (free) > structure > generated by the constant 0, the unary symbol succ, and the binary symbol > +. > > type peano =3D > | Zero > | Succ of peano > | Plus of peano * peano > > R is the (equivalence) relation that expresses that > - 0 is the neutral element for + (for all x in S, 0 + x =3D x and x + 0 = =3D > x), > - + is associative (for all x, y, z in S=B3, (x + (y + z)) =3D ((x + y) += z)). > > The canonical injection is a function from peano -> peano that maps each > value > in S (the type peano) to the canonical representant of its class in S/R > (an > element of S (the type peano)): > > let rec make =3D function > | Zero -> Zero > | Plus (Succ n, p) -> Succ (make (Plus (n, p))) > | Plus (Zero, p) -> p > | Plus (p, Zero) -> p > | Plus (Plus (x, y), z) -> make (Plus (x, make (Plus (y, z)))) > | Succ p -> Succ p > ;; > > (This function may be wrong but you see the idea :)) > > So, if you want to represent S/R for peano in Caml you must: > - (1) define the type peano > - (2) always use the make function to create a value in S/R > - (3) not to confuse S and S/R in your head (I mean in your programs) > > Private data types permits (1), ensures (2), and helps for (3) concerning > the > head part and ensures (3) for programs by means of compile-time type > errors. > > The same example with private types: > ------------------------------------ > > To define a private data type you must define a module. > - in the implementation, you define the carrier S and its canonical > injection. > - in the interface, you export the carrier and the injection. > > The type checker will ensure transparent projection from the quotient to > the > carrier and mandatory use of the canonical projection to build a value in > S/R. > > interface peano.mli > ------------------- > type peano =3D private > | Zero > | Succ of peano > | Plus of peano * peano > ;; > > val zero : peano;; > val succ : peano -> peano;; > val plus : peano * peano -> peano;; > > implementation peano.ml > ----------------------- > type peano =3D > | Zero > | Succ of peano > | Plus of peano * peano > ;; > > let rec make =3D function > ... > ;; > > let zero =3D make Zero;; > let succ p =3D make (Succ p);; > let plus (n, m) =3D make (Plus (n, m));; > > (See note (1) for a discussion on the design of this example.) > > What is given by private types: > ------------------------------- > > - You cannot create a value of S/R if you do not use the canonical > injection > # Zero;; > Cannot create values of the private type peano > > - As a consequence, values in S (i.e. S/R) are always canonical: > # let one =3D succ zero;; > val one : M.peano =3D Succ Zero > # let three =3D plus (one, succ (plus (one, zero)));; > val three : M.peano =3D Succ (Succ (Succ Zero)) > > - Projection is automatic > # let rec int_of_peano =3D function > | Zero -> 0 > | Succ n -> 1 + int_of_peano n > | Plus (n, p) -> int_of_peano n + int_of_peano p > ;; > val int_of_peano : M.peano -> int =3D > # int_of_peano three;; > - : int =3D 3 > > What about private abbreviations ? > ---------------------------------- > > Private abbreviation definitions are a natural extension of private data > type > definitions to abbreviation type definitions. The same notions are carrie= d > out mutatis-mutandis: > > - we have a data structure S (defined by a type s) and a relation R on Sx= S > (defined by a function r from s * s to bool). > - we construct a data structure that represents S/R. > - we have afterwards: > ``No confusion may arise, we always assimilate S to its canonical > injection > in S/R''. > > In the case of abbreviations: > > - the data structure S/R is defined by a type s (which is an abbreviation= ) > and > a relation defined by a function, > - the canonical injection should be defined in the implementation file of > the > private data type module, > - we always assimilate S to its canonical injection in S/R. > > In pratice, as for usual private types (for which the constructive part o= f > the data type is not available outside the implementation), the type > abbreviation > is not known outside the implementation (it is really private to its > implementation). This prevents the construction of values of S/R without > using the canonical injection. > > Th noticeable difference is the projection function: it cannot be fully > implicit (otherwise, as you said Alain, the assimilation will turn to > complete > confusion: we would have S identical to S/R, hence row=3Dint and no > difference > between a regular abbreviation definition and a private abbreviation > definition). If not implicit, the injection function should granted to be > the > identity function (something that we would get for free, if we allow > projection via sub-typing coercion). > > In short: abstract data types provide values that cannot be inspected nor > safely manipulated without using the functions provided by the module tha= t > defines the abstract data type. In contrast, private data types are > explicitely concrete and you can freely write any algorithm you need. A > good > test is printing: you can always write a function to print values of a > private type, it is up to the implementor of an abstract type to give you > the > necessary primitives to access the components of the abstracted values. > > Automatic generation of the canonical injection: > ------------------------------------------------ > > You may have realized that writing the canonical injection can be a real > challenge. > > The moca compiler (see http://moca.inria.fr/) helps you to write the > canonical injection by generating one for you, provided you can express > the > injection at hand via a set of predefined algebraic relations (and/or > rewrite > rules you specify) attached to the constructors of the private type. > Private > types with constructors having algebraic relations are named relational > types. Moca generated canonical injections for relation types. > > For instance, you would write the peano example as the following peano.ml= m > file: > > type peano =3D private > | Zero > | Succ of peano > | Plus of peano * peano > begin > associative > neutral (Zero) > rule Plus (Succ n, p) -> Succ (Plus (n, p)) > end;; > > The mocac compiler will generate the interface and implementation of the > peano module for you, including the necessary canonical injection > function. > > Best regards, > > -- > Pierre Weis > > INRIA Rocquencourt, http://bat8.inria.fr/~weis/ > > Note (1): > - we can't just export the canonical injection since you could not build > any > value of the type without previously defined values! > - we provide specialized versions of the canonical injection function > introducing the convention that the lowercase name of a value constructo= r > is > the name of its associated canonical injection. > - we do not export the plasin true canonical injection since it would be > more > confusing than useful. > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > ------=_Part_6215_2261711.1195173018344 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline Most of what you said about quotient types made sense to me, but I must adm= it to being deeply confused about the nature of the change to the language.=   Consider the following trivial module and two possible interfaces. <= br>
module Int =3D struct
   type t =3D int
   le= t of_int x =3D x
   let to_int x =3D x
end

module t= ype Abs_int =3D sig
   type t
  val of_int : int ->= t
  val to_int : t -> int
end

module type Priv_int = =3D sig
   type t =3D private int
   val of_int : int -&= gt; t
   val to_int : t -> int
end

So, what is th= e difference between (Int : Abs_int) and (Int : Priv_int)?  For instan= ce, can I write (Priv_int.of_int 3) + (Priv_int.of_int 5)?  Can you po= int to anything concrete I can do with the private version that I can't= do with the abstract version?  Is there any expression that is legal = for one but not for the other?

y

On Nov 15, 2007 8:26 AM, Pierre= Weis <pierre.weis@inria.fr&= gt; wrote:
> >- a value of type row is in fact a concrete = integer (it is not hidden in
> >any way),
>
> But you = cannot apply integer operations to it, so it is not a normal
> concre= te integer, right?

Right: a value of type row has type row ... not type int!
=

> Can you show an example where replacing all = "type t =3D private ..."
> definitions by "type t"= ; changes a well-typed program into an ill-typed
> one?   I understand that if private types create real subtype= s (w.r.t.
> :>) then they are different than abstract types, but o= therwise, I don't
> see the difference for the type-checker.
<= br>
May be, I must recall what are private types in the first place: priv= ate
types has been designed to implement quotient data structure.
(***  Warning.

Wao: after re-reading this message I realize th= at it is really long.

You can skip it, if you already know something about mathematical q= uotient
structures, private types for record and variant, relational typ= es and the
mocac compiler!

***)

What is a quotient ?
--------------------

 Here quotient has to be understood in the= mathematical sense of the term:
given a set S and an equivalence relati= on R, you consider the set S/R of the
equivalence classes modulo the rel= ation R. S/R is named the quotient
structure of S by R. Quotient structures are fundamental in mathematics= and
there properties have been largely studied, in particular to find t= he
relationship between operations defined on S and operations on S/R: w= hich
operations on S can be extended to operations on S/R ? Which properties= of
operations on S are still valid for there extension on S/R ? and so = on.

Simple examples of quotient structures can be found everywhere i= n maths, for
instance consider the equivalence relation R on pairs of integer values=
defined as

 z_1 equiv z_2 if and only if z_1 and z_2 are bo= th odd or are both even
(in Caml terms
 z_1 equiv z_2 if and onl= y if (z_1 mod 2) =3D (z_2 mod 2))

The set Z/R is named Z/2Z and it inherits properties of operations = on Z: it
is an abelian group (and more).

A wonderful example of s= uch inheritance of interesting properties by
inheritance of operations t= hanks to a definition by a quotient structure is
the hierarchy of sets of numbers: starting with N (the set of naturalnumbers) we define Z (the set of relative integer numbers) as a quotient = of
NxN), then Q (the rational numbers) as a quotient of ZxZ*, R (the set= of real
numbers) as a quotient of Q^N (the sets of sequences of rational number= s), C
(the set of complex numbers) as a quotient of R[X] (the set of pol= ynomials
with one unknown and real coefficients). Note here that at each= step of the
hierarchy the quotient structure is richer (has more properties and/or = more
elements) than the original structure: first we have a monoide, the= n a group
and a ring, then a field, then a complete field and so on.

Why quotient structures ?
-------------------------

So qu= otient structures are a fundamental tool to express mathematical
structu= res and properties. Exactly as mathematical functions, relations and
sets. As you may have noticed, programming languages are extremely related = to
maths (due to their purely logical bases) even if, in some cases, the= zealots
of the language at hand try to hide the mathematical fundation = into a strange
anthropomorphic discurse to describe their favorite language features.<= br>
In the end, the computer programing languages try hard to incorporat= e
powerful features from mathematics, because these features have been p= olished
by mathematicians for centuries. As a consequence of this work, we know=
facts, properties and theorems about the mathematical features and this= is an
extremely valuable benefit.

Now, what is the next frontier= ? What can we steal more to mathematics for the
benefit of our favorite programming language ?

If we review the = most powerful tools of mathematicians, we found that
functions have been= borrowed (hello functional programming, lambda-calculus
and friends :))= , relations have been borrowed (data bases, hash tables,
association lists), sets have been more or less borrowed (hello setle,<= br>pascal, and set definition facilities from various libraries of various<= br>languages...). More or less, we have all those basic features.

>From the mathematical set construction tools, we have got in Caml:
<= br>- the cartesian product of sets (the * binary type constructor, the reco= rd
 type definitions),
- the disjunct union of sets (the | of p= olymorphic variants, the sum (or
 variant) type definitions).

Unfortunately, we have no pow= erful way to define a quotient data
structure. That what private type de= finitions have been designed to do.

What do we need for a quotient d= ata structure ?
-----------------------------------------------

In the first pla= ce, we need the ``true'' thing, the real feature that is
indeed = used in maths. Roughly speaking this means to assimilate the quotient
set S/R to a subset of S.

 In the previous definition of quotie= nt structures, there is a careful
distinction between the base set S and= the quotient set S/R. In fact, there
always exists a canonical injectio= n from S to S/R, and if we choose a
canonical representant in each equivalence class of S/R, we get another=
canonical injection from S/R to S, so that S/R can be considered as a s= ubset
of S (the story is a bit more complex but that's the idea). Th= is
injection/projection trickery is intensively used in maths; for instanc= e, in
the hierarchy of number sets, we say and consider that N is a subs= et of Z
that itself is a subset of Q, a subset of R, a subset of C. Rigo= urously, we
should say for instance, there is a subset of Z that is canonically
= isomorphic to N; in fact, we abusively assimilate N to this subset of Z;hence, we say that N is ``included'' in Z, when we should say ``th= e image of
N by the canonical isomorphism from N to Z'' is included in Z; = then, we go
one step further in the assimilation of N to a subset of Z, = by denoting the
same, the elements of N and there image in Z; for instan= ce, ``the neutral
element of the multiplication in Z'' and the successor of 0 in = N is denoted
``1''; and we now can say that 1 belongs to Z. Note= here that, in the first
place, ``the neutral element of the multiplicat= ion in Z'' is an equivalence
class (as all elements in Z are). So it is a set. More exactly, the ``n= eutral
element of the multiplication in Z'' is the infinite set = of pairs of natural
numbers (n, m) such that n - m =3D 1 (here ``-'&= #39; is an operation in N and ``1''
is the successor of the natural number ``0'', so that n - m =3D= 1 is a
shorthand for n =3D succ m). The assimilation between N and its = isomorphic
image allows to use 1 as the denotation of this infinite set = of pairs of
natural numbers.

We understand why the mathematicians always wri= te after having designed a
quotient structure: ``thanks to this isomorph= ism, and if no confusion may
arise, we always assimilate S to its canoni= cal injection in S/R''.

This assimilation is what private type definitions allow.

Ho= w do we define a quotient data structure ?
-----------------------------= ---------------

The mathematical problem:
- we have a set S and a= n equivalence relation R on SxS,
- we construct the quotient S/R.
- we state afterwards:
 ``= if no confusion may arise, we always assimilate S to its canonical
&nbs= p;  injection in S/R''.

The programming problem:
- w= e have a data structure S (defined by a type s) and a relation R on SxS
 (defined by a function r from s * s to bool).
- we construct = a data structure that represents S/R.
- we have afterwards:
 ``= No confusion may arise, we always assimilate S to its canonical injection    in S/R''.

The private data type solution:
- the data structure S is define= d as any Caml data structure and the
 relation R is implemented by= the canonical injection(s) from S to S/R.
- the canonical projection fr= om S/R to S is automatic.
- S (defined by s) is assimilated to S/R (which is then also s!).
We defined S/R as a subset of S, the set of canonical representants ofequivalence classes of S/R.

More exactly, the canonical injection f= rom S to S/R maps each element of S to
its equivalent class in S/R; if we assimilate each equivalence class to= its
canonical representant (an element of S), the canonical injection m= aps each
element of S to the canonical representant of its equivalence c= lass. Hence
the canonical injection has type S -> S.

An example treated w= ithout private types:
-----------------------------------------

L= et's take a simple example:

S is the following data structure th= at implements a mathematical (free) structure
generated by the constant 0, the unary symbol succ, and the binary symb= ol +.

type peano =3D
  | Zero
  | Succ of peano   | Plus of peano * peano

R is the (equivalence) relation tha= t expresses that
- 0 is the neutral element for + (for all x in S, 0 + x =3D x and x + 0= =3D x),
- + is associative (for all x, y, z in S=B3, (x + (y + z)) =3D = ((x + y) + z)).

The canonical injection is a function from peano -&g= t; peano that maps each value
in S (the type peano) to the canonical representant of its class in S/R= (an
element of S (the type peano)):

let rec make =3D function  | Zero -> Zero
 | Plus (Succ n, p) -> Succ (make (Pl= us (n, p)))
 | Plus (Zero, p) -> p
 | Plus (p, Zero) -> p
=  | Plus (Plus (x, y), z) -> make (Plus (x, make (Plus (y, z))))
=  | Succ p -> Succ p
;;

(This function may be wrong but y= ou see the idea :))

So, if you want to represent S/R for peano in Caml you must:
- (= 1) define the type peano
- (2) always use the make function to create a = value in S/R
- (3) not to confuse S and S/R in your head (I mean in your= programs)

Private data types permits (1), ensures (2), and helps for (3) conc= erning the
head part and ensures (3) for programs by means of compile-ti= me type errors.

The same example with private types:
------------= ------------------------

To define a private data type you must define a module.
- in the= implementation, you define the carrier S and its canonical injection.
-= in the interface, you export the carrier and the injection.

The typ= e checker will ensure transparent projection from the quotient to the
carrier and mandatory use of the canonical projection to build a value = in
S/R.

interface peano.mli
-------------------
type peano = =3D private
  | Zero
  | Succ of peano
  | Plus = of peano * peano
;;

val zero : peano;;
val succ : peano -> peano;;
val p= lus : peano * peano -> peano;;

implementation peano.ml
-----------------------
type = peano =3D
  | Zero
  | Succ of peano
  | Plus of peano * = peano
;;

let rec make =3D function
 ...
;;

let= zero =3D make Zero;;
let succ p =3D make (Succ p);;
let plus (n, m) = =3D make (Plus (n, m));;

(See note (1) for a discussion on the design of this example.)
<= br>What is given by private types:
-------------------------------
- You cannot create a value of S/R if you do not use the canonical inject= ion
 # Zero;;
 Cannot create values of the private type pean= o

- As a consequence, values in S (i.e. S/R) are always canonical:  # let one =3D succ zero;;
 val one : M.peano =3D Succ Zer= o
 # let three =3D plus (one, succ (plus (one, zero)));;
 val three : M.peano =3D Succ (Succ (Succ Zero))

- Project= ion is automatic
 # let rec int_of_peano =3D function
  &= nbsp;  | Zero -> 0
     | Succ n -> 1 + int_o= f_peano n
     | Plus (n, p) -> int_of_peano n + int_= of_peano p
   ;;
 val int_of_peano : M.peano -> int =3D <= ;fun>
 # int_of_peano three;;
 - : int =3D 3

Wh= at about private abbreviations ?
----------------------------------
<= br>Private abbreviation definitions are a natural extension of private data= type
definitions to abbreviation type definitions. The same notions are carr= ied
out mutatis-mutandis:

- we have a data structure S (defined b= y a type s) and a relation R on SxS
 (defined by a function r from= s * s to bool).
- we construct a data structure that represents S/R.
- we have after= wards:
 ``No confusion may arise, we always assimilate S to its ca= nonical injection
   in S/R''.

In the case of = abbreviations:

- the data structure S/R is defined by a type s (which is an abbrev= iation) and
 a relation defined by a function,
- the canonical = injection should be defined in the implementation file of the
 pri= vate data type module,
- we always assimilate S to its canonical injection in S/R.

In p= ratice, as for usual private types (for which the constructive part of
t= he data type is not available outside the implementation), the type abbrevi= ation
is not known outside the implementation (it is really private to itsimplementation). This prevents the construction of values of S/R withoutusing the canonical injection.

Th noticeable difference is the pro= jection function: it cannot be fully
implicit (otherwise, as you said Alain, the assimilation will turn to c= omplete
confusion: we would have S identical to S/R, hence row=3Dint and= no difference
between a regular abbreviation definition and a private a= bbreviation
definition). If not implicit, the injection function should granted to = be the
identity function (something that we would get for free, if we al= low
projection via sub-typing coercion).

In short: abstract data = types provide values that cannot be inspected nor
safely manipulated without using the functions provided by the module t= hat
defines the abstract data type. In contrast, private data types are<= br>explicitely concrete and you can freely write any algorithm you need. A = good
test is printing: you can always write a function to print values of a<= br>private type, it is up to the implementor of an abstract type to give yo= u the
necessary primitives to access the components of the abstracted va= lues.

Automatic generation of the canonical injection:
---------------= ---------------------------------

You may have realized that writing= the canonical injection can be a real
challenge.

The moca compil= er (see=20 http://moca.inria.fr/) helps you to write the
canonical injection by generating one for you= , provided you can express the
injection at hand via a set of predefined= algebraic relations (and/or rewrite
rules you specify) attached to the constructors of the private type. Pr= ivate
types with constructors having algebraic relations are named relat= ional
types. Moca generated canonical injections for relation types.

For instance, you would write the peano example as the following pe= ano.mlm
file:

type peano =3D private
  | Zero
 = | Succ of peano
  | Plus of peano * peano
  begin
&n= bsp;   associative
    neutral (Zero)
    rule Plus (Succ n, p) -> Succ (Plus (n, p))
 = ; end;;

The mocac compiler will generate the interface and implement= ation of the
peano module for you, including the necessary canonical inj= ection function.

Best regards,

--
Pierre Weis
INRIA Rocquencourt, http://bat8.inria.fr/~weis/

Note (1):
- we can= 9;t just export the canonical injection since you could not build any
 value of the type without previously defined values!
- we pro= vide specialized versions of the canonical injection function
 int= roducing the convention that the lowercase name of a value constructor is  the name of its associated canonical injection.
- we do not export the plasin true canonical injection since it would b= e more
 confusing than useful.

_______________________________________________
Caml-list mail= ing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://ca= ml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners=
Bug reports: http://caml.inria.fr/bin/caml-bugs
------=_Part_6215_2261711.1195173018344--