... | ... | @@ -41,7 +41,7 @@ The current plan is to steam forward to the end of the year, and begin to get re |
|
|
|
|
|
- **Overloaded record fields**[\[OverloadedRecordFields](records/overloaded-record-fields)\]. After countless more discussions and several revisions, Adam Gundry implemented the new `-XOverloadedRecordFields` extension for GHC - again! - but this time with a newer design - and the first piece of the implementation is up for review at [ https://phabricator.haskell.org/D761](https://phabricator.haskell.org/D761) - we're hoping to review it and integrate it soon.
|
|
|
|
|
|
- **Using an SMT Solver as a type-checker plugin**[ \[TCSMT](https://github.com/yav/type-nat-solver)\]. Iavor Diatchki is working on implementing support for using SMT solvers in the typechecker, via the plugins mechanism. 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.
|
|
|
- **Using an SMT Solver as a type-checker plugin**[ \[repo](https://github.com/yav/type-nat-solver)\] [ \[paper](https://github.com/yav/type-nat-solver/raw/master/docs/paper.pdf)\]. Iavor Diatchki is working on implementing support for using SMT solvers in the typechecker, via the plugins mechanism. 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.
|
|
|
|
|
|
- **Kind equality, kind coercions, and dependently typed Core** \[KindEqualities\]. Richard Eisenberg (with support from Simon PJ and Stephanie Weirich, among others) is implementing a change to the Core language, as described in "[ System FC with explicit kind equality](http://www.seas.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf)" \[FCkinds\]. 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.
|
|
|
This can also go down as one of the **larger** changes in recent memory - [ https://phabricator.haskell.org/D808](https://phabricator.haskell.org/D808) is the biggest Phabricator review we've done to date, changing over 10,000 lines of code in the compiler!
|
... | ... | @@ -90,4 +90,5 @@ The current plan is to steam forward to the end of the year, and begin to get re |
|
|
- \[[StaticPointers](static-pointers)\] [ https://ghc.haskell.org/trac/ghc/wiki/StaticPointers](https://ghc.haskell.org/trac/ghc/wiki/StaticPointers)
|
|
|
- [\[TCPlugins](plugins/type-checker)\] [ https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker](https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker)
|
|
|
- [ \[TCSMT](https://github.com/yav/type-nat-solver)\] [ https://github.com/yav/type-nat-solver](https://github.com/yav/type-nat-solver)
|
|
|
- [ \[TCSMT_paper](https://github.com/yav/type-nat-solver/raw/master/docs/paper.pdf)\] [ https://github.com/yav/type-nat-solver/raw/master/docs/paper.pdf](https://github.com/yav/type-nat-solver/raw/master/docs/paper.pdf)
|
|
|
- [Typeable](typeable)[ https://ghc.haskell.org/trac/ghc/wiki/Typeable](https://ghc.haskell.org/trac/ghc/wiki/Typeable) |
|
|
\ No newline at end of file |