-
Q: How to implement typeclasses in proof assistants (Coq, Lean).
- video of the basics
- Haskell
- apartness
- coherence: all instances are the same
- it is used to ensure code correctness (sorted map with insert and union)
- How Scala handles it if you union two sorted map with different order instances: it doesn’t care if the second parameter is sorted or not, link
- in video: it should use dependent type, the SortedMap depends on the order
- Scala
- Tabled Type class Resolution
-
Q: How is extension methods implemented
-
Q: Again, how the elaborator as a whole works: integrate meta solving, type class resolution, ad-hoc overloading and coercions?
- The Lean 2 paper seems not apply very well to Lean 4 implementation
-
Overview of Lean 4 source code
- slides from 2019
- outdated, compiler is in Lean
- slides from 2020
- the object header is 1 word, it use 64bits to encode a lot of information
- Lean 4 repo
/src
Lean
is the elaborator & compiler of Lean implemented in Lean
Compiler
backend
Elab
is the elaborator
PreDefinition
is termination checking, or translation to eliminators
Meta
is meta solving and all that
Parser
is the extensible parsers and all that
-
Lean4 changed its naming convention from snake_case
to camelCase
??!!