User loginNavigation 
Erasure and Polymorphism in Pure Type SystemsErasure and Polymorphism in Pure Type Systems by Nathan MishraLinger and Tim Sheard Abstract
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 typelevel 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 nondependent 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, typelevel computations, dependent types...). They have been mentioned on LtU before: While PTS may also describe nondependent 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 typelevel) and "nonerasable" (or valuelevel) 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 programmingoriented and prooforiented dependentlytyped systems. By gasche at 20101022 21:44  LtU Forum  previous forum topic  next forum topic  other blogs  9144 reads

Browse archivesActive forum topicsNew forum topics

Recent comments
6 hours 55 min ago
16 hours 31 min ago
17 hours 26 min ago
18 hours 51 min ago
1 day 1 hour ago
1 day 4 hours ago
1 day 4 hours ago
2 days 1 hour ago
4 days 3 hours ago
4 days 4 hours ago