[Camllist] opaque polymorphism
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20010910 (23:19) 
From:  Brian Rogoff <bpr@b...> 
Subject:  Phantom types (very long) (Was Re: [Camllist] opaque polymorphism) 
On Mon, 10 Sep 2001, Francois Pottier wrote: > So ``hiding the polymorphism in 'b'' can be done, but you have to tell > the compiler which internal type should be used instead of 'b, i.e. you > have to choose <some type>. I guess the unit type will do in most > situations. There's a sort of "dual" trick of parameterizing a type over a type variable which is not used in the definition, the socalled phantom types. This trick seems to be well known by ML experts, but its not mentioned in any ML programming texts, sort of like the parameterization trick for recursive types and modules. I'll show three examples of phantom types below; if you already know this trick you can skip my very long, rambling message. The easiest example to start with is the core of an untyped lambda calculus interpreter. type term = Int of int  Bool of bool  Add of term * term  App of term * term  Lam of (term > term);; As we know, since this is untyped we can have self applications. # let bug = Lam(fun x > App(x,x));; val bug : term = Lam <fun> We'd like to forbid this, and one way is to implement a type checker. Here's how we can piggyback off of the OCaml one with phantom types. type 'a expr = Expr of term;; (* The phantom type *) let int : int > int expr = fun i > Expr (Int i);; let bool : bool > bool expr = fun b > Expr (Bool b);; let add : int expr > int expr > int expr = fun (Expr e1) (Expr e2) > Expr (Add(e1,e2));; let app : ('a > 'b) expr > ('a expr > 'b expr) = fun (Expr e1) (Expr e2) > Expr (App(e1,e2));; let lam : ('a expr > 'b expr) > ('a > 'b) expr = fun f > Expr (Lam(fun x > let (Expr b) = f (Expr x) in b));; Now we use these functions instead of the raw constructors. So our buggy term becomes # let bug = lam (fun x > app x x);; This expression has type 'a expr but is here used with type ('a > 'b) expr Cool! Note that we have to use explicit types or use the module system here (.mli and .ml files) otherwise we have (assuming I omit the type declarations in int, bool, add, app, lam) # let bug = lam (fun x > app x x);; val bug : '_a expr = Expr (Lam <fun>) The next example is based on a mail to this very Caml list http://caml.inria.fr/archives/199912/msg00090.html One of the points of that example was to put the permissions (readable or writable) of an entity into it's type. Rather than just copy Vouillon's excellent approach with row types, I'll be infinitesimally creative and show a version with polymorphic variants. here's the .mli (* Vouillon's phantom type, which originally used row types but works just fine with polymorphic variants. The idea is to make the permission check only once, when the mapped file is created, and thereafter use the type system to enforce read/write safety. *) type 'a perms type 'a t val read_only : [ `Readable ] perms val write_only : [ `Writable ] perms val read_write : [> `Readable  `Writable ] perms val map_file : string > 'a perms > int > 'a t val get : [> `Readable ] t > int > char val set : [> `Writable ] t > int > char > unit (* Vouillon's original interface with row types val read_only : <read:unit> perms val write_only : <write:unit> perms val read_write : <read:unit;write:unit> perms val map_file : string > 'a perms > int > 'a t val get : <read:unit;..> t > int > char val set : <write:unit;..> t > int > char > unit *) and here's a sample .ml, which type checks but might now work ;). open Unix open Bigarray type bytes = (int, int8_unsigned_elt, c_layout) Bigarray.Array1.t type 'a perms = int type 'a t = bytes let read_only = 1 let write_only = 2 let read_write = 3 let openflags_of_perms n = if n = 1 then O_RDONLY, 0o400 else if n = 2 then O_WRONLY, 0o200 else if n = 3 then O_RDWR, 0o600 else invalid_arg "openflags_of_perms" let access_of_openflags = function O_RDONLY > [R_OK; F_OK]  O_WRONLY > [W_OK; F_OK]  O_RDWR > [R_OK; W_OK; F_OK]  _ > invalid_arg "access_of_openflags" (* Check that "fd" permissions and "perms" matches *) let map_file filename perms sz = let (oflags, fperm) = openflags_of_perms perms in try access filename (access_of_openflags oflags); (* Check... *) let fd = Unix.openfile filename [oflags; O_CREAT] fperm in Array1.map_file fd int8_unsigned c_layout false sz with _ > invalid_arg "map_file: not even a valid permission!" let get a i = Char.chr (Array1.get a i) let set a i c = Array1.set a i (Char.code c) The final example is familiar to anyone who reads comp.lang.ml, where I mistakenly asserted that you couldn't have statically typed array dimensions in ML like you can in C++ or Ada. Matthias Blume then posted a solution which works (though it reminds me a bit of that proverb of the dancing bear). I've included a translation of the code into OCaml, with most of Blume's original comments. (* It is, surprisingly to some perhaps, actually possible to statically type arrays with (statically) fixed bounds in ML (just like in C). Here is the trick: We build an infinite family of types together with value constructors such that there is a 11 correspondence between nonnegative integers and types that have constructable values in this family. We can use the types in the family as "witness types" (aka "phantom types") that statically track array dimensions: In Ocaml: *) module DimArray : sig type dec type 'a d0 and 'a d1 and 'a d2 and 'a d3 and 'a d4 type 'a d5 and 'a d6 and 'a d7 and 'a d8 and 'a d9 type zero and nonzero type ('a, 'z) dim0 type 'a dim = ('a, nonzero) dim0 val dec : ((dec, zero) dim0 > 'b) > 'b val d0 : 'a dim > ('a d0 dim > 'b) > 'b val d1 : ('a, 'z) dim0 > ('a d1 dim > 'b) > 'b val d2 : ('a, 'z) dim0 > ('a d2 dim > 'b) > 'b val d3 : ('a, 'z) dim0 > ('a d3 dim > 'b) > 'b val d4 : ('a, 'z) dim0 > ('a d4 dim > 'b) > 'b val d5 : ('a, 'z) dim0 > ('a d5 dim > 'b) > 'b val d6 : ('a, 'z) dim0 > ('a d6 dim > 'b) > 'b val d7 : ('a, 'z) dim0 > ('a d7 dim > 'b) > 'b val d8 : ('a, 'z) dim0 > ('a d8 dim > 'b) > 'b val d9 : ('a, 'z) dim0 > ('a d9 dim > 'b) > 'b val dim : ('a, 'z) dim0 > ('a, 'z) dim0 val to_int : ('a, 'z) dim0 > int (* arrays with static dimensions *) type ('t, 'd) dim_array val make : 'd dim > 't > ('t, 'd) dim_array val init : 'd dim > (int > 'a) > ('a, 'd) dim_array val copy : ('a, 'd) dim_array > ('a, 'd) dim_array (* other array operations go here ... *) val get : ('a, 'd) dim_array > int > 'a val set : ('a, 'd) dim_array > int > 'a > unit val combine : ('a, 'd) dim_array > ('b, 'd) dim_array > ('a > 'b > 'c) > ('c, 'd) dim_array val length : ('a, 'd) dim_array > int val update : ('a, 'd) dim_array > int > 'a > ('a, 'd) dim_array val iter : f:('a > unit) > ('a, 'd) dim_array > unit val map : f:('a > 'b) > ('a, 'd) dim_array > ('b, 'd) dim_array val iteri : f:(int > 'a > unit) > ('a, 'd) dim_array > unit val mapi : f:(int > 'a > 'b) > ('a, 'd) dim_array > ('b, 'd) dim_array val fold_left : f:('a > 'b > 'a) > init:'a > ('b,'d) dim_array > 'a val fold_right : f:('b > 'a > 'a) > ('b, 'd) dim_array > init:'a > 'a val iter2 : f:('a > 'b > unit) > ('a,'d) dim_array > ('b, 'd) dim_array > unit val map2 : f:('a > 'b > 'c) > ('a, 'd) dim_array > ('b, 'd) dim_array > ('c, 'd) dim_array val iteri2 : f:(int > 'a > 'b > unit) > ('a,'d) dim_array > ('b, 'd) dim_array > unit val mapi2 : f:(int > 'a > 'b > 'c) > ('a, 'd) dim_array > ('b, 'd) dim_array > ('c, 'd) dim_array val fold_left2 : f:('a > 'b > 'c > 'a) > init:'a > ('b, 'd) dim_array > ('c, 'd) dim_array > 'a val fold_right2 : f:('a > 'b > 'c > 'c) > ('a, 'd) dim_array > ('b, 'd) dim_array > init:'c > 'c val to_array : ('a, 'd) dim_array > 'a array end = struct type dec = unit type 'a d0 = unit type 'a d1 = unit type 'a d2 = unit type 'a d3 = unit type 'a d4 = unit type 'a d5 = unit type 'a d6 = unit type 'a d7 = unit type 'a d8 = unit type 'a d9 = unit type zero = unit type nonzero = unit type ('a, 'z) dim0 = int (* Phantom type *) type 'a dim = ('a, nonzero) dim0 let dec k = k 0 let d0 d k = k (10 * d + 0) let d1 d k = k (10 * d + 1) let d2 d k = k (10 * d + 2) let d3 d k = k (10 * d + 3) let d4 d k = k (10 * d + 4) let d5 d k = k (10 * d + 5) let d6 d k = k (10 * d + 6) let d7 d k = k (10 * d + 7) let d8 d k = k (10 * d + 8) let d9 d k = k (10 * d + 9) let dim d = d let to_int d = d type ('t, 'd) dim_array = 't array let make d x = Array.make (to_int d) x let init d f = Array.init (to_int d) f let copy x = Array.copy x (* other array operations go here ... *) let get : ('a, 'd) dim_array > int > 'a = fun a d > Array.get a d let set : ('a, 'd) dim_array > int > 'a > unit = fun a d v > Array.set a d v let unsafe_get : ('a, 'd) dim_array > int > 'a = fun a d > Array.unsafe_get a d let unsafe_set : ('a, 'd) dim_array > int > 'a > unit = fun a d v > Array.unsafe_set a d v let combine : ('a, 'd) dim_array > ('b, 'd) dim_array > ('a > 'b > 'c) > ('c, 'd) dim_array = fun a b f > Array.init (Array.length a) (fun i > f a.(i) b.(i)) let length : ('a, 'd) dim_array > int = fun a > Array.length a let update : ('a, 'd) dim_array > int > 'a > ('a, 'd) dim_array = fun a d v > let result = Array.copy a in (Array.set result d v; result) let iter f a = Array.iter f a let map f a = Array.map f a let iteri f a = Array.iteri f a let mapi f a = Array.mapi f a let fold_left f x a = Array.fold_left f x a let fold_right f a x = Array.fold_right f a x let rec iter2 f a1 a2 = for i = 0 to length a1  1 do f (unsafe_get a1 i) (unsafe_get a2 i) done let rec map2 f a1 a2 = let l = length a1 in if l = 0 then [] else (let r = Array.make l (f (unsafe_get a1 0) (unsafe_get a2 0)) in for i = 1 to l  1 do unsafe_set r i (f (unsafe_get a1 i) (unsafe_get a2 i)) done; r) let rec iteri2 f a1 a2 = for i = 0 to length a1  1 do f i (unsafe_get a1 i) (unsafe_get a2 i) done let mapi2 f a1 a2 = let l = length a1 in if l = 0 then [] else (let r = Array.make l (f 0 (unsafe_get a1 0) (unsafe_get a2 0)) in for i = 1 to l  1 do unsafe_set r i (f i (unsafe_get a1 i) (unsafe_get a2 i)) done; r) let fold_left2 f accu a1 a2 = let r = ref accu in for i = 0 to length a1  1 do r := f !r (unsafe_get a1 i) (unsafe_get a2 i) done; !r let fold_right2 f a1 a2 accu = let r = ref accu in for i = length a1  1 downto 0 do r := f (unsafe_get a1 i) (unsafe_get a2 i) !r done; !r let to_array : ('a, 'd) dim_array > 'a array = fun d > d end;; (* Once all this is in place, you can say things like this ... open DimArray;; let d1230 = dec d1 d2 d3 d0 dim;; let a = make d1230 0.0;; ... open DimArray;; let d12 = dec d1 d2 dim;; let a = make d12 "bullshi";; let b = make d12 't';; let f s c = s ^ (Char.escaped c);; let abf = combine a b f;; ... The type of d1230 is "dec d1 d2 d3 d0 dim" (work it out!). By careful construction, this even happens to be textually the same as the expression that created d1230. Moreover, the value behind d1230 is 1230. In general, you get the dim value for any number by writing the number in decimal, adding "d" to each digit, adding a few spaces, and surrounding the thing with "dec ... dim". With this, you can now declare a variable to be an array of some precisely specified length: let a : (int, dec d1 d2 d3 d0) arr = ... The type checker will statically reject any attempt of making a an array of different size. This is just like in C. Now, beyond C, you can write functions that require twe equalsized arrays (but which make no other demands): val dot_product : (real, 'd) arr * (real, 'd) arr > real etc. It's easy to extend this to multidimensional arrays, where we can define a more type safe product val ( * ) : ('a, 'rows, 'cols) dim_array2 > ('b, 'cols, 'rows) dim_array2 > ('a > 'b > 'c) > ('c, 'rows, 'cols) dim_array2 You might argue that the above construction is ugly and lengthy, but it can be packaged up and put into a library. This is what I have done for my C interface, for example. Usage is exceedingly easy because thanks to ML's type inference you rarely have to actually write these types. Notice also that the above construction is slightly more complicated than it needs to be: I wrote the value constructors in CPS to get that cute type/expression equivalence. The set of constructors would have less complicated types if we were content to write let d1230 = d0 (d3 (d2 (d1 dec))) instead of the much cooler (:) let d1230 = dec d1 d2 d3 dim *)  Brian  Bug reports: http://caml.inria.fr/bin/camlbugs FAQ: http://caml.inria.fr/FAQ/ To unsubscribe, mail camllistrequest@inria.fr Archives: http://caml.inria.fr