Algebraic Subtyping for Ouroboro
Assigned to Justus Springer.
Algebraic subtyping is a new approach which unifies parametric polymorphism, subtyping and complete type inference with principal types. The presentations used in the literature illustrate the approach by considering systems with function types, record types and base types, since these form a minimal type theory which allows to illustrate contravariance (function types) and subtyping (record types).
Algebraic subtyping is a very natural fit for a system which only contains extensible data and codata types, since these subsume function types, record types, ordinary data types and many more.
The thesis consists in applying and extending the algebraic subtyping approach to a structural version of the Ouroboro type theory.
Further Information
- Stephen Dolan, Algebraic Subtyping (PhD Thesis)
- Stephen Dolan, Alan Mycroft, Polymorphism, Subtyping and Type Inference in MLsub
- Polymorphism, Subtyping and Type Inference in MLsub, POPL2017 Presentation (Youtube)
- Lionel Parreaux, The Simple Essence of Algebraic Subtyping (Functional Pearl)
- Lionel Parreaux, The Simple Essence of Algebraic Subtyping (Scala Code)