Types as first class citizens in OCaml

Yes, you can do this, and various solutions are already provided by different libraries, e.g., Janestreet’s Univ module from the Core Kernel library. Usually, it is called Universal values, but in fact, these are dynamically typed values, implemented with GADT+Extensible Variants+First class modules.

Basically, the representation of a value is a packed existential:

type univ = Pack : 'a witness * 'a -> univ

where the witness is an extensible GADT type

type 'a witness = ..

Runtime types are represented as first class modules, of the following type:

module type Witness = sig 
     type t 
     type _ witness += Id : t witness
end

type 'a typeid = (module Witness with type t = 'a)

New types are created on fly:

let newtype (type u) () = 
   let module Witness = struct 
          type t = u
          type _ witness += Id : t witness
      end in
   (module Witness : Witness with type t = u)

For example,

let int : int typeid = newtype ()

Having the runtime type we can provide the pack function:

let pack (type u) (module Witness : Witness with type t = u) x = 
  Pack (Witness.Id,x)

E.g.,

let x : univ = pack int 42

and the unpack function:

let unpack (type u) 
   (module Witness : Witness with type t = u) (Pack (id,x)) : u option = 
   match id with
   | Witness.Id -> Some x
   | _ -> None

E.g.,

 unpack int x;;
- : int option = Some 42

So this gives you fully working dynamic typing in OCaml. You can also provide dictionaries and other specialized data structures. You may also provide adhoc polymorphism by requiring/allowing registering implementations for types, i.e., you may ask a user to provide the t -> string function, and then provide a generic show : univ -> string function.

The main drawback of this solution, is serialization. The default marshal module won’t work, as it will loose (correctly) the type witness. A possible solution is to use something else (e.g. UUID) for type witnessing when a global witness is required (e.g., distwit library).

34 Likes