Abstract

Since the dawn of time, typed functional languages have assumed that type constructors are total. That is, if I have a `List a`, we understand that to mean that I can have lists of any type I can imagine. However, what if I want a partial type constructor? For example, if I have a datatype that describes binary search trees, that type makes sense only with elements that have an ordering. Or maybe I have a type that has an optimized representation, but only for certain types like Int and Float. Many other examples are out there! This talk will present a design for a type system that supports partial type constructors, realized through constraints, much like how Haskell supports ad-hoc polymorphism through constraints. Our approach simplifies code that works over partial types and allows better static detection of non-sensical types. This work has been conditionally accepted to be presented at POPL 2020 .