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:

Contacts for the project

Dependently Typed Languages in Statix

Student: Jonathan Brouwer
Supervisor(s): Jesper Cockx, Aron Zwaan