Changes between Version 1 and Version 2 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 12:19:03 PM (14 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v1 v2  
    11= Adding dependent types to Haskell =
    22
    3 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.
     3This 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.
     4
     5== Surface Language Design ==
     6
     7It 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.
     8
     9=== Quantifiers ===
     10
     11As pointed out in the [#hasochism Hasochism paper],
    412
    513== Related work ==
     14
     15'''Readers:''' Please add to these lists!
    616
    717There are several published works very relevant to the design:
     
    1323
    1424* [http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf Dependently typed programming with singletons]. Richard A. Eisenberg and Stephanie Weirich. Haskell Symposium 2012.
    15 * [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.
     25* [=#hasochism [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.