The gentle art of levitation

James Chapman, Pierre-Evariste Dagand, Conor Mcbride, Peter Morris

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

20 Citations (Scopus)

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 regress.
Original languageEnglish
Title of host publicationICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming
EditorsPaul Hudak
Place of PublicationNew York
Pages3-14
Number of pages12
DOIs
Publication statusPublished - 2010
EventICFP 2010 - Baltimore, United States
Duration: 27 Sep 2010 → …

Conference

ConferenceICFP 2010
CountryUnited States
CityBaltimore
Period27/09/10 → …

Keywords

  • programming
  • dependent type theory
  • datatype-generic programming

Cite this

Chapman, J., Dagand, P-E., Mcbride, C., & Morris, P. (2010). The gentle art of levitation. In P. Hudak (Ed.), ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming (pp. 3-14). New York. https://doi.org/10.1145/1863543.1863547
Chapman, James ; Dagand, Pierre-Evariste ; Mcbride, Conor ; Morris, Peter. / The gentle art of levitation. ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. editor / Paul Hudak. New York, 2010. pp. 3-14
@inproceedings{3f0bd5e89f14489bbda3dd8d470efbe1,
title = "The gentle art of levitation",
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 regress.",
keywords = "programming, dependent type theory , datatype-generic programming",
author = "James Chapman and Pierre-Evariste Dagand and Conor Mcbride and Peter Morris",
year = "2010",
doi = "10.1145/1863543.1863547",
language = "English",
isbn = "9781605587943",
pages = "3--14",
editor = "Paul Hudak",
booktitle = "ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming",

}

Chapman, J, Dagand, P-E, Mcbride, C & Morris, P 2010, The gentle art of levitation. in P Hudak (ed.), ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. New York, pp. 3-14, ICFP 2010, Baltimore, United States, 27/09/10. https://doi.org/10.1145/1863543.1863547

The gentle art of levitation. / Chapman, James; Dagand, Pierre-Evariste; Mcbride, Conor; Morris, Peter.

ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. ed. / Paul Hudak. New York, 2010. p. 3-14.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - The gentle art of levitation

AU - Chapman, James

AU - Dagand, Pierre-Evariste

AU - Mcbride, Conor

AU - Morris, Peter

PY - 2010

Y1 - 2010

N2 - 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 regress.

AB - 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 regress.

KW - programming

KW - dependent type theory

KW - datatype-generic programming

U2 - 10.1145/1863543.1863547

DO - 10.1145/1863543.1863547

M3 - Conference contribution book

SN - 9781605587943

SP - 3

EP - 14

BT - ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming

A2 - Hudak, Paul

CY - New York

ER -

Chapman J, Dagand P-E, Mcbride C, Morris P. The gentle art of levitation. In Hudak P, editor, ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming. New York. 2010. p. 3-14 https://doi.org/10.1145/1863543.1863547