## Universal type

A universal type is a type into which all other types can be embedded. A module implementing such a type here will satisfy the following signature.

module type UNIVERSAL = sig type t val embed : unit → (α → t) * (t → α option) end;;The

`type t`

is the universal type and each call
to `embed`

returns a pair of functions : an injection
function for embedding a value into the universal type and, a
projection function for extracting the value from its embedding
in the universal type. The following code demonstrates intended
usage.
module type TEST = sig val run : unit → unit end;; module type UNIVERSAL_TEST = functor (U : UNIVERSAL) → TEST;; module Basic_usage : UNIVERSAL_TEST = functor (U : UNIVERSAL) → struct let run () = let ((of_int : int → U.t) , (to_int : U.t → int option)) = U.embed () in let ((of_string : string → U.t) , (to_string : U.t → string option)) = U.embed () in let r : U.t ref = ref (of_int 13) in begin assert (to_int !r = Some 13); assert (to_string !r = None); r := of_string "foo"; assert (to_string !r = Some "foo"); assert (to_int !r = None); end end;;

One possible implementation is via the use of exceptions
together with local modules. The core idea exploits the fact that
the primitive type `exn`

is an open extensible
sum. Here's the complete implementation. We'll break it down
later.

module Universal_exn : UNIVERSAL = struct type t = exn module type ANY = sig type c exception E of c end type α any = (module ANY with type c = α) let mk : unit → α any = fun (type s) () → (module struct type c = s exception E of c end : ANY with type c = s) let inj (type s) (p : s any) (x : s) : t = let module Any = (val p : ANY with type c = s) in Any.E x let proj (type s) (p : s any) (y : t) : s option = let module Any = (val p : ANY with type c = s) in match y with | Any.E x → Some x | _ as e → None let embed () = let p = mk () in inj p, proj p end;;Before delving into an explanation of the program, one can verify it satisfies the basic test.

# module Test_basic = Mk_universal_test(Universal_exn);; # Test_basic.run ();; - : unit = ()

The definition of the universal type `t`

is an alias
to the predefined type `exn`

.

type t = exnA module type

`ANY`

is introduced. Modules that
implement this signature define an abstract type `c`

and
introduce an `exn`

constructor `E of c`

.
module type ANY = sig type c exception E of c endAn alias for the type of a module value satisfying this signature comes next. Using aliases of this kind are helpful in reducing "syntactic verbosity" in code accepting and returning module values.

type α any = (module ANY with type c = α)Next follow a set of functions that are private to the implementation of the module. The first of these is

`mk`

.
let mk : unit → α any = fun (type s) () → (module struct type c = s exception E of c end : ANY with type c = s)This function

`mk`

takes the `unit`

argument
and each invocation computes a new module instance which is packed
as a first class value and returned. The locally abstract
type `s`

connects to the `α`

in the
return type.
The next function to be defined is `inj`

which computes
a universal type value from its argument.

let inj (type s) (p : s any) (x : s) : t = let module Any = (val p : ANY with type c = s) in Any.E xAs was the case for

`mk`

, a locally abstract type is
used in the definition of `inj`

and observe how that
type ensures a coherence between the module
parameter `p`

and the type of the parameter to be
embedded `x`

.
The projection function `proj`

comes next and also uses
a locally abstract type ensuring coherence among its parameters.

let proj (type s) (p : s any) (y : t) : s option = let module Any = (val p : ANY with type c = s) in match y with | Any.E x → Some x | _ as e → NoneThe body of

`proj`

unpacks the module value parameter into
a module named `Any`

and then attempts to
match `y`

against the constructor defined
by `Any`

. Recall, at the end of the day, `y`

is of type `exn`

. The match contains two cases : the
first matching the constructor `Any.E x`

with `x`

having type `s`

, the second anything
else (that is, `proj`

is total).
Finally we come to the public function `embed`

.

let embed () = let p = mk () in inj p, proj p

`embed`

calls `mk`

to produce a new
embedding `p`

and returns the pair of partial
applications `(inj p, proj p)`

.
Our examination of the implementation is concluded. There are
however various implications of the implementation we are now in a
position to understand that are not immediately obvious from the
specification. As a first example, consider the inferred type of a
call to `embed`

.

# module U = Universal_exn;; # let inj, proj = U.embed ();; val inj : '_a → U.t =val proj : U.t → '_a option =

**Property 1 :**

`embed`

produces weakly polymorphic
functions.
Consider the following scenario:

# let of_int, to_int = U.embed ();; # let of_string, to_string = U.embed ();;At this point all of

`of_int`

, `to_int`

, `of_string`

and `to_string`

are weakly polymorphic.
# let r : U.t ref = ref (of_int 13);;The call to

`of_int`

fixes it's type to ```
int →
U.t
```

and that of `to_int`

to ```
U.t → int
option
```

. The types of `of_string`

and `to_string`

remain unfixed.
# to_string !r = Some 13;; - : bool = falseThe programmer has mistakenly used a projection function from a different embedding.

# r := of_string "foo";; Error: This expression has type string but an expression was expected of type intThe erroneous usage of

`to_string`

incidentally fixed
the type of `of_string`

to `int → U.t`

! One
can imagine errors of this kind being difficult to diagnose.
**Property 2 :** Injection/projection functions of different
embeddings may not be mixed.

# let ((of_int : int → U.t), (to_int : U.t → int option)) = U.embed ();; # let ((of_int' : int → U.t), (to_int' : U.t → int option)) = U.embed ();;Two embeddings have been created, the programmer has fixed the types of the injection/projection functions

*a priori*(presumably as a defense against the problems of the preceding example).

# let r : U.t ref = ref (of_int 13);; # to_int !r = Some 13;; - : bool = trueThe first embedding is used to inject an integer. That integer can be extracted using the projection function of that embedding.

# to_int' !r = Some 13;; - : bool = falseWe cannot extract the integer from the universal type value using the projection function from the other embedding despite all of the types involved being the same. One can imagine that also as being quite the source of bugs and confusion to the unknowing programmer.

The constraint of property 2 is beyond the ability of the type system to enforce. About the best one can do is to enhance the specification of the type with documentation.

module type UNIV = sig type t val embed : unit → (α → t) * (t → α option) (* A pair [(inj, proj)] returned by [embed] works together in that [proj u] will return [Some v] if and only if [u] was created by [inj v]. If [u] was created by a different function then [proj u] will return [None]. *) end;;