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

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

[Shaddin Doghmi]

 From the CVS version  changes file, under language features:

- Support for "private types", or more exactly concrete data types
  with private constructors or labels.  These data types can be
  de-structured normally in pattern matchings, but values of these
  types cannot be constructed directly outside of their defining module.

What is the syntax for those? is there some kind of documentation on the 
CVS server, like a development version of the manual or something?


-------------------
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

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

[brogoff]

On Fri, 27 Jun 2003, Shaddin Doghmi wrote:
>  From the CVS version  changes file, under language features:
> 
> - Support for "private types", or more exactly concrete data types
>   with private constructors or labels.  These data types can be
>   de-structured normally in pattern matchings, but values of these
>   types cannot be constructed directly outside of their defining module.
> 
> What is the syntax for those? is there some kind of documentation on the 
> CVS server, like a development version of the manual or something?

No documents are available yet. Check out the following:

bpr@granite[bpr]$ ledit ~/bin/ocaml
        Objective Caml version 3.06+36 (2003-06-19)

# type t = private { x : int; y : int } ;;
type t = private { x : int; y : int; }
# type ('a, 'b) choice = private L of 'a | R of 'b;;
type ('a, 'b) choice = private L of 'a | R of 'b
# let p0 = { x = 0; y = 0 } ;;
One cannot create values of the private type t
# module Point2D : 
    sig 
      type t = private { x : int; y : int }
      val grid : int 
      val mkPoint : int -> int -> t 
    end = 
  struct
    type t = { x : int; y : int }
    let grid = 10 

    let snap i =
      let rem = i mod grid in
      if rem <= 0 then
	i - rem
      else
	i - rem + grid

    let mkPoint x y = { x = snap x; y = snap y } 
  end;;
module Point2D :
  sig
    type t = private { x : int; y : int; }
    val grid : int
    val mkPoint : int -> int -> t
  end
# open Point2D;;
# match mkPoint 5 5 with { x = x; y = y } -> Printf.printf "(%d, %d)\n" x y;;
(10, 10)
- : unit = ()

-- Brian

-------------------
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

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

[Shaddin Doghmi]

brogoff@speakeasy.net wrote:

>On Fri, 27 Jun 2003, Shaddin Doghmi wrote:
>  
>
>> From the CVS version  changes file, under language features:
>>
>>- Support for "private types", or more exactly concrete data types
>>  with private constructors or labels.  These data types can be
>>  de-structured normally in pattern matchings, but values of these
>>  types cannot be constructed directly outside of their defining module.
>>
>>What is the syntax for those? is there some kind of documentation on the 
>>CVS server, like a development version of the manual or something?
>>    
>>
>
>No documents are available yet. Check out the following:
>
>bpr@granite[bpr]$ ledit ~/bin/ocaml
>        Objective Caml version 3.06+36 (2003-06-19)
>
># type t = private { x : int; y : int } ;;
>type t = private { x : int; y : int; }
># type ('a, 'b) choice = private L of 'a | R of 'b;;
>type ('a, 'b) choice = private L of 'a | R of 'b
># let p0 = { x = 0; y = 0 } ;;
>One cannot create values of the private type t
># module Point2D : 
>    sig 
>      type t = private { x : int; y : int }
>      val grid : int 
>      val mkPoint : int -> int -> t 
>    end = 
>  struct
>    type t = { x : int; y : int }
>    let grid = 10 
>
>    let snap i =
>      let rem = i mod grid in
>      if rem <= 0 then
>	i - rem
>      else
>	i - rem + grid
>
>    let mkPoint x y = { x = snap x; y = snap y } 
>  end;;
>module Point2D :
>  sig
>    type t = private { x : int; y : int; }
>    val grid : int
>    val mkPoint : int -> int -> t
>  end
># open Point2D;;
># match mkPoint 5 5 with { x = x; y = y } -> Printf.printf "(%d, %d)\n" x y;;
>(10, 10)
>- : unit = ()
>
>-- Brian
>
>-------------------
>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
>  
>
neat. However, private doesnt seem to work with polymorphic 
variants(tried a bunch of variations of the syntax, nothing worked). 
Looking at the parser source seems to confirm that (i think ?), or am i 
missing something....




-------------------
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

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

[brogoff]

Yup, private also doesn't work with tuples.

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"? 

As Jacques Garrigue said in another message, polymorphic variants are somewhat  
inimical to abstract types, and private doesn't make much sense without type 
abstraction. Since one needn't predeclare variant tags or qualify them with 
module paths, it makes sense that private doesn't apply. 

-- Brian



-------------------
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

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

[Pierre Weis]

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

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

[Chris Hecker]

[Excellent rationale for private types snipped.]

>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.

So, when do we get views to solve this problem for abstract types?  If 
pattern matching is so great (which it is) it seems a crime to not allow it 
on abstract types (another great feature).  To make an american candy joke, 
peanut butter and chocolate taste great together!

Chris

-------------------
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

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

[brogoff]

On Mon, 30 Jun 2003, Chris Hecker wrote:
> [Excellent rationale for private types snipped.]

Indeed. Nice feature. 

> >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.
> 
> So, when do we get views to solve this problem for abstract types?  If 
> pattern matching is so great (which it is) it seems a crime to not allow it 
> on abstract types (another great feature).  To make an american candy joke, 
> peanut butter and chocolate taste great together!

I guess we all know what you're going for when you hit that vending machine!

I was going to reply to a message in last week's thread about polytypic 
programming in which the use of open recursion/fixed points on functions was
demonstrated, that there is a "dual" trick at the level of types, the 
so-called two level types. One place this trick finds some use is in the 
encoding of views into ML like languages. You can find the trick demonstrated 
for SML here 

http://www.cs.princeton.edu/~danwang/drafts/recursion-schemes.pdf

but I'm not sure how much using this style costs in efficiency in OCaml. 
If it costs too much, we'll have to bug Stephen Weeks to implement OCamlton. 
BTW, it's nice to have views (and all kinds of things) supported directly in 
the language but these tricks seem workable to me. It seems like OCaml 
could be a bit nicer than SML here (what a surprise! :), since we could use 
polymorphic variants for the external interface, as there is no type 
abstraction there. For example, something like the following for the earliest 
examples in that paper 

module type NAT =
  sig
    type t
    type 'a s = [`Zero | `Succ of 'a]
    val inj : t s -> t
    val prj : t -> t s
  end

module SimpleNat : NAT =
  struct
    type 'a s = [`Zero | `Succ of 'a]

    (* Look ma, no intermediate constructor for recursive types! *)
    type t = t s

    let inj x = x
    let prj x = x
  end

module FastNat : NAT =
  struct
    type 'a s = [`Zero | `Succ of 'a]
    type t = int

    let inj = function
        `Zero -> 0
      | `Succ n -> n + 1

    let prj = function
        0 -> `Zero
      | n -> `Succ (n - 1)
  end

As a digression, the two level type trick is also used (in OCaml) here 

http://www.eecs.harvard.edu/~nr/pubs/mania-abstract.html
(This is a very appealing paper to me, as the embedded language technique the 
author describes looks applicable to a few things I'm doing) 

and here 

http://homepage.iis.sinica.edu.tw/~trc/padl00.ps

and of course in a ton of Haskell/Gofer/Squiggol oriented papers. 

As another digression, the trick of using open recursive functions and "fixing" 
them manually with special fps is explained nicely here:

 http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-375/

though the post last week was the first time I saw it used in quite that way. 
That was quite neat. I wonder how that technique dovetails with two level 
types? 

-- Brian


-------------------
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

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

[Pierre Weis]

> So, when do we get views to solve this problem for abstract types?  If 
> pattern matching is so great (which it is) it seems a crime to not allow it 
> on abstract types (another great feature).  To make an american candy joke, 
> peanut butter and chocolate taste great together!
> 
> Chris

Hem, the introduction of the private type feature was just my answer
to this question. I wanted to get the security of type abstraction
without the drawback of loosing pattern matching.

Put it another way:

-- regular data types are concrete, you can freely create their values
with constructors or labels, you can inspect their values via pattern
matching,

-- private types are ``semi concrete'', you cannot freely create their
values (you are obliged to use their construction functions) but you
can still inspect their values via pattern matching,

-- abstract types are not concrete, you cannot freely create their
values (you are obliged to use the construction functions they
provide) and you cannot inspect their values via pattern matching (you
are also obliged to use the inspection functions they provide).

Yet another way (coarse and oversimplified view (:)):

-- concrete types are freely readable/writable data types,

-- private types are freely read only data types,

-- abstract types are nor freely readable nor freely writable data types.

And some specific advantages of each:

-- concrete types give you the maximum freedom (no invariants to
respect, no burden with construction functions), but you get a maximum
dependancy on the implementation (modification of the concrete type is
visible all over the place). Addition of operators is easy.

-- abstract types give you the maximum security (strict enforcement of
invariants by the compiler), no dependancy on the implementation that
can be modified as required by the implementor of the type, no
possibility of confidentiality leaks: the contents of a value that can
have truely hidden parts. Addition of operators is difficult or impossible.

-- private types give you the same security as abstract types for
invariants and the same facility for the addition of new
operators. You loose the ability to hide parts of values.

In my mind, private types give you for free a lot of useful facilities
that you could have with views, while retaining invaluable, both
conceptual and implementationnal, simplicity.

You may be right that eventually Caml could still need an extra
feature as powerful and complex as views for abstract data types, but
for the time being let's start and experiment with this now available,
simple, and effective feature. It has already proved to be incredibly
powerful and efficient for some applications. So let's go and discover
where we still need more :)

