Changes between Version 15 and Version 16 of Status/May14


Ignore:
Timestamp:
Apr 28, 2014 11:59:31 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Status/May14

    v15 v16  
    2121 * **Using an SMT Solver in the type-checker** - Iavor Diatchki is working on utilizing an off-the-shelf SMT solver in GHC's constraint solver. Currently, the main focus for this is improved support for reasoning with type-level natural numbers, but it opens the doors to other interesting functionality, such as supported for lifted (i.e., type-level) `(&&)`, and `(||)`, type-level bit-vectors (perhaps this could be used to implement type-level sets of fixed size), and others.   This work is happening on branch `wip/ext-solver`. 
    2222 
    23  * **Kind equality and kind coercions** - TODO Richard 
     23 * **Kind equality and kind coercions** - Richard Eisenberg (with support from Simon PJ and Stephanie Weirich, among others) is implementing a change to the Core language, as described in a recent paper [FC]. When this work is complete, ''all'' types will be promotable to kinds, and ''all'' data constructors will be promotable to types. This will include promoting type synonyms and type families. As the details come together, there may be other source language effects, such as the ability to make kind variables explicit. It is not expected for this to be a breaking change -- the change should allow strictly more programs to be accepted. 
    2424 
    2525 * **Partial type signatures** - TODO Simon, Thomas 
     
    5454[KD] Kinds without Data - ​http://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData  [[br]]  
    5555[TA] Explicit type application - ​http://ghc.haskell.org/trac/ghc/wiki/ExplicitTypeApplication [[br]] 
     56[FC] "System FC with Explicit Kind Equality" - http://www.seas.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf [[br]] 
    5657[!CoverityScan] https://scan.coverity.com [[br]]  
    5758[PPA] https://launchpad.net/~hvr/+archive/ghc/ [[br]]