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 tis the universal type and each call to
embedreturns 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
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
type t = exnA module type
ANYis introduced. Modules that implement this signature define an abstract type
cand introduce an
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
let mk : unit → α any = fun (type s) () → (module struct type c = s exception E of c end : ANY with type c = s)This function
unitargument and each invocation computes a new module instance which is packed as a first class value and returned. The locally abstract type
sconnects 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
injand observe how that type ensures a coherence between the module parameter
pand the type of the parameter to be embedded
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
projunpacks the module value parameter into a module named
Anyand then attempts to match
yagainst the constructor defined by
Any. Recall, at the end of the day,
yis of type
exn. The match contains two cases : the first matching the constructor
s, the second anything else (that is,
Finally we come to the public function
let embed () = let p = mk () in inj p, proj p
mkto produce a new embedding
pand 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
# module U = Universal_exn;; # let inj, proj = U.embed ();; val inj : '_a → U.t =Property 1 :
val proj : U.t → '_a option =
embedproduces 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
to_stringare weakly polymorphic.
# let r : U.t ref = ref (of_int 13);;The call to
of_intfixes it's type to
int → U.tand that of
U.t → int option. The types of
# 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_stringincidentally fixed the type of
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;;