Phantom types and polymorphic containers

Phantom types and polymorphic containers

[Goswin von Brederlow]

Hi,

I'm wondering if one can create a polymorphic container with Phantom
types that can store types that themself have phantom types and get the
two to correlate. So far I've only been able to create a non-polymorphic
container with phantom types and even that isn't perfect:

Say I have my phantom typed string:

module S : sig
  type 'a t = private string
  val make : string -> [`Read | `Write] t
  val make_const : string -> [`Const | `Read] t
  val read_only : [> `Read] t -> [`Read] t
  val get : [> `Read | `Const] t -> int -> char
  val set : [> `Write] t -> int -> char -> unit
end = struct
  type 'a t = string
  let make x = x
  let make_const x = String.copy x
  let read_only x = x
  let get x i = x.[i]
  let set x i c = x.[i] <- c
end

And then my (non-polymorphic) Container:

module C : sig
  type ('a, 'b) t = private 'a S.t ref
  val make : 'a S.t -> ('a, [`Read | `Write]) t
  val read_only : ('a, [> `Read]) t -> ('a, [`Read]) t
  val get : ('a, [> `Read]) t -> 'a S.t
  val set : ('a, [> `Write]) t -> 'a S.t -> unit
end = struct
  type ('a, 'b) t = 'a S.t ref
  let make x = ref x
  let read_only x = x
  let get x = !x
  let set x y = x := y
end

Now to test this: (this is the expected behaviour)

# let s = S.make "write";;
val s : [ `Read | `Write ] S.t = "write"
# let c = C.make s;;
val c : [ `Read | `Write ] C.t = {contents = "write"}
# C.set c s;;
- : unit = ()
# let s2 = C.get c;;
val s2 : [ `Read | `Write ] S.t = "write"
# S.set s2 0 'C';;
- : unit = ()
# let d = C.read_only c;;
val d : ([ `Read | `Write ], [ `Read ]) C.t = {contents = "write"}
# C.set d s;;
        ^
Error: This expression has type ([ `Read | `Write ], [ `Read ]) C.t
       but an expression was expected of type
         ([ `Read | `Write ], [> `Write ]) C.t
       The first variant type does not allow tag(s) `Write
# let s2 = C.get d;;
val s2 : [ `Read | `Write ] S.t = "write"
# S.set s2 0 'W';;
- : unit = ()


# let s = S.read_only (S.make "read");;
val s : [ `Read ] S.t = "read"
# let c = C.make s;;
val c : [ `Read ] C.t = {contents = "read"}
# C.set c s;;
- : unit = ()
# let s2 = C.get c;;
val s2 : [ `Read ] S.t = "read"
# S.set s2 0 'C';;
        ^^
Error: This expression has type [ `Read ] S.t
       but an expression was expected of type [> `Write ] S.t
       The first variant type does not allow tag(s) `Write



But one thing doesn't quite work:

# let s1 = S.make "foo";;
val s1 : [ `Read | `Write ] S.t = "foo"
# let s2 = S.read_only s1;;
val s2 : [ `Read ] S.t = "foo"
# let c = C.make s2;;
val c : ([ `Read ], [ `Read | `Write ]) C.t = {contents = "foo"}
# C.set c s1;;
          ^^
Error: This expression has type [ `Read | `Write ] S.t
       but an expression was expected of type [ `Read ] S.t
       The second variant type does not allow tag(s) `Write

I would like c to accept [> `Read] strings. I want a signature like this:

  val set : ('a, [> `Write]) t -> [> 'a] S.t -> unit

and I think the get would have to change then to:

  val get : ('a, [> `Read]) t -> [> 'a] S.t

But [> type] only seems to work with specific polymorphic variant types
and not with polymorphic types:

# type 'a foo = [`A | `B];;
type 'a foo = [ `A | `B ]
# type ('a, 'b) f = ([> 'b] as 'a) -> unit;;
                        ^^
Error: The type 'a is not a polymorphic variant type
# type ('a, 'b) f = ([> 'b foo] as 'a) -> unit;;
type ('a, 'b) f = 'a -> unit constraint 'a = [> 'b foo ]

At least I can't find how.


Any ideas how to make the container polymorphic?

MfG
        Goswin