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
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
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.