Quickstart Tutorial

This tutorial is for an implementer (you!) to integrate this library into your type theory implementation as quickly as possible. We will assume you are already familiar with OCaml and dependent type theory, and are using a typical OCaml package structure.

Introduction

Following Conor McBride’s crude but effective stratification and our algebraic reformulation, a universe level in this library is represented as a pair of a variable together with some displacement. For example, a universe level might be x + 10, meaning the variable level x shifted (bumped) by 10 levels. The shifting of 10 levels is the displacement. For the same variable x, the level x + n is larger than x + m if n is larger than m, while levels x + n and y + m are in general incomparable for different variables x and y. Substituting x + n1 for y in y + n2 results in the level x + (n1 + n2).

While this scheme (with only a variable and some displacement) looks limited, we proved that it is in a sense universal if you allow all mathematically possible displacements beyond natural numbers. We also call the minimum algebra of displacements that would make the scheme work a displacement algebra. See our POPL paper for more details.

This library implements several displacement algebras you could choose from, along with a uniform interface to construct and compare universe levels.

Choose Your Displacements

The first step is to choose your favorite displacements. We will use Mugen.Shift.Int (integers) as the starting point, and it is easy to switch to another displacement algebra later. Other displacements are under Mugen.Shift and Mugen.ShiftWithJoin.

Free Level Expressions

Free level expressions are expressions freely generated by only variables and shifting operators. In contrast, we will have a different kind of level expressions embedded in your datatype holding terms or types. The free level expressions are the only ones that can be compared against each other; the embedded ones must be converted to free ones for comparison. More on this point later.

Save the following content as the file ULvl.ml for free level expressions, assuming that you are using integers to represent variables.

module Param =
struct
  (** Your chosen displacement algebra *)
  module Shift = Mugen.Shift.Int

  (** The representation of variables in free level expressions *)
  type var = int

  (** The equality checker for variables *)
  let equal_var : var -> var -> bool = Int.equal
end
include Param

(** An alias of the type of displacements *)
type shift = Shift.t

(** An alias of the type of free level expressions *)
type t = (shift, int) Mugen.Syntax.free

(** Smart constructors for free level expressions *)
include Mugen.Builder.Free.Make (Param)

(** Comparators for free level expressions *)
include Mugen.Theory.Make (Param)

Take a look at Mugen.Syntax.free for the definition of free level expressions.

Extend Your Syntax

Now we have the free level expressions ready, you need to extend your datatype to embed levels and define the conversion functions to free ones. A typical datatype holding terms or types will have the following pattern:

type t =
  | Var of int (* maybe using De Bruijn indexes or levels *)
  (* ... more syntax follows ... *)

There are three steps to add level expressions to your datatype

Change the Datatype

The idea is to use Mugen.Syntax.endo, instead of Mugen.Syntax.free, so that displacements can syntactically apply to any term or type in your language (but most of them will be ill-formed terms or types). The first parameter of Mugen.Syntax.endo is the type of displacements, and the second parameter is your datatype. It needs to be defined together with your datatype due to the mutual recursion; in the following example, we choose to add a new constructor, ULvl, to embed level expressions:

(** Use [endo] to embed levels into your datatype. *)
type ulvl = (ULvl.shift, t) Mugen.Syntax.endo

(** The datatype of terms. *)
and t =
  | Var of int
  (* ... more syntax follows ... *)
  | ULvl of ulvl

You can take a look at Mugen.Syntax.endo for the definition of embedded level expressions.

Add Converters

(** Conversion to free level expressions *)
let rec to_ulvl : t -> ULvl.t =
  function
  | Var i -> Mugen.Syntax.Var i
  | ULvl endo -> endo_to_ulvl endo
  | _ -> invalid_arg "to_ulvl"

and endo_to_ulvl : ulvl -> ULvl.t =
  let module M = Mugen.Syntax in
  function
  | M.Shifted (l, s) -> ULvl.shifted (to_ulvl l) s
  | M.Top -> ULvl.top

Add Smart Constructors

Comparing Levels

The most common tasks are to compare two embedded levels. The code is straightforward---the ULvl module you have created comes with comparators for free level expressions. It is sufficient to convert embedded level expressions to free ones and compare them accordingly. Copy and paste the following code snippet after the definition of your datatype:

(** Conversion to free level expressions *)
let rec to_ulvl : t -> ULvl.t =
  function
  | Var i -> Mugen.Syntax.Var i
  | ULvl endo -> endo_to_ulvl endo
  | _ -> invalid_arg "to_ulvl"

and endo_to_ulvl : ulvl -> ULvl.t =
  let module M = Mugen.Syntax in
  function
  | M.Shifted (l, s) -> ULvl.shifted (to_ulvl l) s
  | M.Top -> ULvl.top

Now, the comparators for embedded level expressions can be defined as followed:

let equal_ulvl l1 l2 = ULvl.equal (to_ulvl l1) (to_ulvl l2)
let leq_ulvl l1 l2 = ULvl.leq (to_ulvl l1) (to_ulvl l2)
let lt_ulvl l1 l2 = ULvl.lt (to_ulvl l1) (to_ulvl l2)

You might have noticed that there is a "top" level---we added the top level for convenience.

Building Levels

Another common task in a real system is to parse user inputs and construct corresponding (embedded) level expressions. The recommended approach is to use smart constructors that will consolidate displacements when building level expressions. To do so, these smart constructors need to know how to check whether an expression in your datatype is a level expression. Here is the snippet to copy and paste to summon smart constructors:

(** Include smart constructors for universe levels *)
include
  Mugen.Builder.Endo.Make
    (struct
      (** Your chosen displacement algebra *)
      module Shift = ULvl.Shift

      (** The type of embedded level expressions *)
      type level = t

      (** A function to embed a level expression *)
      let level (l : ulvl) : t = ULvl l

      (** A function to check whether an expression is an embedded level expression *)
      let unlevel : t -> ulvl option = function ULvl l -> Some l | _ -> None
    end)

See Remember that you have included the smart constructors in previous steps.

The essential one

let _ = shifted l s

to obtain the level l shifted by the displacement s. Constructing the displacement s depends on your chosen displacement algebra. If you were using integers, aliasing the stock Mugen.Shift.Int as ULvl.Shift), then the shifting by 10 levels can be implemented as:

let _ = shifted l (ULvl.Shift.of_int 10)

For convenience, we also introduced the top level

let _ = top

that will be greater than any other level. (Note that you cannot shift the distinguished top level!)

Concluding Notes

That's it! Now you have rich universe levels. Here are a few remarks:

Ugly Printers for Debugging

It is recommended to write your own pretty printer. However, if you wish to dump the universe levels, check out Mugen.Syntax.Free.dump for free level expressions and Mugen.Syntax.Endo.dump for embedded ones.

Changing the Displacement Algebra

It is trivial to switch to another displacement algebra by aliasing ULvl.Shift to another module implementing the interface Mugen.Shift.S. Changing the displacement algebra only affects how displacements are constructed and printed.