Lambda the Ultimate

Erasure and Polymorphism in Pure Type Systems by Nathan Mishra-Linger and Tim Sheard

Abstract

We introduce Erasure Pure Type Systems, an extension to Pure Type Systems with an erasure semantics centered around a type constructor ∀ indicating parametric polymorphism. The erasure phase is guided by lightweight program annotations. The typing rules guarantee that well-typed programs obey a phase distinction between erasable (compile-time) and non-erasable (run-time) terms.

The erasability of an expression depends only on how its value is used in the rest of the program. Despite this simple observation, most languages treat erasability as an intrinsic property of expressions, leading to code duplication problems. Our approach overcomes this deficiency by treating erasability extrinsically.

Because the execution model of EPTS generalizes the familiar notions of type erasure and parametric polymorphism, we believe functional programmers will find it quite natural to program in such a setting.

This paper is a shorter presentation of some of the ideas of Nathan Linger PhD thesis. The general idea is that, in a dependent type systems, erasable terms are not defined intrisically (by their type or another classification), but by how they are used in the program. Functions are classified by two type-level constructs, one meaning that the function argument is used during runtime computation, and the other meaning that the parameter is computationnaly irrelevant (it only appears in type annotations, proof term, etc.). A very nice idea is that parametric polymorphism and erasability (type erasure, proof irrelevance...) may actually be the same thing.

Being more familiar with non-dependent systems (ML, System F), I'm interested in "type erasure semantics", but find it very nice that insights can be gained by looking at dependent sytems.

.

Background

Pure type systems are a generalization of the Lambda Cube, parametrized by arbitrary dependency between sorts (type polymorphism, type-level computations, dependent types...). They have been mentioned on LtU before:

• Lambda Cube and programming languages
• Examples of encodings in Pure Type Systems

While PTS may also describe non-dependent type systems, the problematic handled in this paper are mostly familiar to dependent type systems. Those have been discussed numerous times on LtU, among them, in chronological order:

• Why Dependent Types Matter
• Dependent types: literature, implementations and limitations ? with a nice Curry-Howard-style introduction by neelk
• Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus) with a discussion of the strong link between dependent types and total (non Turing-complete) functional languages
• Summary of Dependently Typed Systems? discusses the "practical" tools available today (Coq, Agda, Epigram, ATS...) for proving and programming in dependently-typed systems

Other approaches try to access to some of the power of dependent types without adding them in their full complexity. The programming language Ωmega, also by Tim Sheard, has been mentioned recently.

A nice thing about the erasure treatment in Nathan Linger's paper is that it avoids the duplication between different families of "erasable" (or type-level) and "non-erasable" (or value-level) terms, such as can be observed in Coq between Set and Prop, or between the different kind layers of Ωmega. I think this is a promising idea, both for programming-oriented and proof-oriented dependently-typed systems.