|Version 2 (modified by goldfire, 13 months ago) (diff)|
Adding dependent types to Haskell
This page is to track design and implementation ideas around adding a form of dependent types to Haskell. This work will also fix bug #7961. Richard Eisenberg (a.k.a. goldfire) is expecting to take on most (all?) of this work.
Surface Language Design
It is possible to fix #7961 without any surface language changes, as that bug addresses only lifting restrictions on promotion. There is a chance that this bugfix will enter HEAD without all of the other features below, but this writeup generally will not consider fixing #7961 separate from adding dependent types.
As pointed out in the Hasochism paper,
Readers: Please add to these lists!
There are several published works very relevant to the design:
- System FC with Explicit Kind Equality. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. ICFP 2013.
- Type Inference, Haskell, and Dependent Types. Adam Gundry. PhD Thesis, 2013.
There are also many works addressing the use of dependent types in Haskell. Here is a selection:
- Dependently typed programming with singletons. Richard A. Eisenberg and Stephanie Weirich. Haskell Symposium 2012.
- [https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf Hasochism: The Pleasure and Pain of Dependently Typed Haskell]. Sam Lindley and Conor McBride. Haskell Symposium 2013.