Re: [Caml-list] Compiler feature - useful or not?

[Fernando Alegre <fernando@mail.alemor.org>]

The main problem I have with abstract types is that they are heavyweight
since they need to be defined inside modules. In that particular, the
proposed private types are also heavyweight.

I would like to have private types be some kind of lightweight abstract
types, as illustrated in the following example with two different
injections and two different projections between integers and even
numbers. Note that no modules are needed. The only way to get into or out
of a private type would be by explicit coercion.

Private types defined this way would be sound, as expressions like
"half 10" would be forbidden by the compiler. The right expression
would be "half (10 :> even)". A programmer may break the semantics of
"even" by writing things such as "(11 :> even)", but he better know
what he is doing. The current abstract types can be used to make a private
type abstract too if that safety is needed.

type even = private int

let half (x:even) = (x :> int)/2
val half : even -> int

let int_of_even (x:even) = (x :> int)
val int_of_even : even -> int

let dbl (x:int) = (2*x :> even)
val dbl : int -> even

let even_of_int (x:int) =
	if x mod 2 = 0 then (x :> even)
	else invalid_arg "even_of_int"
val even_of_int : int -> even

There is another less natural way to encode even numbers that enforces
automatically the semantics: even number 2*n is encoded as integer n.
Then, the example becomes:

type even = private int

let half (x:even) = (x :> int)
let int_of_even (x:even) = 2*(x :> int)

let dbl (x:int) = (x :> even)
let even_of_int (x:int) =
	let e = x/2 in
	if 2*e = x then (e :> even)
	else invalid_arg "even_of_int"

However, this kind of semantics-preserving encoding is just a matter of good
luck, and I don't think it can be generalized to many cases, at least
statically. You could always have a run-time check, but that misses the
point. Although, I don't see a way to avoid the run-time check in the
function even_of_int...

In summary, in my opinion private types should be completely orthogonal
to abstract types, so that both can be used either together or
separately.

Thanks,
Fernando

On Thu, Nov 15, 2007 at 11:29:25AM -0600, Edgar Friendly wrote:
> Okay, let's see if I can summarize:
> 
> Private types have use because you can expose your implementation while
> still having control over construction of values.  This is important for
> implementing quotient structures.
> 
> 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.
> 
> E.
> 
> _______________________________________________
> 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