There’s more than one way to get to a Dependent Core. Various formalisms are presented in:
[Type Inference, Haskell and Dependent Types](https://adam.gundry.co.uk/pub/thesis/), PhD thesis by Adam Gundry (2013)
[Dependent Types in Haskell: Theory and Practice](https://richarde.dev/papers/2016/thesis/eisenberg-thesis.pdf), PhD thesis by Richard A. Eisenberg (2016)
A Specification for Dependently-Typed Haskell, by Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg (2017) A graded dependent type system with a usage-aware semantics, by Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich (2021)
I’m going to update the roadmap with these links.
The main theoretical questions are:
- Whether to combine the term and type languages within Core (the ambitious vs. the incremental approach).
- How to combine dependent types with linear types (don’t forget multiplicity polymorphism).
Long-term, I’d prefer a Core that combines the term and type languages. But realistically, if the goal is to get to Π-types via the safest route without reengineering half of GHC, Adam’s thesis presents a compelling phase-separated approach.
Hmm. This conversation has proved rather insightful. I think I now realise what Conor was hinting at. Indeed, we could start with a Core that simply adds foreach
and dcase
, then work on combining terms and types afterwards.