I’ll be soon publishing a task breakdown for DH. In addition to the planned changes, I decided to include the recent history of related work (2018–2024) in the form of links to specific proposals, issues, and commits.
Here’s an example of what a single section is going to look like:
A notable omission in the task graph has caught my eye: We need to figure out the interaction between type families, associated types, and dependent types. This is a very foundational point that is both very nuanced and has long lasting consequences. If there is pre-existing agreement or even discussion of this I haven’t seen it.
Just to name a few nuances: Type families on the surface look like promoted functions but their equations aren’t (always) matched from top to bottom, and the equations can repeat quantified variables (example). That makes them more similar in spirit to conservatively extending a theory by adjoining a functional symbol. They use “evaluation by unification”, whereas “normalization by evaluation” is standard in dependent types. Associated types are currently just type families with a cosmetic attachment to a parent type class. However in a dependently typed language we would instead have them as Type-kinded fields in the class dictionary.
