Dependently Typed Languages in Statix
Master Project of Jonathan Brouwer

Project Description

When working with the Spoofax workbench, the Statix meta-language can be used for the specification of Static Semantics. With this language, we aim to provide a high-level, declarative and compact description of a type-system. To provide these advantages to as many language developers as possible, Statix also aims to cover a broad range of languages and type-systems. However, we never made an attempt to express dependently typed languages in Statix.

Dependently typed languages are different from other languages because they allow types to be parameterized by values. This allows more rigourous reasoning over types and the values that are inhabited by a type, which makes dependent types particularly suitable for proof assistants. This expressiveness also makes dependent type systems more complicated to implement. Especially, deciding equality of types requires evaluation of the terms they are parametrized by. Second, type assumptions cannot be treated as a set, because they can depend on earlier introduced values. Instead, sequences of type assumptions called telescopes are used.

The main research question for this project is to evaluate how well Statix is fit for the task of defining a simple dependently-typed language. In other words, we want to investigate whether typical features of dependently typed language can be encoded concisely in Statix. This question is divided into the following sub-questions:

• Can telescopes be encoded concisely using scope graphs?
• Can beta-reduction be encoded concisely in Statix?
• How do the language-parametric services built on Statix, such as renaming, inlining and semantic code completion, behave for dependently typed languages?

If the project goes well, it could be extended with one or more of the following options:

• Adding inference of implicit arguments.
• Adding fixpoints and termination checking.
• Adding used-defined algebraic data types with positivity checking and coverage checking.
• Adding universes and universe consistency checking.

Relevant literature:

• Löh, A., McBride, C., Swierstra, W. (2001). A tutorial implementation of a dependently typed lambda calculus. Fundamenta Informaticae XXI. 1001–1032. http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf
• Martin-Löf, P., & Sambin, G. (1984). Intuitionistic type theory (Vol. 9). Naples: Bibliopolis. http://people.csail.mit.edu/jgross/personal-website/papers/academic-papers-local/Martin-Lof80.pdf
• Coquand, T., & Huet, G. (1986). The calculus of constructions (Doctoral dissertation, INRIA). https://hal.inria.fr/inria-00076024/document
• Altenkirch T., Danielsson N.A., Löh A., Oury N. (2010). ΠΣ: Dependent Types without the Sugar. In: Blume M., Kobayashi N., Vidal G. (eds) Functional and Logic Programming. FLOPS 2010. Lecture Notes in Computer Science, vol 6009. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12251-4_5
• Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. 2018. Scopes as types. In: Proc. ACM Program. Lang. 2, OOPSLA, Article 114 (November 2018), 30 pages. DOI:https://doi.org/10.1145/3276484

Contacts for the project

• Jesper Cockx (TU Delft)
• Aron Zwaan (TU Delft)