I mean, try it :)

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

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

[Hendrik Tews]

Pierre Weis writes:
   
   As you should already know, usual sum and product types in Caml
   correspond to the mathematical notion of free algebraic data
   structures. 

If you consider the ocaml fragment without recursive values.
For instance:

   type nat =
      | Zero
      | Succ of nat;;
   
   let rec x = Succ x;;

This x does not belong to the free algebra. 


(And BTW, the product types are not free, they are cofree or
terminal or final, whatever terminology you prefer.)


Sorry for nitpicking,

Hendrik Tews

-------------------
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

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

[Yaron M. Minsky]

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

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

[Yaron M. Minsky]

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

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

[Pierre Weis]

> 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
> -- 
> |--------/            Yaron M. Minsky              \--------|
> |--------\ http://www.cs.cornell.edu/home/yminsky/ /--------|

You are right: that's yet another way to say it :)

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

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

[brogoff]

On Tue, 1 Jul 2003, Pierre Weis wrote:
> > 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
> > -- 
> > |--------/            Yaron M. Minsky              \--------|
> > |--------\ http://www.cs.cornell.edu/home/yminsky/ /--------|
> 
> You are right: that's yet another way to say it :)

To make this a bit more consistent, wouldn't it be better to restrict the 
occurrence of private to signatures? It is currently allowed in structs too. 
Is there a case where it is useful outside of a signature?

There was a similar idea that was proposed a while ago about providing 
an immutable view of mutable objects, which is also appealing. Any progress 
with that one? 

-- Brian


-------------------
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

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

[John Max Skaller]

Pierre Weis wrote:


> 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.


Well said. If I may add: this can already be done using

classes, or abstraction of modules. However these tools
are much *too* heavyweight, because they also hide the
algebraic structure of the types completely.

The user then must provide all the accessor functions,
for example, instead of using record labels or pattern matching.

For immutable values, establishing an invariant at construction

time is enough to ensure the invariant is preserved: therefore,
it is enough to make construction abstract to ensure all values
of the type satisfy the invariants.

Just for interest, this is not the case for mutable objects,

for example:

	type rational = private { mutable x: float; mutable y: float };
	...
	let mess_up_invariant (z:rational) = z.y <- 0.0

Be interested to know the treatment of records with mutable fields.
Are they permitted? Or are the mutators disallowed?

> 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.


Indeed, a fine dissertation, and a good choice for an extension

as well. Thanks!

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
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

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

[Pierre Weis]

> > 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.
> 
> 
> Well said. If I may add: this can already be done using
> 
> classes, or abstraction of modules. However these tools
> are much *too* heavyweight, because they also hide the
> algebraic structure of the types completely.
> 
> The user then must provide all the accessor functions,
> for example, instead of using record labels or pattern matching.

Absolutely. That's just the idea behind private types: ensure the
necessary invariants but keep the ease of rpogramming new functions
via pattern matching (and save the burden to provide all the
accessors).

> For immutable values, establishing an invariant at construction
> time is enough to ensure the invariant is preserved: therefore,
> it is enough to make construction abstract to ensure all values
> of the type satisfy the invariants.

Exactly.

> Just for interest, this is not the case for mutable objects,
> for example:
> 
> 	type rational = private { mutable x: float; mutable y: float };
> 	...
> 	let mess_up_invariant (z:rational) = z.y <- 0.0
> 
> Be interested to know the treatment of records with mutable fields.
> Are they permitted? Or are the mutators disallowed?

