User loginNavigation |
The Gentle Art of Levitation
The Gentle Art of Levitation
2010 by James Chapman, Pierre-Evariste Dagand, Conor McBride, Peter Morrisy We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe. Each inductive datatype arises by interpreting its description—a first-class value in a datatype of descriptions. Moreover, the latter itself has a description. Datatype-generic programming thus becomes ordinary programming. We show some of the resulting generic operations and deploy them in particular, useful ways on the datatype of datatype descriptions itself. Surprisingly this apparently self-supporting setup is achievable without paradox or infinite regress.It's datatype descriptions all the way down. |
Browse archives
Active forum topics |
Recent comments
1 week 4 days ago
3 weeks 6 days ago
13 weeks 1 day ago
13 weeks 3 days ago
13 weeks 4 days ago
20 weeks 4 days ago
26 weeks 2 days ago
26 weeks 3 days ago
27 weeks 2 days ago
30 weeks 23 hours ago