First-Class Subtypes

Jeremy Yallop
(University of Cambridge)
Stephen Dolan
(University of Cambridge)

First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in most functional programming languages.

We present several encodings of first-class subtypes using existing features of the OCaml language (made more convenient by the proposed modular implicits extension), show that any such encodings are interconvertible, and illustrate the utility of the encodings with several examples.

In Sam Lindley and Gabriel Scherer: Proceedings ML Family / OCaml Users and Developers workshops (ML 2017), Oxford, UK, 7th September 2017, Electronic Proceedings in Theoretical Computer Science 294, pp. 74–85.
Published: 16th May 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: