Generalized algebraic data types and all that

Опубликовано 7 сентября 2016, 16:25

Generalized algebraic data types (GADTs) extend algebraic data types by a form of type refinement connected to pattern matchings. There are numerous useful examples which exploit this feature such as type-safe evaluators etc. In this talk, I take a closer look at the GADT type inference problem and investigate how to compile GADTs to a typed intermediate language. Specifically, I will explain why type inference for GADTs is such a hard problem and suggest possible solutions to guarantee complete and decidable type inference. I also argue for a combination of GADTs with other type extensions such as type classes. This provides the user with reasoning capabilities which used to be the domain of specialized tools such as logical frameworks and proof assistants.