Erasing type parameter

Question

I have a module Socket using phantom types to enforce some simple access control:

module Socket : sig
  type 'a t

  val ro : string -> [ `Read ] t
  val rw : string -> [ `Read | `Write ] t
end

I want to wrap a Socket.t in a Container.t record, but is there some way not to propagate the phantom type parameter also into Container.t?

module Container : sig
  type 'a t =
  {     
  owner: string;
  socket: 'a Socket.t;
  }     
end

Answer 1

In general, you may use existential types to forget about some type parameter: instead of the type 'a foo, you use exists_foo that contains a value of type 'a foo, for some 'a you don't know about. There are several ways to build existential types in OCaml (polymorphic records or first-class modules).

In the case of a phantom type, you can provide a way, through your interface, to convert any socket into an "untyped socket" that has forgotten about its previous capabilities.

type untyped

module Socket : sig
  type 'a t

  val ro : string -> [ `Read ] t
  val rw : string -> [ `Read | `Write ] t
  val untyped : 'a t -> untyped t
end = struct
  type 'a t = string
  let ro s = s
  let rw s = s
  let untyped s = s
end

type t = { owner : string; socket : untyped Socket.t }

let test = {
  owner = "foo";
  socket = Socket.(untyped (ro "bar"))
}

Of course, you have to choose what is possible for an untyped socket, for which you don't know anymore how it was opened. Maybe it's not what you had in mind?

You can also keep the socket in a sum type, to preserve the knowledge of its capabilities:

module Socket : sig
  type 'a t
  val ro : string -> [ `Read ] t
  val rw : string -> [ `Read | `Write ] t

  val read : [> `Read ] t -> unit
  val write : [> `Write ] t -> unit
end = struct
  type 'a t = string
  let ro s = s
  let rw s = s
  let read _ = ()
  let write _ = ()
end

type some_socket =
  | Ro of [ `Read ] Socket.t
  | Rw of [ `Read | `Write ] Socket.t

type t = { owner : string; socket : some_socket }

let test = {
  owner = "foo";
  socket = Ro (Socket.ro "bar")
}

let write container = match container.socket with
  | Ro _ -> failwith "write not allowed"
  | Rw s -> Socket.write s

Finally, there is another way to implement the first solution: instead of using a top untyped type, you may allow subtyping of values at type Socket. For this you need to specify, in your interface, the variance of the Socket.t type: is it invariant ('a t), covariant (+'a t) or contravariant (-'a t)?

If your mental model is that a phantom variant type with more cases is "more capable", then subtyping should go from a variant with some cases to a variant with less cases, which is a smaller type: to have a t ≤ b t one should have a ≥ b (a has more cases): t should be contravariant.

module Socket : sig
  type -'a t
  val ro : string -> [ `Read ] t
  val rw : string -> [ `Read | `Write ] t

  val read : [> `Read ] t -> unit
  val write : [> `Write ] t -> unit
end = struct
  type 'a t = string
  let ro s = s
  let rw s = s
  let read _ = ()
  let write _ = ()
end

type t = { owner : string; socket : [ `Read ] Socket.t }

let test = {
  owner = "foo";
  socket = (Socket.rw "bar" :> [ `Read ] Socket.t)
}

Notice the explicit cast (socket :> [ `Read ]) Socket.t to a smaller socket type.