# First-Class Subtypes

## TL;DR

This paper explores how to encode first-class subtypes in OCaml using existing features and modular implicits, demonstrating their equivalence and practical utility through various examples.

## Contribution

It introduces multiple encodings of first-class subtypes in OCaml, showing their interconvertibility and practical applications, advancing type relation representations in functional languages.

## Key findings

- Multiple encodings of first-class subtypes are interconvertible.
- Encodings are practical and useful in real OCaml programs.
- Modular implicits facilitate more convenient subtype representations.

## Abstract

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.