On Fri, 16 Nov 2007, Alain Frisch wrote:

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

Using the notation for polymorphic variant types:

val f : [< int ] -> bool

Type [> int ] would be the same as [ int ] or int.



> 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

Thanks, this is clear now.


--
http://wink.com/profile/mjambon
http://martin.jambon.free.fr