Home

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.
By Andris Birkmanis at 2018-05-11 19:26 | Semantics | Type Theory | other blogs | 25865 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Turtles

I call it the "turtle type system" (i.e. it's turtles the whole way down). I hadn't realized that anyone else had attempted this approach; thanks for the link. It's not as easy to boot-strap, but once the wheels are up, you can't ever imagine touching back down ....

By cpurdy at Tue, 2018-05-15 01:41 | login or register to post comments