Document Open Access Logo

Dependently Typed Languages in Statix

Authors Jonathan Brouwer , Jesper Cockx , Aron Zwaan

PDF
Thumbnail PDF

File

OASIcs.EVCS.2023.6.pdf
  • Filesize: 0.53 MB
  • 8 pages

Document Identifiers

Author Details

Jonathan Brouwer
  • Delft University of Technology, The Netherlands
Jesper Cockx
  • Delft University of Technology, The Netherlands
Aron Zwaan
  • Delft University of Technology, The Netherlands

Cite AsGet BibTex

Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently Typed Languages in Statix. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/OASIcs.EVCS.2023.6

Abstract

Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Software and its engineering → Functional languages
  • Software and its engineering → Compilers
Keywords
  • Spoofax
  • Statix
  • Dependent Types
  • Scope Graphs
  • Calculus of Constructions

Metrics

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

Supplementary Materials

References

  1. Andrej Bauer, Philipp G. Haselwarter, and Anja Petkovic. Equality checking for general type theories in andromeda 2. In Anna Maria Bigatti, Jacques Carette, James H. Davenport, Michael Joswig, and Timo de Wolff, editors, Mathematical Software - ICMS 2020 - 7th International Conference, Braunschweig, Germany, July 13-16, 2020, Proceedings, volume 12097 of Lecture Notes in Computer Science, pages 253-259. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-52200-1_25.
  2. Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The lm-calculus modulo as a universal proof language. In David Pichardie and Tjark Weber, editors, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012, volume 878 of CEUR Workshop Proceedings, pages 28-43. CEUR-WS.org, 2012. URL: http://ceur-ws.org/Vol-878/paper2.pdf.
  3. Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently typed languages in statix. Delft University Of Technology. To be published on URL: https://repository.tudelft.nl.
  4. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2–3):95-120, February 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  5. Luís Eduardo de Souza Amorim and Eelco Visser. Multi-purpose syntax definition with sdf3. In Software Engineering and Formal Methods: 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020, Proceedings, pages 1-23, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-58768-0_1.
  6. Jana Dunfield and Neel Krishnaswami. Bidirectional typing. ACM Comput. Surv., 54(5), May 2021. URL: https://doi.org/10.1145/3450952.
  7. Lennart Kats and Eelco Visser. The spoofax language workbench. ACM SIGPLAN Notices, 45:237-238, October 2010. URL: https://doi.org/10.1145/1869542.1869592.
  8. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher Order Symbol. Comput., 20(3):199-207, September 2007. URL: https://doi.org/10.1007/s10990-007-9018-9.
  9. Lena Magnusson and Bengt Nordström. The alf proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 213-237. Springer, 1993. URL: https://doi.org/10.1007/3-540-58085-9_78.
  10. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Extensions of Logic Programming, International Workshop, Tübingen, FRG, December 8-10, 1989, Proceedings, volume 475 of Lecture Notes in Computer Science, pages 253-281. Springer, 1989. URL: https://doi.org/10.1007/BFb0038698.
  11. Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, volume 9032 of Lecture Notes in Computer Science, pages 205-231. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_9.
  12. Daniel A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. Language-parametric static semantic code completion. Proceedings of the ACM on Programming Languages, 6(OOPSLA1), April 2022. URL: https://doi.org/10.1145/3527329.
  13. Frank Pfenning. Logic programming in the LF logical framework, pages 149-182. Cambridge University Press, 1991. URL: https://doi.org/10.1017/CBO9780511569807.008.
  14. Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume 1632 of Lecture Notes in Computer Science, pages 202-206. Springer, 1999. URL: http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm.
  15. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 1 edition, February 2002. Google Scholar
  16. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as types. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1-30, 2018. URL: https://doi.org/10.1145/3276484.
  17. Stephanie Weirich. Implementing dependent types in pi-forall, 2022. URL: https://doi.org/10.48550/arXiv.2207.02129.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact