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

[Alain Frisch <alain@frisch.fr>]

Martin Jambon wrote:
> You can write
>   match (x : Priv_int.t) with 0 -> true | _ -> false

Actually, you cannot do that, at least with private types as implemented 
in OCaml's CVS. And this is to be expected given the lack of implicit 
subsumption in OCaml. If you were able to do such a thing, what type 
schema would you give to:

   let f = function 0 -> true | _ -> false

?

This function should work on integers as well as on values of type 
Priv_int.t, but the type algebra cannot express that.


My understanding (Pierre will correct me if I'm wrong) is that private 
type abbreviations, as they are currently implemented, can always be 
replaced by abstract types without turning a well-typed program into an 
ill-typed one. Doing so will prevent some type-based optimizations to 
happen, though.

But the really interesting thing is that the new feature opens the door 
to extending the subtyping operator :> to take into account the natural 
(identity) injection from a private abbreviation to the underlying type. 
This is especially useful when the value of the private type appears 
deeply nested in a structure. With a normal function that implements the 
injection, you need to lift it to the whole structure which forces 
useless copies (and worse: the manual lifting may not be possible if 
some module declares a covariant type without a corresponding map 
function).

For instance:

(l : (Priv_int.t * Priv_int.t) list :> (int * int) list)

instead of

List.map (fun (x, y) -> (Priv_int.to_int x, Priv_int.to_int y)) l



-- Alain