Time: Wed 2016-03-09 13:15
Room: Johanneberg, Gothenburg
Type-checking a dependently-typed language involves solving equality constraints between λ-terms. Reduction to a normal form is the first step before applying a unification procedure.
The goal of the talk to spur some discussion on which techniques show more promise to speed up the Agda implementation. Anyone with experience or an interest in the implementation of dependent type-checking is welcome.
- Michal argued for
- Having a more transparent cost-model
- Developing profiling tools that help the user change the program for it to type-check faster.
- Clarifying which use cases are we targeting, as there is no performance silver-bullet.
- Some other tools worth checking out:
- Fredrik mentioned a body of particularly hard problems
whose solutions where hard to type-check with Agda.
- Nested Σ are particularly hard.
- Bas mentioned Dunchev, 2015. It is a fast implementation of a λProlog intepreter with the explicit goal of typechecking dependently-typed proofs.