Self Types for Dependently Typed Lambda Encodings

摘要

We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type-assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel's implicit product. We add a type construct (ιx.T), called a self type, which allows T to refer to the subject of typing. We show how the resulting System S with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of S is established by defining an erasure from S to a version of F_ω with positive recursive type definitions, which we analyze. We also prove type preservation for S.