Extensible elaborators for dependently-typed languages

Bohdan Liesnikov

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.

---

Previous: | Tactics in Agda using reflection
Next: Paul van der Stel | Tactics in Agda using reflection