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  6715 reads

Browse archivesActive forum topics 
Recent comments
3 hours 42 min ago
7 hours 7 min ago
7 hours 19 min ago
8 hours 16 min ago
8 hours 43 min ago
8 hours 55 min ago
9 hours 10 min ago
9 hours 14 min ago
13 hours 46 min ago
13 hours 57 min ago