... | ... | @@ -29,28 +29,28 @@ See also [ Stephen Deihl's Haskell implementation reading list](http://www.steph |
|
|
|
|
|
- [ System FC, as implemented in GHC](http://git.haskell.org/ghc.git/blob/refs/heads/master:/docs/core-spec/core-spec.pdf) (2013), Richard Eisenberg.
|
|
|
|
|
|
- [ Modular type inference with local assumptions](http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn)[ doi link](http://dx.doi.org/10.1017/S0956796811000098), Simon Peyton Jones, Dimitrios Vytiniotis, Tom Schrijvers, Martin Sulzmann, Journal of Functional Programming, 2011. This epic 83-page JFP paper brings together, in a single uniform framework, a series of our earlier papers on type inference for type systems involving local constraints, including GADTs and indexed type families.
|
|
|
- [ Modular type inference with local assumptions](http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn) [ doi link](http://dx.doi.org/10.1017/S0956796811000098), Simon Peyton Jones, Dimitrios Vytiniotis, Tom Schrijvers, Martin Sulzmann, Journal of Functional Programming, 2011. This epic 83-page JFP paper brings together, in a single uniform framework, a series of our earlier papers on type inference for type systems involving local constraints, including GADTs and indexed type families.
|
|
|
|
|
|
- [ Practical Type Inference for Arbitrary-Rank Types](http://repository.upenn.edu/cis_papers/315/). Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields. JFP '07. [ doi](http://dx.doi.org/10.1017/S0956796806006034)[ technical appendix](http://repository.upenn.edu/cis_reports/58/) Describes type inference for higher-rank types.
|
|
|
- [ Practical Type Inference for Arbitrary-Rank Types](http://repository.upenn.edu/cis_papers/315/). Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields. JFP '07. [ doi](http://dx.doi.org/10.1017/S0956796806006034) [ technical appendix](http://repository.upenn.edu/cis_reports/58/) Describes type inference for higher-rank types.
|
|
|
|
|
|
- Type equalities in GHC's intermediate language:
|
|
|
|
|
|
- [ System FC with Explicit Kind Equality](http://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf). Stephanie Weirich, Justin Hsu, Richard A. Eisenberg. ICFP '13. [ doi](http://dx.doi.org/10.1145/2500365.2500599) Merges types with kinds, allowing promotion of GADTs and type families. Implementation not yet merged (July 2015).
|
|
|
- *Equality proofs and deferred type errors*, Simon Peyton Jones, Dimitrios Vytiniotis and Pedro Magalhaes (ICFP 2012). An exploration of what happens when you take equality proofs seriously in a compiler. [ doi](http://dx.doi.org/10.1145/2364527.2364554)[ pdf](http://dreixel.net/research/pdf/epdtecp.pdf)
|
|
|
- *Giving Haskell a promotion*, Brent Yorgey, Stepanie Weirich, Julien Cretin, Simon Peyton Jones, and Dimitrios Vytiniotis (TLDI 2012). How to (a) add kind polymorphism and (b) promote data types to become data kinds. [ doi](http://dx.doi.org/10.1145/2103786.2103795)[ pdf](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/promotion.pdf)
|
|
|
- *Evidence Normalization in System FC*. Dimitrios Vytiniotis, Simon Peyton Jones. RTA '13. [ doi](http://dx.doi.org/10.4230/LIPIcs.RTA.2013.20)[ pdf](http://drops.dagstuhl.de/opus/volltexte/2013/4050/pdf/3.pdf) Explains the coercion optimizer.
|
|
|
- *System F with Type Equality Coercions*, Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones (TLDI 2007). The first paper about System FC. [ doi](http://dx.doi.org/10.1145/1190315.1190324)[ extended pdf](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/tldi22-sulzmann-with-appendix.pdf)
|
|
|
- *Equality proofs and deferred type errors*, Simon Peyton Jones, Dimitrios Vytiniotis and Pedro Magalhaes (ICFP 2012). An exploration of what happens when you take equality proofs seriously in a compiler. [ doi](http://dx.doi.org/10.1145/2364527.2364554) [ pdf](http://dreixel.net/research/pdf/epdtecp.pdf)
|
|
|
- *Giving Haskell a promotion*, Brent Yorgey, Stepanie Weirich, Julien Cretin, Simon Peyton Jones, and Dimitrios Vytiniotis (TLDI 2012). How to (a) add kind polymorphism and (b) promote data types to become data kinds. [ doi](http://dx.doi.org/10.1145/2103786.2103795) [ pdf](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/promotion.pdf)
|
|
|
- *Evidence Normalization in System FC*. Dimitrios Vytiniotis, Simon Peyton Jones. RTA '13. [ doi](http://dx.doi.org/10.4230/LIPIcs.RTA.2013.20) [ pdf](http://drops.dagstuhl.de/opus/volltexte/2013/4050/pdf/3.pdf) Explains the coercion optimizer.
|
|
|
- *System F with Type Equality Coercions*, Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones (TLDI 2007). The first paper about System FC. [ doi](http://dx.doi.org/10.1145/1190315.1190324) [ extended pdf](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/tldi22-sulzmann-with-appendix.pdf)
|
|
|
|
|
|
- Type families:
|
|
|
|
|
|
- [ Associated Types with Class](http://research.microsoft.com/en-us/um/people/simonpj/Papers/assoc-types/assoc.pdf). Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, Simon Marlow. POPL '05. [ doi](http://dx.doi.org/10.1145/1040305.1040306) Introduces associated data families.
|
|
|
- [ Associated Type Synonyms](http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/at-syns.pdf). Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones. ICFP '05. [ doi](http://dx.doi.org/10.1145/1086365.1086397) Introduces associated type families.
|
|
|
- [ Closed Type Families with Overlapping Equations](http://www.seas.upenn.edu/~sweirich/papers/popl14-axioms.pdf). Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich. POPL '14. [ doi](http://dx.doi.org/10.1145/2535838.2535856)[ extended version](http://repository.upenn.edu/cis_reports/990/) Introduces closed type families.
|
|
|
- [ Closed Type Families with Overlapping Equations](http://www.seas.upenn.edu/~sweirich/papers/popl14-axioms.pdf). Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich. POPL '14. [ doi](http://dx.doi.org/10.1145/2535838.2535856) [ extended version](http://repository.upenn.edu/cis_reports/990/) Introduces closed type families.
|
|
|
- [ Injective Type Families for Haskell](http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones_eisenberg_injectivity.pdf). Jan Stolarek, Simon Peyton Jones, Richard Eisenberg. Haskell '15. [ doi](http://dx.doi.org/10.1145/2804302.2804314). Introduces injective type families.
|
|
|
|
|
|
- [ Safe Zero-Cost Coercions for Haskell](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/coercible.pdf). Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich. ICFP '14. [ doi](http://dx.doi.org/10.1145/2628136.2628141)[ extended pdf](http://www.seas.upenn.edu/~sweirich/papers/coercible-extended.pdf) Introduces the `Coercible` mechanism.
|
|
|
- [ Safe Zero-Cost Coercions for Haskell](http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/coercible.pdf). Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich. ICFP '14. [ doi](http://dx.doi.org/10.1145/2628136.2628141) [ extended pdf](http://www.seas.upenn.edu/~sweirich/papers/coercible-extended.pdf) Introduces the `Coercible` mechanism.
|
|
|
|
|
|
- [ Partial Type Signatures for Haskell](https://lirias.kuleuven.be/bitstream/123456789/423475/3/paper.pdf). Thomas Winant, Dominique Devriese, Frank Piessens, Tom Schrijvers. PADL 2014 [ TR](https://lirias.kuleuven.be/bitstream/123456789/424883/1/CW649.pdf)[ doi](http://dx.doi.org/10.1007/978-3-319-04132-2_2) Introduces partial type signatures.
|
|
|
- [ Partial Type Signatures for Haskell](https://lirias.kuleuven.be/bitstream/123456789/423475/3/paper.pdf). Thomas Winant, Dominique Devriese, Frank Piessens, Tom Schrijvers. PADL 2014 [ TR](https://lirias.kuleuven.be/bitstream/123456789/424883/1/CW649.pdf) [ doi](http://dx.doi.org/10.1007/978-3-319-04132-2_2) Introduces partial type signatures.
|
|
|
|
|
|
- [ Understanding Functional Dependencies via Constraint Handling Rules](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp06.pdf). Martin Sulzmann, Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey. JFP '07. [ doi](http://dx.doi.org/10.1017/S0956796806006137)
|
|
|
|
... | ... | @@ -77,7 +77,7 @@ Please add: System FC, GADTs, kind polymorphism etc |
|
|
|
|
|
- [ Secrets of the GHC inliner](http://research.microsoft.com/en-us/um/people/simonpj/papers/inlining/index.htm), Simon Peyton Jones and Simon Marlow, Journal of Functional Programming 12(4), July 2002, pp393-434. Describes how the Simplifier does inlining.
|
|
|
|
|
|
- [ A short cut to deforestation](http://research.microsoft.com/en-us/um/people/simonpj/papers/deforestation-short-cut.ps.Z), A Gill, SL Peyton Jones, J Launchbury, Proc Functional Programming Languages and Computer Architecture (FPCA'93), Copenhagen, June 1993, pp223-232. The famous foldr/build rule. Andy's [ PhD thesis](http://research.microsoft.com/en-us/um/people/simonpj/papers/andy-thesis.ps.gz) has more.
|
|
|
- [ A short cut to deforestation](http://research.microsoft.com/en-us/um/people/simonpj/papers/deforestation-short-cut.ps.Z), A Gill, SL Peyton Jones, J Launchbury, Proc Functional Programming Languages and Computer Architecture (FPCA'93), Copenhagen, June 1993, pp223-232. The famous foldr/build rule. Andy's [ PhD thesis](http://research.microsoft.com/en-us/um/people/simonpj/papers/andy-thesis.ps.gz) has more.
|
|
|
|
|
|
- [ Playing by the rules: rewriting as a practical optimisation technique in GHC](http://research.microsoft.com/en-us/um/people/simonpj/papers/rules.htm), Simon Peyton Jones, Andrew Tolmach and Tony Hoare, Haskell Workshop 2001. Describes how RULES work, which are heavily used in GHC.
|
|
|
|
... | ... | |