Document Open Access Logo

Deeper Shallow Embeddings

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

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.28.pdf
  • Filesize: 0.6 MB
  • 18 pages

Document Identifiers

Author Details

Jacob Prinz
  • University of Maryland, College Park, MD, USA
G. A. Kavvos
  • University of Bristol, UK
Leonidas Lampropoulos
  • University of Maryland, College Park, MD, USA

Funding

This material is based upon work supported by NSF award #2107206, Efficient and Trustworthy Proof Engineering (any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF).

Cite AsGet BibTex

Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos. Deeper Shallow Embeddings. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.28

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering
  • Software and its engineering → General programming languages
  • Social and professional topics → History of programming languages
Keywords
  • type theory
  • shallow embedding
  • deep embedding
  • Agda

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 18-29. Association for Computing Machinery, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  2. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science, 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:1)2017.
  3. Thorsten Altenkirch and Bernhard Reus. Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Jörg Flum and Mario Rodriguez-Artalejo, editors, Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 453-468, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-48168-0_32.
  4. Lennart Augustsson. Making edsls fly. http://vimeo.com/73223479, 2012.
  5. Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute, editors, Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings, volume A-10 of IFIP Transactions, pages 129-156. North-Holland, 1992. URL: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/EmbeddingPaper.pdf.
  6. Jacques Carette, Oleg Kiselyov, and Chung-Chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509-543, 2009. URL: https://doi.org/10.1017/S0956796809007205.
  7. James Chapman. Type Theory Should Eat Itself. Electronic Notes in Theoretical Computer Science, 228:21-36, 2009. URL: https://doi.org/10.1016/j.entcs.2008.12.114.
  8. Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. Kami: A platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110268.
  9. Koen Claessen. Embedded Languages for Describing and Verifying Hardware. PhD thesis, Chalmers University of Technology, Gothenburg, Sweden, 2001. URL: http://publications.lib.chalmers.se/publication/636-embedded-languages-for-describing-and-verifying-hardware.
  10. Koen Claessen and John Hughes. Quickcheck: A lightweight tool for random testing of haskell programs. Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP, 46, January 2000. URL: https://doi.org/10.1145/1988042.1988046.
  11. Thierry Coquand. Canonicity and normalization for dependent type theory. Theoretical Computer Science, 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  12. Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 93-109. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_7.
  13. Peter Dybjer and Anton Setzer. Indexed induction–recursion. The Journal of Logic and Algebraic Programming, 66(1):1-49, 2006. URL: https://doi.org/10.1016/j.jlap.2005.07.001.
  14. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proceedings of the 4th ACM SIGPLAN international conference on Principles and Practice of Declarative Programming - PPDP '02, pages 26-37. ACM Press, 2002. URL: https://doi.org/10.1145/571157.571161.
  15. Jeremy Gibbons and Nicolas Wu. Folding domain-specific languages: deep and shallow embeddings (functional pearl). In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pages 339-347. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628138.
  16. Martin Hofmann. Syntax and Semantics of Dependent Types. In Andrew M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. URL: https://doi.org/10.1017/CBO9780511526619.004.
  17. Paul Hudak and Donya Quick. The Haskell School of Music: From Signals to Symphonies. Cambridge University Press, 2018. URL: https://doi.org/10.1017/9781108241861.
  18. Ambrus Kaposi, András Kovács, and Nicolai Kraus. Shallow Embedding of Type Theory is Morally Correct. In Graham Hutton, editor, Mathematics of Program Construction, volume 11825 of Lecture Notes in Computer Science, pages 329-365, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-33636-3_12.
  19. Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner’s Luck: a language for property-based generators. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 114-129, 2017. URL: http://dl.acm.org/citation.cfm?id=3009868, URL: https://doi.org/10.1145/3009837.3009868.
  20. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. Google Scholar
  21. Conor McBride. Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming, WGP '10, pages 1-12, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1863495.1863497.
  22. Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman Amarasinghe. Halide: A language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. SIGPLAN Not., 48(6):519-530, June 2013. URL: https://doi.org/10.1145/2499370.2462176.
  23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  24. Vasco T. Vasconcelos. Fundamentals of session types. Information and Computation, 217:52-70, 2012. URL: https://doi.org/10.1016/j.ic.2012.05.002.
  25. Brent Yorgey. Diagrams: A declarative dsl for creating vector graphics. https://diagrams.github.io/doc/manual.html, 2013.
  26. Christina Zeller and Ivan Perez. Mobile game programming in haskell. In Donya Quick and Daniel Winograd-Cort, editors, Proceedings of the 7th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, FARM@ICFP 2019, Berlin, Germany, August 18-23, 2019, pages 37-48. ACM, 2019. URL: https://doi.org/10.1145/3331543.3342580.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact