|Version 4 (modified by goldfire, 2 years 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, Haskell currently enjoys a confluence of design decisions. One says that compile-time arguments are elided in runtime code. For example, when calling map :: (a -> b) -> [a] -> [b], the type instantiations for a and b are properly arguments to map (and are passed quite explicitly in Core), but these arguments are always elided in surface Haskell. As the levels are mixing, we may want to revisit this. Along similar lines, type arguments in Haskell are always erasable -- that is, instantiations for types are never kept at runtime. While this is generally a Good Thing and powers much of Haskell's efficiency, dependent typing relies on keeping some types around at runtime. Here, it is even more apparent that sometimes, we want to be able to pass in values for type arguments, especially if those values can be inspected at runtime.
Haskell currently has two quantifiers: forall and ->, as classified in the following table:
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.
- Hasochism: The Pleasure and Pain of Dependently Typed Haskell. Sam Lindley and Conor McBride. Haskell Symposium 2013.