System Fi: A higher-order polymorphic λ-calculus with erasable term-indices

Abstract

We introduce a foundational lambda calculus, System Fi, for studying programming languages with term-indexed datatypes - higher-kinded datatypes whose indices range over data such as natural numbers or lists. System Fi is an extension of System Fω that introduces the minimal features needed to support term-indexing. We show that System F i provides a theory for analysing programs with term-indexed types and also argue that it constitutes a basis for the design of logically-sound light-weight dependent programming languages. We establish erasure properties of Fi-types that capture the idea that term-indices are discardable in that they are irrelevant for computation. Index erasure projects typing in System Fi to typing in System Fω. So, System F i inherits strong normalization and logical consistency from System Fω. © 2013 Springer-Verlag.