Document Open Access Logo

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation

Authors Matthew Sirman, Meven Lennon-Bertrand , Neel Krishnaswami

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.5.pdf
  • Filesize: 0.92 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
  • Theory of computation → Type theory
  • Theory of computation → Denotational semantics
Keywords
  • Dependent type theory
  • Bidirectional typing
  • Observational equality
  • Normalisation by evaluation

Metrics

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

Abstract

We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.’s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda’s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality.

Cite As Get BibTex

Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami. Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.5

Author Details

Matthew Sirman
  • University of Cambridge, UK
Meven Lennon-Bertrand
  • University of Cambridge, UK
Neel Krishnaswami
  • University of Cambridge, UK

Supplementary Materials

References

  1. Andreas Abel. Normalization by Evaluation Dependent Types and Impredicativity. PhD thesis, Institut für Informatik Ludwig-Maximilians-Universität München, München, May 2013. URL: https://www.cse.chalmers.se/~abela/habil.pdf.
  2. Andreas Abel, Thierry Coquand, and Miguel Pagano. A modular type-checking algorithm for type theory with singleton types and proof irrelevance. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, pages 5-19, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02273-9_3.
  3. Andreas Abel and Brigitte Pientka. Higher-Order Dynamic Pattern Unification for Dependent Types and Records. In Luke Ong, editor, Typed Lambda Calculi and Applications, volume 6690, pages 10-26. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_5.
  4. Thorsten Altenkirch. Extensional equality in intensional type theory. In Proceedings - Symposium on Logic in Computer Science, pages 412-420, February 1999. URL: https://doi.org/10.1109/LICS.1999.782636.
  5. Thorsten Altenkirch and Conor McBride. Towards Observational Type Theory, 2006. Google Scholar
  6. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, pages 57-68, Freiburg Germany, October 2007. ACM. URL: https://doi.org/10.1145/1292597.1292608.
  7. Bob Atkey. Simplified observational type theory, 2017. URL: https://github.com/bobatkey/sott.
  8. Henning Basold and Herman Geuvers. Type Theory based on Dependent Inductive and Coinductive Types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 327-336, July 2016. URL: https://doi.org/10.1145/2933575.2934514.
  9. Rafael Bocquet. obstt, 2023. URL: https://gitlab.com/RafaelBocquet/obstt.
  10. Thierry Coquand. An algorithm for testing conversion in type theory. Logical frameworks, 1:255-279, 1991. Google Scholar
  11. Thierry Coquand and Christine Paulin. Inductively defined types. In G. Goos, J. Hartmanis, D. Barstow, W. Brauer, P. Brinch Hansen, D. Gries, D. Luckham, C. Moler, A. Pnueli, G. Seegmüller, J. Stoer, N. Wirth, Per Martin-Löf, and Grigori Mints, editors, COLOG-88, volume 417, pages 50-66. Springer Berlin Heidelberg, Berlin, Heidelberg, 1990. URL: https://doi.org/10.1007/3-540-52335-9_47.
  12. Marcelo Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Mathematical Structures in Computer Science, 32(8):1028-1065, September 2022. URL: https://doi.org/10.1017/S0960129522000263.
  13. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without k. Proceedings of the ACM on Programming Languages, 3(POPL):1-28, January 2019. URL: https://doi.org/10.1145/329031610.1145/3290316.
  14. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  15. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a modal dependent type theory. Proc. ACM Program. Lang., 3(ICFP), July 2019. URL: https://doi.org/10.1145/3341711.
  16. Robert Harper. Boolean Blindness, 2011. URL: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/.
  17. Martin Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995. URL: https://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/.
  18. András Kovács. Elaboration with first-class implicit function types. Proceedings of the ACM on Programming Languages, 4(ICFP):1-29, August 2020. URL: https://doi.org/10.1145/3408983.
  19. András Kovács. Elaboration-zoo, May 2023. URL: https://github.com/AndrasKovacs/elaboration-zoo.
  20. András Kovács. Efficient evaluation with controlled definition unfolding. In 3rd Workshop on the Implementation of Type Systems, 2025. Google Scholar
  21. Per Martin-Löf. Intuitionistic type theory. In Studies in Proof Theory, 1984. Google Scholar
  22. Conor McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 1999. Google Scholar
  23. Nax Paul Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1-2):159-172, March 1991. URL: https://doi.org/10.1016/0168-0072(91)90069-X.
  24. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007. Google Scholar
  25. Erik Palmgren. On universes in type theory, pages 191–-204. Oxford University Press, 1998. URL: https://doi.org/10.1093/oso/9780198501275.003.0012.
  26. Loïc Pujet. Computing with Extensionality Principles in Dependent Type Theory. PhD thesis, Nantes Université, December 2022. Google Scholar
  27. Loïc Pujet and Nicolas Tabareau. Observational equality: Now for good. Proceedings of the ACM on Programming Languages, 6(POPL):1-27, January 2022. URL: https://doi.org/10.1145/3498693.
  28. Loïc Pujet and Nicolas Tabareau. Impredicative observational equality. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571739.
  29. Loïc Pujet and Nicolas Tabareau. Observational equality meets cic. In Stephanie Weirich, editor, Programming Languages and Systems, pages 275-301. Springer Nature Switzerland, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_12.
  30. Matthew Sirman. A normalisation by evaluation implementation of a type theory with observational equality. Bachelor’s thesis, University of Cambridge, 2023. Google Scholar
  31. Matthew Sirman. observational-type-theory, May 2023. URL: https://github.com/matthew-sirman/observational-type-theory.
  32. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact