Abstract

Algebraic datatypes have fundamental roles in functional programming, which are often treated as primitive types in languages including Haskell and Coq. Primitive datatypes complicate the type theory but are necessary because induction principle is difficult to encode in pure lambda terms. One recent approach to enable inductive data with pure lambdas is called “self type”. In this talk, we first revisit classic lambda encodings introduced in previous talks and then show the mechanism and properties of self type.