Conversion and reduction in dependently-typed calculi
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.
Material
Future work
- 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:
- AUTOMATH
- Idris
- Fredrik mentioned a body of particularly hard problems whose solutions where hard to type-check with Agda.
- Nested Σ are particularly hard.
Anders mentioned Boespflug, 2011. It demonstrates a scheme to compile open CIC terms into OCaml for fast reduction. Something similar could be done for Agda by using the GHC API (see hint)
Bas mentioned Dunchev, 2015. It is a fast implementation of a λProlog intepreter with the explicit goal of typechecking dependently-typed proofs.