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.