A few years back, Stephen wrote a fun post about how to build a so-called “universal type” in OCaml. Such a type allows you to embed any other type within in it, letting you do things like creating ad-hoc lists containing elements of multiple different types.

I’ve been thinking about universal types again because I’ve been working on a project lately that uses a universal type as a central architectural piece. Most ML programmers find the idea of a universal type a little jarring, and so I’ve been thinking about how to present it to make it easy to understand. Perhaps the first thing to consider is what the signature should look like. Here’s what I started with:

module Univ : sig
  module Type : sig
    type 'a t
    val create : unit -> 'a t
  end

  type t
  val embed : 'a Type.t -> 'a -> t
  val project : 'a TYpe.t -> t ->'a option
end

And here’s a simple example of Univ in action.

let int_type = (Univ.Type.create () : int Univ.Type.t)
let string_type = (Univ.Type.create () : string Univ.Type.t)

let mixed_list = [ Univ.embed int_type 3
                 ; Univ.embed string_type "whatever"
                 ; Univ.embed int_type 5 ]

let () =
  assert (List.filter_map ~f:(Univ.project int_type ) mixed_list
         = [3;4]);
  assert (List.filter_map ~f:(Univ.project string_type) mixed_list
         = ["whatever"]);

But there’s something pointlessly confusing about this type. For one thing, the use of the term “type” makes promises that can’t quite be satisfied. For instance, there’s no guarantee that two values of the same type embedded into Univ.t can be reached in the same way. Consider this example.

let int_type = (Univ.Type.create () : int Univ.Type.t)
let int_type' = (Univ.Type.create () : int Univ.Type.t)

let mixed_list = [ Univ.embed int_type 3
                 ; Univ.embed int_type' 4
                 ; Univ.embed int_type 5 ]

let () =
  assert (List.filter_map ~f:(Univ.project int_type) mixed_list
          = [3;4;5]);

WHen I tried to explain what Univ was to people verbally, I described it as a kind of extensible sum type. When Stephen heard me giving this description, he proposed that we change the type signature to reflect this. We ended up with a signature that looks like this:

module Univ : sig
  module Variant : sig
    type 'a t
    val create : unit -> 'a t
  end

  type t
  val create : 'a Variant.t -> 'a -> t
  val match_ : 'a Variant.t -> t -> 'a option
end

The names now point you in the right direction: every time you call Variant.create, you’re creating a new arm of this extensible sum type. There’s no guarantee that two variants won’t be created with the same type, and there’s no need for such a guarantee.

We also changed the embed and project to create and match_, to better track the terminology used in the rest of the language for constructing and deconstructing sum types.

Along the way, we made one other change to Univ, which was to add some default functionality to each variant. In particular, the ability to figure out the name of any variant within the Univ type, and the ability to serialize a Univ.t to an s-expression. This is useful for dynamically browsing a collection of Univ.t values at run-time. The final interface looks like this:

module Univ : sig
  module Variant : sig
    type 'a t
    (** [create variant_name to_sexp] creates a new variant with the
      given name and serializer *)
    val create : string -> ('a -> Sexp.t) -> 'a t
  end

  type t
  val create : 'a Variant.t -> 'a -> t
  val match_ : 'a Variant.t -> t -> 'a option

  val to_sexp : t -> Sexp.t
  val variant_name : t -> string
end

The other thing that struck me about this is that when I first heard about it, the idea of Univ seemed interesting but mostly a curiousity – I just didn’t have any applications for it in mind.

But just because an idea isn’t useful right now, doesn’t mean it’s not going to become useful later.