... deliberately practicing something I want to be more of an expert in.
- linear
- compilation (registers, etc)
- toggle HOAS / bidirectional knobs
- ABTs
- data types!
- effects
- equality / homotopy
- reflection
- propagators
- pattern matching
- universe hierarchies
- subtyping
Day | Calendar | Summary |
---|---|---|
1 | Apr 5 | Bidirectional dependent typechecker with HOAS (inspiration) |
2 | Apr 6 | Was going to get data types working, but just made it to nat lits. This day turned out to be mostly about exploring the representation from the article linked in Day 1. |
3 | Apr 6 | refinements to day 2 |
4 | Apr 7 | first cut at representing data types |
5 | Apr 8 | Day 4 + pattern matching, typechecking, elimination |
6 | Apr 9 | Day 5 + pretty printing |
7 | Apr 10 | Experiment with four binder representations from Chargueraud's locally nameless survey |
8 | Apr 11 | Implement locally bound operations (from Chargueraud) |