wiki:DependentHaskell

Version 2 (modified by goldfire, 12 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,

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: