License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.28
URN: urn:nbn:de:0030-drops-167379
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16737/
Go to the corresponding LIPIcs Volume Portal

Prinz, Jacob ; Kavvos, G. A. ; Lampropoulos, Leonidas

Deeper Shallow Embeddings

pdf-format:
LIPIcs-ITP-2022-28.pdf (0.6 MB)

Abstract

Deep and shallow embeddings are two popular techniques for embedding a language in a host language with complementary strengths and weaknesses. In a deep embedding, embedded constructs are defined as data in the host: this allows for syntax manipulation and facilitates metatheoretic reasoning, but is challenging to implement - especially in the case of dependently typed embedded languages. In a shallow embedding, by contrast, constructs are encoded using features of the host: this makes them quite straightforward to implement, but limits their use in practice.
In this paper, we attempt to bridge the gap between the two, by presenting a general technique for extending a shallow embedding of a type theory with a deep embedding of its typing derivations. Such embeddings are almost as straightforward to implement as shallow ones, but come with capabilities traditionally associated with deep ones. We demonstrate these increased capabilities in a number of case studies; including a DSL that only holds affine terms, and a dependently typed core language with computational beta reduction that leverages function extensionality.

BibTeX - Entry

@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28,
  author =	{Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
  title =	{{Deeper Shallow Embeddings}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16737},
  URN =		{urn:nbn:de:0030-drops-167379},
  doi =		{10.4230/LIPIcs.ITP.2022.28},
  annote =	{Keywords: type theory, shallow embedding, deep embedding, Agda}
}

Keywords: type theory, shallow embedding, deep embedding, Agda
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI