##
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)

Student: Jonathan Brouwer

Supervisor(s): Jesper Cockx, Aron Zwaan