Improving Agda’s module system

Ivar de Bruin

Agda is a language used to write computer-verified proofs. It has a module system that provides namespacing, module parameters and module aliases. These parameters and aliases can be used to write shorter and cleaner proofs. However, the current implemen- tation of the module system has several problems, such as an ex- ponential desugaring of module aliases. This paper shows how the module system can be changed to address these problems. We have found that we do not need any desugarings during type-checking, but can instead handle module parameters and aliases during sig- nature lookup by making a small change to the scope-checker, com- pletely eliminating any exponential growth problems and unnec- essary complexity. This will allow users to make more effective use of the module system, simplifying their proofs. Furthermore, the improvements to the module system will allow future research to fix the problems with Agda’s implementation of pretty-printing, records and open public statements.

---

Previous: Jaap de Jong | Speeding up program synthesis using specification discovery
Next: Luka Miljak | Formal semantics of declarative disambiguation rules