Records with mutable fields are permitted. Mutators explicitely exported
as functions are allowed, other mutations are forbidden.

I once wrote a lot of arithmetics and helped people writing core
arithmetics libraries for Caml. I always thought we had a major flaw
in the design of the library, due to type abstraction: we were
constantly oscillating between two conflicting attitudes; on the one
hand, using abstract data types all over the place to preserve
invariants and on the other hand turning to concrete types, not to be
forced to code everything ourself within the module implementing the
ADT.

I think private types are also a good answer to the
problem. Implementation of rational numbers would use a record with
mutable fields, and define a rational creation and a normalization
functions, preserving invariants:

type rat = {
  mutable numerator : int;
  mutable denominator : int;
};;

let rec mk_rat n d =
 if d = 0 then failwith "mk_rat: null denominator" else
 if d < 0 then mk_rat (- n) (- d) else
 { numerator = n; denominator = d};;

(* Left as an exercise *)
let gcd n m = 1;;

let normalize_rat r =
 let g = gcd r.numerator r.denominator in
 if g <> 1 then begin
   r.numerator <- r.numerator / g;
   r.denominator <- r.denominator / g
 end;;

Then interface of the module would abstract creation and mutation:

type rat = private {
  mutable numerator : int;
  mutable denominator : int;
};;

val mk_rat : int -> int -> rat;;

val normalize_rat : rat -> unit;;

This way, there is no need to define access to numerator and
denominator, or even to write printing functions: the user can write
them easily:

open Rat;;

let print_rat r =
 normalize_rat r;
 match r with
 | { numerator = n; denominator = d} -> Printf.printf "%d/%d" n d;;   

Also, any attempt to mutate a rational is now statically rejected by
the typechecker:

let r = mk_rat 1 2 in
r.numerator <- 4;

Cannot assign field numerator of private type Rat.rat.

Hence, in a sense, private types can also serve as a primitive way to
turn a mutable data type into an immutable one outside its defining
implementation, provided that no mutating functions are exported.

A small addition for the language, a big step for the programmer :)

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

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

[John Max Skaller]

Pierre Weis wrote:


> Records with mutable fields are permitted. Mutators explicitely exported
> as functions are allowed, other mutations are forbidden.


...


> type rat = {
>   mutable numerator : int;
>   mutable denominator : int;
> };;
 
> Then interface of the module would abstract creation and mutation:
> 
> type rat = private {
>   mutable numerator : int;
>   mutable denominator : int;
> };;
> 
> val mk_rat : int -> int -> rat;; 
> val normalize_rat : rat -> unit;;

OK. Nice. 'private' is allowed in the interface, and matches
a non-private record defined in the module. [I imagine
generated accessor and mutators here .. a field label
just being shorthand way to specify a projection function
etc ..]

-- 
John Max Skaller, mailto:skaller@ozemail.com.au
snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia.
voice:61-2-9660-0850


-------------------
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

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

[Laurent Vibert]

On Sun, 13 Jul 2003, John Max Skaller wrote:

> Pierre Weis wrote:
> 
> 
> > Records with mutable fields are permitted. Mutators explicitely exported
> > as functions are allowed, other mutations are forbidden.
> 

So just a question : since mutations are forbidden, would it be safe to 
relaxe the variance for mutable field, to allow something like

type +'a foo = private {mutable it : 'a}



-------------------
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

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

[Pierre Weis]

> On Sun, 13 Jul 2003, John Max Skaller wrote:
> 
> > Pierre Weis wrote:
> > 
> > 
> > > Records with mutable fields are permitted. Mutators explicitely exported
> > > as functions are allowed, other mutations are forbidden.
> > 
> 
> So just a question : since mutations are forbidden, would it be safe to 
> relaxe the variance for mutable field, to allow something like
> 
> type +'a foo = private {mutable it : 'a}

No, since the field ``it'' is indeed mutable and can be mutated either
directly from within the module implementation, or indirectly via a
mutator function that would be exported in the interface.

In addition, the compiler has to know that field ``it'' is mutable, so
that it can take care of ``it'' fields in pattern matching (the
compiler must bind the contents of those field patterns to avoid bus
errors in the expression part of the corresponding clause).

Euh, if you really want a field to be treated as not mutable, just
define it as immutable :)

Simple enough, isnt'it ?

Best regards,

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