First-Class Subtypes

Jeremy Yallop, Stephen Dolan

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 relat…