An implementation of Conor McBride’s crude but effective stratification. Our POPL 2023 paper “An Order-Theoretic Analysis of Universe Polymorphism” explained the theory behind our design.
⚠ The API is experimental and unstable. We will break things!
- Mugen.Shift: example displacement algebras
- Mugen.ShiftWithJoin: example displacement algebras with joins
- Mugen.Syntax: syntax of universe levels
- Mugen.Semantics: smart builders and comparators
- The distinguished level variable for top-level definitions should be explicit in the core language for clean semantics. (It can remain implicit in the surface language.)
- One-variable universe polymorphism with cumulativity is enough. Typical ambiguity (as in Coq) and multi-variable universe polymorphism (as in Agda) are overkill.
- It is convenient to have the top level for type checking. However, end users should not be allowed to write the top level, and shifting the top level is forbidden.
In Conor McBride’s notes, it was noted that any class of strictly monotone operators on levels closed under identity and composition will work. We codified such a class as a displacement algebra. The classic displacement operators may be recovered by using the following module with non-negative numbers:
You need OCaml 4.13 or later. Here is the fastest way to install the library with OPAM 2.1:
opam pin mugen git+https://github.com/RedPRL/mugenmodule I = Mugen.Shift.Int
module M = Mugen.Syntax
(* The type of universe levels, using integers as displacements and strings as variable names. *)
type ulevel = (I.t, string) M.free
(* The level representing "x + 10" *)
let l : ulevel = M.Free.(shifted (var "x") (I.of_int 10))