Papers, drafts, and reports on type inference

We give below papers and reports on type inference for several extensions of the Haskell 98 type system. This is joint work with Simon Peyton Jones, Stephanie Weirich, and Geoff Washburn.

Papers

[1] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Simple unification-based type inference for GADTs. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 50-61, New York, NY, USA, 2006. ACM Press.
[ bib | .pdf ]
[2] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy types: inference for higher-rank types and impredicativity. In ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, pages 251-262, New York, NY, USA, 2006. ACM Press.
[ bib | .pdf ]
[3] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. J. Funct. Program., 17(1):1-82, 2007.
[ bib | http ]

Reports

[4] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Practical type inference for arbitrary-rank types, Technical Appendix. Technical Report MS-CIS-05-14, University of Pennsylvania, July 2005.
[ bib | .pdf ]
[5] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy type inference for higher-rank types and impredicativity, Technical Appendix. Technical Report MS-CIS-05-23, University of Pennsylvania, April 2006.

This report accompanies the boxy types paper and provides proofs for the claims in that paper.
[ bib | .pdf ]

[6] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Simple unification-based type inference for GADTs, Technical Appendix. Technical Report MS-CIS-05-22, University of Pennsylvania, April 2006.

This is a new version of the GADT paper technical report. Includes treatment of fresh most general unifiers and scoped type variables, but handles only non-nested patterns for simplicity; all the problems encountered in the treatment of nested patterns already occur in the treatment of non-nested patterns. The old version of the report available from http://www.cis.upenn.edu/~dimitriv/wobbly/wobbly-techreport-old.pdf treats also nested patterns but assumes that the inference algorithm and the specification use exactly the same most general unifier procedure for GADT type refinement.
[ bib | .pdf ]