# History of DH (Dependent Types in Haskell) contributions > Source: > Published: 2026-08-14 13:20:28+00:00 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.