@unpublished{leftcorner, author = "Baars, Arthur I. and Swierstra, S. Doaitse", title = {{Typed Transformations of Typed Abstract Syntax}}, note = "http://www.cs.uu.nl/wiki/Center/TTTAS", month = "4", year = "2008" } @inproceedings{jones06, author = {Simon L. {Peyton~Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn}, title = {{Simple Unification-based Type Inference for GADTs}}, booktitle = {ICFP}, year = {2006}, pages = {50-61}, ee = {http://doi.acm.org/10.1145/1159803.1159811}, bibsource = {DBLP, http://dblp.uni-trier.de} } @TECHREPORT{jones04, AUTHOR = {Simon L. {Peyton~Jones} and Geoffrey Washburn and Stephanie Weirich}, TITLE = {Wobbly types: type inference for generalised algebraic data types}, INSTITUTION = {University of Pennsylvania}, ADDRESS = {Computer and Information Science Department, Levine Hall, 3330 Walnut Street, Philadelphia, Pennsylvania, 19104-6389}, YEAR = 2004, MONTH = jul, NUMBER = {MS-CIS-05-26}, PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-26.pdf}, PLCLUB = "yes", ABSTRACT = { Generalised algebraic data types (GADTs), sometimes known as ``guarded recursive data types'' or ``first-class phantom types'', are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is \emph{wobbly types}, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms. } } @inproceedings{baars02, author = {Arthur I. Baars and S. Doaitse Swierstra}, title = {{Typing Dynamic Typing}}, booktitle = {ICFP}, year = {2002}, pages = {157-166}, ee = {http://doi.acm.org/10.1145/581478.581494}, bibsource = {DBLP, http://dblp.uni-trier.de} } @book{pierce02, title = {{Types and Programming Languages}}, author = {Benjamin Pierce}, url = {http://www.cis.upenn.edu/~bcpierce/tapl/}, year = {2002}, keywords = {pgmlang types }, } @inproceedings{sulzmann07, author = {Martin Sulzmann and Manuel M. T. Chakravarty and Simon L. {Peyton~Jones} and Kevin Donnelly}, title = {{System F with Type Equality Coercions}}, booktitle = {TLDI}, year = {2007}, pages = {53-66}, ee = {http://doi.acm.org/10.1145/1190315.1190324}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{sulzmann06, author = {Martin Sulzmann and Jeremy Wazny and Peter J. Stuckey}, title = {{A Framework for Extended Algebraic Data Types}}, booktitle = {FLOPS}, year = {2006}, pages = {47-64}, ee = {http://dx.doi.org/10.1007/11737414_5}, bibsource = {DBLP, http://dblp.uni-trier.de} } @phdthesis{wazny06, author = "Jeremy Richard Wazny", title = {{Type Inference and Type Error Diagnosis for Hindley/Milner with Extensions}}, school = "The university of Melbourne", year = "2006", month = "January", } @inproceedings{vytiniotis06, title = {Boxy types: inference for higher-rank types and impredicativity.}, author = {Dimitrios Vytiniotis and Stephanie Weirich and Simon L. {Peyton~Jones}}, booktitle = {ICFP}, editor = {John H. Reppy and Julia L. Lawall}, pages = {251-262}, publisher = {ACM}, year = {2006}, description = {dblp}, ee = {http://doi.acm.org/10.1145/1159803.1159838}, isbn = {1-59593-309-3}, date = {2006-12-06}, keywords = {dblp } } @inproceedings{pottier06, author = {Fran\c{c}ois Pottier and Yann R{\'e}gis-Gianas}, title = {{Stratified Type Inference for Generalized Algebraic Data Types}}, booktitle = {POPL}, year = {2006}, pages = {232-244}, ee = {http://doi.acm.org/10.1145/1111037.1111058}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{stuckey05, author = {Peter J. Stuckey and Martin Sulzmann}, title = {{Type Inference for Guarded Recursive Data Types}}, journal = {CoRR}, volume = {abs/cs/0507037}, year = {2005}, ee = {http://arxiv.org/abs/cs/0507037}, bibsource = {DBLP, http://dblp.uni-trier.de} } @misc{dijkstra04 , eprint = {papers/dijkstra04ehc-web.pdf} , title = {{EHC Web}} , author = {Dijkstra, Atze} , year = {2004} , url = {http://www.cs.uu.nl/wiki/Ehc/WebHome} , howpublished = {\verb|http://www.cs.uu.nl/wiki/Ehc/WebHome|}} @phdthesis{dijkstra05phd , eprint = {papers/dijkstra05phd.pdf} , title = {{Stepping through Haskell}} , author = {Dijkstra, Atze} , school = {Utrecht University, Department of Information and Computing Sciences} , year = {2005} , url = {http://www.cs.uu.nl/wiki/Ehc/WebHome} , howpublished = {\verb|http://www.cs.uu.nl/wiki/Ehc/WebHome|}} @article{chr98, author={Thom Fr{\"u}hwirth}, title={Theory and Practice of Constraint Handling Rules}, journal={Journal of Logic Programming, Special Issue on Constraint Logic Programming}, volume={37}, year={1998}, pages={95-138}, month={October}, number={1-3}, editor={P. Stuckey, K. Marriot}, url={citeseer.ist.psu.edu/fruhwirth98theory.html}, url={http://www.informatik.uni-muenchen.de/~fruehwir/drafts/jlp-chr1.ps.Z}, annote={HTML Version on: http://www.informatik.uni-muenchen.de/~fruehwir/jlp-chr1/index.html} } @misc{stuckey02, author = "P. Stuckey and M. Sulzmann", title = {{A Theory of Overloading}}, text = "P. J. Stuckey and M. Sulzmann. A theory of overloading. In Proc. of ICFP'02, 2002. to appear.", year = "2002", url = "citeseer.ist.psu.edu/stuckey02theory.html" } @misc{rossberg02, author = "A. Rossberg and M. Sulzmann", title = "A theory of overloading part II: Semantics and coherence", text = "A. Rossberg and M. Sulzmann. A theory of overloading part II: Semantics and coherence. Technical report, The University of Melbourne, 2002.", year = "2002", url = "citeseer.ist.psu.edu/rossberg02theory.html" } @misc{atze07, author = "Atze Dijkstra and Gerrit van den Geest and Bastiaan Heeren and S. Doaitse Swierstra", title = {{Modelling Scoped Instances with Constraint Handling Rules}}, year = "2007", url = "http://www.cs.uu.nl/wiki/bin/view/Ehc/ModellingScopedInstancesWithConstraintHandlingRules" } @mastersthesis{geest07, author = "Gerrit van den Geest", title = "Constraints for Type Class Extensions", school = "Universiteit Utrecht", year = "2007", url = "people.cs.uu.nl/bastiaan/vandengeest07thesis.pdf" } @inproceedings{jeuj09:AFP_2008, author = {Johan Jeuring and Sean Leather and Jos{\'e} Pedro Magalh{\~a}es and Alexey Rodriguez Yakushev}, title = {{Libraries for Generic Programming in Haskell}}, booktitle = {AFP}, year = {2008}, pages = {165-229}, ee = {http://dx.doi.org/10.1007/978-3-642-04652-0_4}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/afp/2008, editor = {Pieter W. M. Koopman and Rinus Plasmeijer and S. Doaitse Swierstra}, title = {Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures}, booktitle = {AFP}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5832}, year = {2009}, isbn = {978-3-642-04651-3}, ee = {http://dx.doi.org/10.1007/978-3-642-04652-0}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/tldi/BaarsSV09, author = {Arthur I. Baars and S. Doaitse Swierstra and Marcos Viera}, title = {{Typed transformations of Typed Abstract Syntax}}, booktitle = {TLDI}, year = {2009}, pages = {15-26}, ee = {http://doi.acm.org/10.1145/1481861.1481865}, crossref = {DBLP:conf/tldi/2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/tldi/2009, editor = {Andrew Kennedy and Amal Ahmed}, title = {Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009}, booktitle = {TLDI}, publisher = {ACM}, year = {2009}, isbn = {978-1-60558-420-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{uhc, author = {Atze Dijkstra and Jeroen Fokker and S. Doaitse Swierstra}, title = {{The architecture of the Utrecht Haskell compiler}}, booktitle = {Haskell}, year = {2009}, pages = {93-104}, ee = {http://doi.acm.org/10.1145/1596638.1596650}, crossref = {DBLP:conf/haskell/2009}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/haskell/2009, editor = {Stephanie Weirich}, title = {Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, Edinburgh, Scotland, UK, 3 September 2009}, booktitle = {Haskell}, publisher = {ACM}, year = {2009}, isbn = {978-1-60558-508-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/icfp/2009, editor = {Graham Hutton and Andrew P. Tolmach}, title = {Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009}, booktitle = {ICFP}, publisher = {ACM}, year = {2009}, isbn = {978-1-60558-332-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{DBLP:conf/icfp/SchrijversJSV09, author = {Tom Schrijvers and Simon L. Peyton Jones and Martin Sulzmann and Dimitrios Vytiniotis}, title = {{Complete and decidable type inference for GADTs}}, booktitle = {ICFP}, year = {2009}, pages = {341-352}, ee = {http://doi.acm.org/10.1145/1596550.1596599}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/toplas/SimonetP07, author = {Vincent Simonet and Fran\c{c}ois Pottier}, title = {{A Constraint-based Approach to Guarded Algebraic Data types}}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {29}, number = {1}, year = {2007}, ee = {http://doi.acm.org/10.1145/1180475.1180476}, bibsource = {DBLP, http://dblp.uni-trier.de} } @UNPUBLISHED{gadt-short, AUTHOR = {M. Sulzmann and T. Schrijvers and P. J. Stuckey}, TITLE = {Type Inference for {GADTs} via {Herbrand} Constraint Abduction}, NOTE = {Manuscript}, YEAR = {2006}, MONTH = {July}, PS = {http://www.cs.mu.oz.au/~sulzmann/manuscript/gadt-short.ps} } @inproceedings{pointwise, author = {{Chuan-kai} Lin and Tim Sheard}, title = {{Pointwise Generalized Algebraic Data Types}}, booktitle = {TLDI}, year = {2010}, pages = {51-62}, ee = {http://doi.acm.org/10.1145/1708016.1708024}, crossref = {DBLP:conf/tldi/2010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/tldi/2010, editor = {Andrew Kennedy and Nick Benton}, title = {Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Madrid, Spain, January 23, 2010}, booktitle = {TLDI}, publisher = {ACM}, year = {2010}, isbn = {978-1-60558-891-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{mypaper, author = {Arie Middelkoop and Atze Dijkstra and S. Doaitse Swierstra}, title = {{A Leaner Specification for Generalized Algebraic Data Types}}, booktitle = {TFP}, year = {2008}, month = {December}, volume = {9}, pages = {65-80} } @inproceedings{DBLP:conf/icfp/VytiniotisWJ08, author = {Dimitrios Vytiniotis and Stephanie Weirich and Simon L. Peyton Jones}, title = {{FPH: first-class polymorphism for Haskell}}, booktitle = {ICFP}, year = {2008}, pages = {295-306}, ee = {http://doi.acm.org/10.1145/1411204.1411246}, crossref = {DBLP:conf/icfp/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/icfp/2008, editor = {James Hook and Peter Thiemann}, title = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008}, booktitle = {ICFP}, publisher = {ACM}, year = {2008}, isbn = {978-1-59593-919-7}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{1079715, author = {Michael J. Maher}, title = {{Herbrand Constraint Abduction}}, booktitle = {LICS}, year = {2005}, pages = {397-406}, ee = {http://dx.doi.org/10.1109/LICS.2005.21}, crossref = {DBLP:conf/lics/2005}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/lics/2005, title = {20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {2005}, isbn = {0-7695-2266-1}, bibsource = {DBLP, http://dblp.uni-trier.de} } @TECHREPORT{Cheney03first-classphantom, author = {James Cheney and Ralf Hinze}, title = {{First-class Phantom Types}}, institution = {Cornell University}, year = {2003} } @article{DBLP:journals/fuin/Urzyczyn96, author = {Pawel Urzyczyn}, title = {{Positive Recursive Type Assignment}}, journal = {Fundam. Inform.}, volume = {28}, number = {1-2}, year = {1996}, pages = {197-209}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{DBLP:journals/jfp/Mogensen92, author = {Torben {\AE}. Mogensen}, title = {{Efficient Self-Interpretations in lambda Calculus}}, journal = {J. Funct. Program.}, volume = {2}, number = {3}, year = {1992}, pages = {345-363}, bibsource = {DBLP, http://dblp.uni-trier.de} }