Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation

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

16 Citations (Scopus)

Abstract

Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article constructs a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur - it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.
LanguageEnglish
Title of host publicationProceedings of the 6th ACM SIGPLAN workshop on Generic programming
Place of PublicationNew York
Pages1-12
Number of pages12
DOIs
Publication statusPublished - 2010
EventWGP 2010 - Baltimore, United States
Duration: 26 Sep 201026 Sep 2010

Conference

ConferenceWGP 2010
CountryUnited States
CityBaltimore
Period26/09/1026/09/10

Keywords

  • programming techniques
  • applicative programming
  • functional programming
  • design
  • languages
  • theory

Cite this

Mcbride, C. (2010). Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN workshop on Generic programming (pp. 1-12). New York. https://doi.org/10.1145/1863495.1863497
Mcbride, Conor. / Outrageous but meaningful coincidences : dependent type-safe syntax and evaluation. Proceedings of the 6th ACM SIGPLAN workshop on Generic programming . New York, 2010. pp. 1-12
@inproceedings{a0abca2295924243b762d7e92c2e699d,
title = "Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation",
abstract = "Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article constructs a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur - it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.",
keywords = "programming techniques, applicative programming, functional programming, design , languages, theory",
author = "Conor Mcbride",
year = "2010",
doi = "10.1145/1863495.1863497",
language = "English",
isbn = "9781450302517",
pages = "1--12",
booktitle = "Proceedings of the 6th ACM SIGPLAN workshop on Generic programming",

}

Mcbride, C 2010, Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. in Proceedings of the 6th ACM SIGPLAN workshop on Generic programming . New York, pp. 1-12, WGP 2010, Baltimore, United States, 26/09/10. https://doi.org/10.1145/1863495.1863497

Outrageous but meaningful coincidences : dependent type-safe syntax and evaluation. / Mcbride, Conor.

Proceedings of the 6th ACM SIGPLAN workshop on Generic programming . New York, 2010. p. 1-12.

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

TY - GEN

T1 - Outrageous but meaningful coincidences

T2 - dependent type-safe syntax and evaluation

AU - Mcbride, Conor

PY - 2010

Y1 - 2010

N2 - Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article constructs a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur - it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.

AB - Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article constructs a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The KIPLING interpreter example is not merely de rigeur - it is key to the construction. At the heart of the technique is that key component of generic programming, the universe.

KW - programming techniques

KW - applicative programming

KW - functional programming

KW - design

KW - languages

KW - theory

U2 - 10.1145/1863495.1863497

DO - 10.1145/1863495.1863497

M3 - Conference contribution book

SN - 9781450302517

SP - 1

EP - 12

BT - Proceedings of the 6th ACM SIGPLAN workshop on Generic programming

CY - New York

ER -

Mcbride C. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN workshop on Generic programming . New York. 2010. p. 1-12 https://doi.org/10.1145/1863495.1863497