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-16 (15:08)
From: Martin Jambon <martin.jambon@e...>
Subject: Re: [Caml-list] Compiler feature - useful or not?
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.