Deriving High-Quality Type-Checkers from Declarative Type-System Specifications

Aron Zwaan


Date: Wed, January 19, 2022
Time: 11:00
Room: Aron's Zoom Room
Note: This is a PhD Go/No-Go meeting


Type-checking is of vital importance to program robustness. In addition, type information can be used in program transformation/optimization, improving performance, and for editor services, improving the productivity of a programmer.

In our group, the main research focus has been on interpreting declarative type-system specifications expressed in Statix as constraint programs, yielding a type-checker. This works fairly well: Type-checkers derived from Statix are ‘sound’ with respect to the declarative semantics of the language. However, Statix-derived type-checkers are still an order of magnitude slower than hand-written type-checkers. In addition, e.g. Hindley-Milner-based type-systems and substructural type-systems cannot be expressed in Statix, while the representation of explicitly parameterized types (e.g. System F) is verbose. Moreover, the representation of the type-checking result can be improved to enable better editor-services and transformations. In addition, improvements to the Statix language can aid to write better and more concise specifications. In my PhD, I want to address these problems.

In this talk, I first want to present my research of the last year: A framework that incrementalizes scope-graph-based type-checkers.

Then, I want to present the ideas for the coming years. Performance can still be enhanced by synthesizing type-checkers from Statix specifications, rather than interpreting them, and by making the incrementality more fine-grained. Regarding the type-checker result, the quality of error messages should be improved, and it should be possible to transform analysis results together with an AST. Finally, the issues in expressiveness should be adressed. These advancements will make derived type-checkers competitive to hand-written ones.

Previous: Lucas Escot |
Next: |