Module Lrt

Free variable handling

Types with free variables are represented as closures with one ttype argument per free variable. Most APIs, like Print for dynamic printing, consume closed types.

# type 'a tree =
+   | Leave of 'a
+   | Node of 'a tree list
+ [@@deriving t];;
val tree_t : 'a ttype -> 'a tree ttype
# let () = Print.show ~t:(tree_t int_t) (Node [Leave 0; Leave 1]);;
Node [Leave 0; Leave 1]

Stating the types in function application style might be a bit unintuitive. Thus there is an extension point that translates types to applications. Instead of the previous example, you can also write the following.

# let () = Print.show ~t:[%t: int tree] (Node [Leave 0; Leave 1]);;
Node [Leave 0; Leave 1]

Abstract types

We attempt to support abstract types. Whenever you want to hide the actual type definition from the derived ttype, you have to annotate the type declarations with [@@abstract] .

# module M : sig
+   type t [@@deriving t]
+ end = struct
+   type t = int array [@@deriving t]
+ end;;
module M : sig type t val t : t ttype end
# Format.printf "%a\n" Ttype.print M.t;;
int array
# module N : sig
+   type t [@@deriving t]
+ end = struct
+   type t = int array [@@abstract] [@@deriving t]
+ end;;
module N : sig type t val t : t ttype end
# Format.printf "%a\n" Ttype.print M.t;;
//toplevel//.N.t

It is worth to note that abstract types are represented by a string. You can trick the naming mechanism into producing indistinguishable abstract runtime types for distinct OCaml types. You can bypass the name generation by providing a string argument to the abstract annotation.

# type abstract = int [@@abstract "uid"] [@@deriving t];;
val abstract_t : abstract ttype
# Format.printf "%a\n" Ttype.print abstract_t;;
uid

In case you want to expose an abstract ttype, but use a non-abstract version within the module, we recommend to define two types - one non-abstract for internal use and one abstract for satisfying the interface - as outlined below.

# module M : sig
+   type hidden [@@deriving t]
+ end = struct
+   type visible = string list
+   and hidden = visible [@@abstract] [@@deriving t];;
+   (* [visible] represents a string list here. *)
+ end;;

Patching

It happens frequently, that ttypes are not available under the expected name. For such cases, we provide the @patch annotation.

# lazy_t;;
- : 'a ttype -> 'a lazy_t ttype = <fun>
# type 'a lazy_pair = ('a * 'a) Lazy.t [@patch lazy_t] [@@deriving t];;
type 'a lazy_pair = ('a * 'a) lazy_t
val lazy_pair_t : 'a ttype -> 'a lazy_pair ttype = <fun>

When using an external type that has no corresponding ttype we recommend to introduce an abstract alias and use it as replacement.

type external = External.t [@@abstract] [@@deriving t]
type local = (External.t [@patch external_t]) list [@@deriving t]

Properties

Our runtime types support attachments of properties. The behaviour of some APIs can be tweaked by providing certain properties. Properties can be added to core types, record fields and constructors. Keep in mind the binding precedence of annotations.

type sum =
  | A of int [@prop {key1= "binds to constructor A"}]
  | B of (int [@prop {key2= "binds to type int"}])
and record =
  { c : int [@prop {key3= "binds to field c"}]
  ; d : (int [@prop {key4= "binds"; key5="to int"}])
  }
[@@deriving t]

Type representation

Lrt comes with different representations of runtime types. Depending on the application, one might use one or another.

Stype.t or stype in short are an untyped runtime representation of OCaml types. Stypes are easy to construct, serializable and allow to write unsafe but powerful code. Most users want to avoid this interface.

Ttype.t or ttype in short extend the untyped stype with an OCaml type. Ttypes can be built using the [@@deriving t] syntax extension and can be used to safely consume APIs that make use of runtime types.

Xtype.t enable safe inspection of runtime types. Xtypes are used to implement APIs that make use of runtime types.

Unification

The Unify module holds functors that allow to unify an unclosed runtime type with a closed one. This was particularly interesting for implementing the abstract type handling of Print and Variant. It may be that Matcher is strictly more powerful and Unify can be dropped.

Pattern matching

Matcher provides a mechanism for storing data indexed by type using as discrimination tree. The runtime type provided as key during insertion may contain free variables. Data can be retrieved from the store by providing a closed type. During retrieval, the key type is unified with the type used for insertion.

This provides a mechanism similar to OCaml pattern matching but for runtime types.

Type equality

Some of the other modules are able to check for type equality of dynamically crafted types. Such type equalities are inherently out of reach for the OCaml type system. They are "transported back" with help of the TypEq module.

A value of type ('a, 'b) TypEq.t can be interpreted as equality proof for 'a and 'b. OCaml's type system accepts this proof when you open the GADT constructor TypEq.t.Eq. An unwrap may look like the following.

let plus: type a. int -> a -> (a, int) TypEq.t -> int =
 fun a b eq ->
  let TypEq.Eq = eq in
  a + b