The gentle art of levitation

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

doi:10.1145/1863543.1863547

The gentle art of levitation

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

39 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 language	English
Title of host publication	ICFP 2010 Proceedings of the 15th ACM SIGPLAN international conference on functional programming
Editors	Paul Hudak
Place of Publication	New York
Pages	3-14
Number of pages	12
DOIs	https://doi.org/10.1145/1863543.1863547
Publication status	Published - 2010
Event	ICFP 2010 - Baltimore, United States Duration: 27 Sept 2010 → …

Conference

Conference	ICFP 2010
Country/Territory	United States
City	Baltimore
Period	27/09/10 → …

Keywords

programming
dependent type theory
datatype-generic programming

Access to Document

10.1145/1863543.1863547

Reusability and Dependent Types
Ghani, N. (Principal Investigator) & McBride, C. (Co-investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/10/09 → 30/09/13
Project: Research

Cite this

@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",

note = "ICFP 2010 ; Conference date: 27-09-2010",

}

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

T2 - ICFP 2010

Y2 - 27 September 2010

ER -

The gentle art of levitation

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Reusability and Dependent Types

Cite this