Subtypes: first-class subtypes for OCaml

This package provides first-class subtypes for OCaml, analogous to Generalized Algebraic Data Types (GADTs).

GADTS support first-class type equality witnesses, so that a value (a, b) Type.eq is a run-time warrant that a and b are equal.

Analogously, this package supports first-class subtyping witnesses, so that a value (a, b) Subtype.t is a run-time warrant that a is a subtype of b.

The following paper describes the implementation of first-class subtypes, along with a number of motivating examples, including covariant lazy values, iterations over arrays of elements of distinct types, and proofs of variance:

            First-Class Subtypes (pdf)
            Jeremy Yallop and Stephen Dolan
            ML/OCaml 2017

Installation

The implementation depends on the experimental modular implicits extension to OCaml. The modified compiler and this library can be installed as follows:

opam switch 4.02.1+modular-implicits
opam pin add subtypes https://github.com/yallop/subtypes.git

Examples

The tests directory has a number of examples.