The gentle art of levitation
- 27 September 2010
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 45 (9), 3-14
- https://doi.org/10.1145/1863543.1863547
Abstract
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. Simulations in existing systems suggest that this apparently self-supporting setup is achievable without paradox or infinite regressKeywords
This publication has 22 references indexed in Scilit:
- Generic programming with fixed points for mutually recursive datatypesPublished by Association for Computing Machinery (ACM) ,2009
- A UNIVERSE OF STRICTLY POSITIVE FAMILIESInternational Journal of Foundations of Computer Science, 2009
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof IrrelevanceLecture Notes in Computer Science, 2009
- Observational equality, now!Published by Association for Computing Machinery (ACM) ,2007
- Generic Views on Data TypesLecture Notes in Computer Science, 2006
- Exploring the Regular Tree TypesLecture Notes in Computer Science, 2006
- Pure type systems with judgemental equalityJournal of Functional Programming, 2005
- The view from the leftJournal of Functional Programming, 2004
- Scrap your boilerplatePublished by Association for Computing Machinery (ACM) ,2003
- An algorithm for type-checking dependent typesScience of Computer Programming, 1996