English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Compiler feature - useful or not?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-11-15 (22:32)
From: michael.le_barbier@l...
Subject: Re: [Caml-list] Compiler feature - useful or not?
Edgar Friendly <thelema314@gmail.com> writes:

> After reading everything about quotient types and the need for private
> types, I have to ask "why not just completely abstract the type"?  What
> you seem to want from private types, you seem to gain pretty easily
> through abstract types.

I think you have overlooked the following example in Pierre's article:

- Projection is automatic
  # let rec int_of_peano = 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 = <fun>
  # int_of_peano three;;
  - : int = 3

Since we have access to the representation of the value we can filter
values (just like in the example) and since we are unable to create
ill-shaped values, we can assume that good invariants are true in the
values we are examining.

If we want to do the same with abstract data types, we would have
two types involved instead of one:

* the abstract type peano already described;
* a second type `good_representation' and an explicit application
  `projection: peano -> good_representation'

Let's say that sets manipulated through the `Set' module are
represented by balanced trees. If the type set had been private
instead of abstract, we could investigate the representation of a
value of the type but could not produce an ill-formed value (an
`unbalenced tree').

(I also may be totally wrong :) )