Erasure and Polymorphism in Pure Type Systems
Erasure and Polymorphism in Pure Type Systems by Nathan Mishra-Linger and Tim Sheard
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.
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:
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:
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.
Active forum topics
New forum topics