Extensible elaborators for dependently-typed languages
Date: Wed, September 21, 2022
Room: E.420 Turing (building 28) / Zoom room tba
There are a few established implementations of dependently-typed languages like Agda, Coq or Idris. However successful they are the implementation details are quite complex and only a few dare to extend them. This exists in contrast with Haskell, which has a rich culture of extensions, both in the form of pragmas and plugins.
This work aims to bring similar capabilities to the dependently-typed world. We are working on a design sketch of a dependently-typed language that would be extensible on the front-end, without affecting the core and thus, soundness of the language. The focus is on constraint-solving as part of the elaboration procedure, leaving syntax extensions to be solved at a later point. This is work-in-progress.
| Tactics in Agda using reflection
Next: Paul van der Stel | Tactics in Agda using reflection