wiki:DependentHaskell

Version 4 (modified by goldfire, 14 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.

Quantifiers

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:

Quantifier Dependent? Visible? Relevant?
forall yes no no
-> no yes yes

Related work

Readers: Please add to these lists!

There are several published works very relevant to the design:

There are also many works addressing the use of dependent types in Haskell. Here is a selection: