History of DH (Dependent Types in Haskell) contributions

The Haskell development roadmap for Dependent Types (DH) will be updated with links to key research papers, including PhD theses by Adam Gundry (2013) and Richard A. Eisenberg (2016), a specification by Stephanie Weirich et al. (2017), and a graded dependent type system paper by Choudhury et al. (2021). The main theoretical questions are whether to combine term and type languages in Core and how to integrate dependent types with linear types, with a long-term preference for a unified Core but a phase-separated approach as a safer incremental step.

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 https://richarde.dev/papers/2017/dep-haskell-spec/dep-haskell-spec.pdf , 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 https://richarde.dev/papers/2021/grad/grad-extended.pdf , 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.