A universal type?

It is amazing to see you financial people do such theory! I am delighted. This exercise has connection to realizability toposes. I have three remarks.

First, if projection can map into 'a option then it can map into 'a because every type is inhabited, say by a diverging term. So you do not really need the option type. But it is probably better to do it that way, if you can, because returning None is friendlier than diverging.

Second, how is this supposed to play with diverging terms? Are we embedding terms or values? Presumably values. Since Ocaml is call-by-value it might be hard to embed terms that denote diverging values.

Third, what does it mean that injection followed by projection is the identity when we embed higher-order types, such as (int->int)->int? In your example above you indicate how it is supposed to work with int and string. Can you give us an example of how it is supposed to work with a function type, where comparison = does not work?

I got a plain solution which passed the given tests, but I wouldn't consider it universal, as in my solution an an 'a type value encoded by an 'a type encoder can't be decoded by any other 'a type decoders except the one coming from the same pair. Could you confirm that? or could you give the expected behavior of the following code?

let (of_int, to_int) = U.embed ()
let e = of_int 1 
let (of_int', to_int') = U.embed ()
let e' = of_int' 1
assert (to_int e' = Some 1);
assert (to_int' e = Some 1);

I am not going to answer, because it would ruin the fun for others. Actually, Stephen was the first to tell me about this little neat trick. Having a universal type turns out to be pretty powerful. You can easily build a type Univ.t list and then you can store arbitrarily typed data into that list.

The consequence is a type safe property list working for any type. When you get the hang of these, many of the usual tricks from dynamically typed languages become possible. But in a type-safe way! The option type on the projection will protect you.

However, I better not ruin Stephens later blog posts. There is more juice to be squeezed from this lemon.

Here is my implementation of Univ. It is very similar to Alain's using the hidden ref cell, except it uses a unique id per embedding and only stores and clears the ref cell if it knows it will succeed.

module Univ : Univ = struct
  type t = { 
    id : unit ref;
    store : unit -> unit; 
  }
 
  let embed () = 
    let id = ref () in
    let r = ref None in
    let put a =
      let o = Some a in
      { id = id; store = (fun () -> r := o); }
    in
    let get t =
      if id == t.id then (t.store (); let a = !r in r := None; a) else None
    in
    (put, get)
end

The tradeoff between this and Alain's solution is that this one allocates an extra tuple per injection, but does fewer tests per projection, and doesn't store if the projection returns None (Alain's solution does two stores in either case.

Another possible difference might be thread safety. In either solution, once can use a single mutex for the entire module to make the mutation thread safe. However, I think my solution may be easier to extend using a mutex per embedding, which would have less contention. The idea is to wrap t.store (); let a = !r in r := None; in a critical section that holds the per-embedding mutex. For my solution, the single mutex suffices because we know that t.store () and r := None deal with the same ref cell. For Alain's solution, one would need to lock the mutex for both embeddings (which could deadlock), at which point one might as well just test whether one has the right embedding, leading naturally back to my solution. Alain, what do you think?

I am not aware of any other way to implement the Univ signature in OCaml (including using polymorphic variants and exceptions), but would be happy to see one. It is possible to implement Univ in SML using exceptions, but unfortunately not in OCaml because it doesn't have local exception declarations. One could use exceptions in OCaml to implement a functor that has a similar flavor to Univ, but as far as I know, it is not possible to meet the Univ signature. One nice thing about using exceptions (in either language) is that one gets thread safety automatically since no references are used.

Here is another solution:

module U : Univ = struct
  type t = exn
 
  let embed () =
    let new type s in
    let module M = struct exception E of s end in
    (fun x -> M.E x), (function M.E x -> Some x | _ -> None)
end 

It relies on the "let new type t in e" construction developed at LexiFi, that I've mentioned somewhere else on this blog. This new construction should appear in a later official version of OCaml.

This solution is thread-safe and it should be quite efficient. One can of course move the allocation from the projection function into the injection function by declaring "exception E of s option".

The construction "let new type t in e" creates a new abstract type "t" visible in the scope of the sub-expression "e". If this sub-expression "e" is well-typed and the type "t" does not escape to the environment, then the type for "let new type t in e" is obtained from the type for "e" by replacing "t" by a fresh type variable.