[Caml-list] opaque polymorphism

[Caml-list] opaque polymorphism

[Charles Martin]

A feature that would be nice would be to hide the polymorphism of a type in a
module signature:

foo.ml:
type ('a, 'b, 'c) t = { ... }

foo.mli:
type ('a, 'c) t

Thus, clients of Foo would be unaware of the polymorphism in 'b.  This would
require that type variables in signatures and structures be matched on their
names, obviously.

Can any of the type experts out there tell me if this is possible?


__________________________________________________
Do You Yahoo!?
Get email alerts & NEW webcam video instant messaging with Yahoo! Messenger
http://im.yahoo.com
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] opaque polymorphism

[Francois Pottier]

Hello Charles,

You can write:

  foo.ml:
  type ('a, 'b, 'c) internal_t = { ... }

  type ('a, 'c) t = ('a, <some type>, 'c) internal_t

 
  foo.mli:
  type ('a, 'c) t

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.

Hope this helps,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Phantom types (very long) (Was Re: [Caml-list] opaque polymorphism)

[Brian Rogoff]

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 so-called 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 1-1 correspondence between non-negative 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 equal-sized 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/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: Phantom types (very long) (Was Re: [Caml-list] opaque polymorphism)

[Andreas Rossberg]

Brian Rogoff wrote:
> 
> 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).

Actually, Matthias gave a very interesting talk on the Babel workshop in
Florence last Saturday where he showed how to encode the complete C type
system in ML (including functions, pointers, constness, bitfields, and
all dark corners - the only bit still missing is varargs), using even
more phantom type trickery. Unfortunately, the paper is not yet
available online, but as his work is part of the new FFI of SML/NJ you
can read about the encoding in its documentation (inside the
ml-nlffi-lib.tgz of the latest working version).

Cheers,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids; I mean if Pac Man affected us
 as kids, we would all be running around in darkened rooms, munching
 magic pills, and listening to repetitive electronic music."
 - Kristian Wilson, Nintendo Inc.
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

[Caml-list] Re: Phantom types (very long)

[j h woodyatt]

So okay... I take it back.  Caml *does* have invariants.  (I'm 
learning.  Slowly.  But I'm learning.)

This "phantom types" design pattern is one I have never seen before.  It 
doesn't seem to be used in the standard library anywhere I can see.  It 
looks like it might be useful in presenting a safer network programming 
interface than the low-level wrappers around BSD sockets (which I've 
never liked).

Are there any other mind-blowingly elegant design patterns lurking in 
the corners of the Caml type inference engine that I should know about?


--
j h woodyatt <jhw@wetware.com>
"You're standing on sacred ground.  Many strange and wonderful
things have transpired right where you're standing."
                                               --unattributable

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Re: Phantom types (very long)

[Brian Rogoff]

On Tue, 11 Sep 2001, j h woodyatt wrote:
> So okay... I take it back.  Caml *does* have invariants.  (I'm
> learning.  Slowly.  But I'm learning.)
>
> This "phantom types" design pattern is one I have never seen before.

I remember reading J. Vouillon's post a long time ago and thinking "Man,
that's weird, having that type parameter not show up on the right hand
side of the type definition!" But it wasn't until Blume's post on the ML
ng that I got a name for the concept "phantom" and "witness" types. Do a
Google search on "phantom type" and you'll turn up a few Haskell paper's,
most notably tsome ones on connecting Haskell to Microsoft COM, and some
on domain specific languages.

> It doesn't seem to be used in the standard library anywhere I can see.  It
> looks like it might be useful in presenting a safer network programming
> interface than the low-level wrappers around BSD sockets (which I've
> never liked).

It's always a good idea to have thin (low level bindings) available. You
can build your abstractions on top of them, but to do otherwise is an
abstraction inversion.

> Are there any other mind-blowingly elegant design patterns lurking in
> the corners of the Caml type inference engine that I should know about?

Yes! And there there will be even more when we get polymorphic recursion
and generics ;-)

-- Brian

PS: Yeah, I'll post some more soon assuming I don't get blown up. Many
tricks involve simulating dependent types so if you look up dependent
types that'll get you started. In particular try to understand Danvy's
"Functional Unparsing"" paper.



-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Re: Phantom types (very long)

[Daan Leijen]

On Tue, 11 Sep 2001, j h woodyatt wrote:
> This "phantom types" design pattern is one I have never seen before.  It
> doesn't seem to be used in the standard library anywhere I can see.  It
> looks like it might be useful in presenting a safer network programming
> interface than the low-level wrappers around BSD sockets (which I've
> never liked).

We used phantom types extensively  for exactly this purpose -- a typed
wrapper around a low-level interface. It seems that the trick has been in
use
already in the 80's for ML libraries that accessed sockets (allthough it
didn't
had a sexy name in that time). We tried to describe the general use pattern
in detail in the paper "domain specific embedded compilers" which can be
found at:

http://www.cs.uu.nl/~daan/pubs.html

We also used phantom types to encode single type inheritance for the
H/direct frame work (described in "calling hell from heaven and heaven from
hell")

All the best,
    Daan Leijen.


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Re: Phantom types (very long)

[Jacques Garrigue]

> This "phantom types" design pattern is one I have never seen before.  It 
> doesn't seem to be used in the standard library anywhere I can see.  It 
> looks like it might be useful in presenting a safer network programming 
> interface than the low-level wrappers around BSD sockets (which I've 
> never liked).

Thay are used in both Bigarray and Labltk (the 'a widget type). In
fact they were already used in Labltk before the word phantom started
to be used for them.

> Are there any other mind-blowingly elegant design patterns lurking in 
> the corners of the Caml type inference engine that I should know about?

I don't know if this is mind blowing, but thanks to variance
annotations on abstract types, you can also have subtyping on
"phantom" types. This is used in lablgtk for instance:

type (-'a) gtkobj
type widget = [`widget]
type container = [`widget|`container]
type box = [`widget|`container|`box]

now you can cast safely between classes:
    (mybox : box gtkobj :> container gtkobj)

Note that the parameter must be contravariant if you use polymorphic
variant types as indexes, or covariant if you rather use object types.

This also works ok with polymorphism, encoding inheritance (even
multiple) in a direct way.
val add : [> `container] gtkobj -> [> `widget] gtkobj -> unit

Cheers,

        Jacques Garrigue
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] Re: Phantom types (very long)

[Brian Rogoff]

On Fri, 14 Sep 2001, Jacques Garrigue wrote:
> > This "phantom types" design pattern is one I have never seen before.  It
> > doesn't seem to be used in the standard library anywhere I can see.  It
> > looks like it might be useful in presenting a safer network programming
> > interface than the low-level wrappers around BSD sockets (which I've
> > never liked).
>
> Thay are used in both Bigarray and Labltk (the 'a widget type). In
> fact they were already used in Labltk before the word phantom started
> to be used for them.

Right, and I think that each new use causes some of the newer ML (and
Haskell, Mercury too?) programmers to do a few double takes. I know the
first time I saw this usage on this mailing list I was a bit boggled.
In retrospect each new usage seems relatively obvious, but it wouldn't
hurt to have this (and the parameterization trick, and the trick that
Tyng-Ruey Chuang uses to write polynomial data types, and a whole bunch of
others ...) explained simply for the practitioner.

> > Are there any other mind-blowingly elegant design patterns lurking in
> > the corners of the Caml type inference engine that I should know about?
>
> I don't know if this is mind blowing, but thanks to variance
> annotations on abstract types, you can also have subtyping on
> "phantom" types. This is used in lablgtk for instance:
>
> type (-'a) gtkobj
> type widget = [`widget]
> type container = [`widget|`container]
> type box = [`widget|`container|`box]
>
> now you can cast safely between classes:
>     (mybox : box gtkobj :> container gtkobj)
>
> Note that the parameter must be contravariant if you use polymorphic
> variant types as indexes, or covariant if you rather use object types.
>
> This also works ok with polymorphism, encoding inheritance (even
> multiple) in a direct way.
> val add : [> `container] gtkobj -> [> `widget] gtkobj -> unit

What a great mailing list! Thanks for that one. I hope to see it in the
lablgtk docs soon.

-- Brian


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr