For the last few weeks/months, a focus of my work was to import from lean theorem prover using its export format. As I move away from this, its time to record some lessons.
Universes
- Lean uses universe parametrizations.
- For the first time in my code, which universe mattered, with function application failing because the domain and the type of the argument differed in Universes.
- An unsafe hack of making universes equal was implemented.
- Eventually, this should be replaced by an appropriate unified apply function.
Propositions
- Lean makes use of Propositions, which are at level -1.
- Some of the difficulty was in the way propositional witnesses are suppressed - just a pain with no lessons.
- But the main step was implementing propositional types: a universe Prop, symbolic types in this universe, and the definition that symbolic objects with type a proposition are all just named witness, and hence equal.
- This is in general a worthwhile optimization for equality and even function application.
Recursion paralysis
- Lean uses a lot of recursion, going very deep.
- This uncovered some bugs in replacement (where it was trivial) which have been fixed.
- Nevertheless, recursion remains very slow. One can partly blame lean export, but it is worth trying to fix this.
- The key steps in recursion, including replacement and equality, are done without any concurrency or stack safety.
- One should presumably wrap and override these with, for example, Task.