https://wiki.haskell.org/api.php?action=feedcontributions&user=Sulzmann&feedformat=atomHaskellWiki - User contributions [en]2024-03-19T11:10:29ZUser contributionsMediaWiki 1.35.5https://wiki.haskell.org/index.php?title=Research_papers/Type_systems&diff=29128Research papers/Type systems2009-07-17T21:21:05Z<p>Sulzmann: </p>
<hr />
<div>__TOC__<br />
<br />
==Haskell semantics==<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/static-semantics.dvi.gz A static semantics for Haskell]<br />
:SL Peyton Jones and PL Wadler, (draft), Department of Computing Science, University of Glasgow, 1992. (Cited by 20)<br />
<br />
;[http://haskell.org/onlinereport/dynamic-semantics.dvi.gz A Dynamic Semantics for Haskell] <br />
:Kevin Hammond and Cordelia Hall, (draft), University of Glasgow, 1992, 23 pages.<br />
<br />
;[http://citeseer.ist.psu.edu/424440.html Typing Haskell in Haskell] <br />
:Mark P. Jones, In Proceedings of the 1999 Haskell Workshop, Paris, France, October 1999. Published in Technical Report UU-CS-1999-28, Department of Computer Science, University of Utrecht. (Cited by 66)<br />
<br />
;[http://www.pms.informatik.uni-muenchen.de/mitarbeiter/panne/haskell_libs/hsparser.html HParser]<br />
:A parser for Haskell written purely in Haskell (using the Happy parser generator).<br />
<br />
;[http://www.cse.ogi.edu/~hallgren/Talks/LHiH/ A Lexer for Haskell in Haskell]<br />
:Thomas Hallgren, PacSoft Oregon Graduate Institute, 14 January, 2002<br />
<br />
;[http://citeseer.ist.psu.edu/launchbury93natural.html A Natural Semantics for Lazy Evaluation]<br />
:John Launchbury, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, 144--154, 1993.<br />
<br />
;[http://www.cs.nott.ac.uk/~gmh/papers/11.ps A Space Semantics for Core Haskell]<br />
:Adam Bakewell. Proc. 2000 Haskell Workshop. September 2001.<br />
<br />
==Pure type systems==<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/henk.ps.gz Henk: a typed intermediate language]<br />
:SL Peyton Jones and E Meijer, Proceedings of the Types in Compilation Workshop, Amsterdam, June 1997.<br />
<br />
;[http://www.cs.uu.nl/~johanj/MSc/jwroorda/ Pure Type Systems for Functional Programming]<br />
:Jan-Willem Roorda, Masters Thesis, University of Utrecht, INF/SCR-00-13, available online, 2000<br />
<br />
==Dependent Types==<br />
<br />
;[http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf Why Dependent Types Matter]<br />
:Thorsten Altenkirch and Conor McBride and James McKinna, Manuscript, available online, April, 2005. (Cited by 7)<br />
<br />
;[http://www.informatik.uni-bonn.de/~loeh/LambdaPi.html Simply Easy! An Implementation of a Dependently Typed Lambda Calculus]<br />
:Andres Löh, Conor McBride and Wouter Swierstra, 2007.<br />
<br />
==Unboxed values==<br />
<br />
;[http://www.soi.city.ac.uk/~ross/papers/pointed.html Parametricity and Unboxing with Unpointed Types]<br />
:John Launchbury and Ross Paterson, European Symposium on Programming, LNCS, vol. 1058, pp. 204-218, Springer, Linkping, Sweden, 1996.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/unboxed-values.ps.Z Unboxed values as first class citizens]<br />
:SL Peyton Jones and J Launchbury, Functional Programming Languages and Computer Architecture (FPCA'91), Boston, LNCS 523, Springer Verlag, Sept 1991, pp636-666. (Cited by 105)<br />
<br />
==Modules==<br />
<br />
;[http://www.cse.ogi.edu/~diatchki/papers/modules98.pdf A Formal Specification of the Haskell 98 Module System]<br />
:Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren. Proceedings of the 2002 ACM SIGPLAN workshop on Haskell. Pittsburgh, Pennsylvania. 17 - 28 2002 ISBN 1-58113-605-6 (Cited by 12)<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/first-class-modules/index.htm First class modules for Haskell]<br />
:Mark Shields and Simon Peyton Jones; FOOL'02.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/Nicklisch-modules.ps.gz An exploration of modular programs]<br />
:Electronic proceedings of the 1996 Glasgow Functional Programming Workshop, J Nicklisch and SL Peyton Jones, Ullapool, July 1996.<br />
<br />
==Exceptions==<br />
<br />
;[http://www.haskell.org/~simonmar/papers/ext-exceptions.pdf An Extensible Dynamically-Typed Hierarchy of Exceptions]<br />
:Simon Marlow. Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, Portland, Oregon, ACM Press, September 2006<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/imprecise-exn-sem.htm Imprecise Exceptions, Co-Inductively]<br />
:Andy Moran, Soeren Lassen, and Simon Peyton Jones. HOOTS'99.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/imprecise-exn.htm A semantics for imprecise exceptions]<br />
:Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow, Fergus Henderson. Proc Programming Language Design and Implementation (PLDI'99), Atlanta.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/asynch-exns.htm Asynchronous exceptions in Haskell]<br />
:Simon Marlow, Simon Peyton Jones, Andy Moran and John Reppy, PLDI'01.<br />
<br />
;[http://www.reid-consulting-uk.ltd.uk/alastair/publications/except6.ps.gz Handling Exceptions in Haskell]<br />
:A. Reid, Research Report YALEU/DCS/RR-1175, Yale University, August, 1998<br />
<br />
==Lexically scoped type variables==<br />
<br />
;[http://research.microsoft.com/%7Esimonpj/papers/scoped%2Dtyvars/ Lexically scoped type variables]<br />
:Simon Peyton Jones and Mark Shields. 2004.<br />
<br />
==Records==<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/records.htm Lightweight Extensible Records for Haskell]<br />
:Mark Jones and Simon Peyton Jones, Haskell Workshop 1999.<br />
<br />
;[http://www.cs.uu.nl/~daan/download/papers/scopedlabels.pdf Extensible records with scoped labels]<br />
:Daan Leijen. The 2005 Symposium on Trends in Functional Programming (TFP'05), Tallin, Estonia, September 2005.<br />
<br />
;[http://www.cs.uu.nl/~daan/download/papers/fclabels.pdf First-class labels for extensible rows]<br />
:Daan Leijen. Technical Report UU-CS-2004-51, Departement of Computer Science, Universiteit Utrecht, 2004.<br />
<br />
;[http://www.reid-consulting-uk.ltd.uk/alastair/publications/h-wkshop95a/index.html Haskell Records]<br />
:J. Peterson, A. Reid, Proceedings of the Haskell Workshop, La Jolla, June 1995. <br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/96-3.ps.gz A Polymorphic Type System for Extensible Records and Variants]<br />
:Benedict R. Gaster and Mark P. Jones. Department of Computer Science, University of Nottingham. Technical report NOTTCS-TR-96-3. November 1996.<br />
<br />
==Meta programming==<br />
<br />
;[http://research.microsoft.com/copyright/accept.asp?path=/users/simonpj/papers/dyntyping.ps.gz&pub=ACM Dynamic typing as staged type inference]<br />
:MB Shields, T Sheard, and SL Peyton Jones, POPL98.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/meta-haskell/index.htm Template meta-programming for Haskell]<br />
:Tim Sheard and Simon Peyton Jones, Proceedings of the Haskell Workshop, Pittsburgh, 2002<br />
<br />
;[http://www.cse.unsw.edu.au/~chak/papers/SCK04.html Optimising Embedded DSLs using Template Haskell]<br />
:Sean Seefried, Manuel M. T. Chakravarty, and Gabriele Keller. In Gabor Karsai and Eelco Visser, editors, Third International Conference on Generative Programming and Component Engineering (GPCE'04), LNCS 3286, Springer-Verlag, pages 186-205, 2004. [An earlier draft was presented at the IFL 2003 - 15th International Workshop on the Implementation of Functional Languages, 2003.<br />
<br />
;[http://www.haskell.org/th/papers/Unrolling_and_Simplifying_Expressions_with_Template_Haskell.ps Unrolling and Simplifying Expressions with Template Haskell]<br />
:Ian Lynagh, May 2003.<br />
<br />
;[http://www.haskell.org/th/papers/hlpp.ps Automatic skeletons in Template Haskell]<br />
:Kevin Hammond, Jost Berthold and Rita Loogen, June 2003. Proceedings of 2003 Workshop on High Level Parallel Programming, Paris, France<br />
<br />
;[http://www.haskell.org/th/papers/Typing_Template_Haskell__Soft_Types.ps Typing Template Haskell: Soft Types]<br />
:Ian Lynagh, August 2004.<br />
<br />
==Dynamic typing==<br />
<br />
;[http://www.cs.uu.nl/groups/ST/stbib/swierstra-by-year/BaSw02.bib Typing dynamic typing]<br />
:A. I. Baars and S. D. Swierstra. In S. Peyton Jones, editor, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pages 157--166. ACM Press, 2002<br />
<br />
==Parametricity==<br />
<br />
;[http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps.gz Theorems for free!]<br />
:Philip Wadler. 4'th International Conference on Functional Programming and Computer Architecture, London, September 1989.<br />
<br />
;[http://www.soi.city.ac.uk/~ross/papers/pointed.html Parametricity and Unboxing with Unpointed Types]<br />
:John Launchbury and Ross Paterson, European Symposium on Programming, LNCS, vol. 1058, pp. 204-218, Springer, Linkping, Sweden, 1996.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/seqFinal.pdf The Impact of seq on Free Theorems-Based Program Transformations]<br />
:Patricia Johann and Janis Voigtländer, Fundamenta Informaticae, vol. 69(1-2), pp. 63-102, 2006.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/TCS.pdf Selective strictness and parametricity in structural operational semantics, inequationally]<br />
:Janis Voigtländer and Patricia Johann, Theoretical Computer Science, vol. 388(1-3), pp. 290-318, 2007.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/pepm09-voigtlaender.pdf Proving Correctness via Free Theorems: The Case of the destroy/build-Rule]<br />
:Janis Voigtländer. Workshop on Partial Evaluation and Program Manipulation (PEPM'08), Proceedings, ACM Press, 2008.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/iandc.pdf A family of syntactic logical relations for the semantics of Haskell-like languages]<br />
:Patricia Johann and Janis Voigtländer, Information and Computation, vol. 207(2), pp. 341-368, 2009.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/tlca09.pdf Parametricity for Haskell with Imprecise Error Semantics]<br />
:Florian Stenger and Janis Voigtländer. International Conference on Typed Lambda Calculi and Applications (TLCA'09), Proceedings, Springer-Verlag, 2009.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/icfp09.pdf Free Theorems Involving Type Constructor Classes]<br />
:Janis Voigtländer. International Conference on Functional Programming (ICFP'09), Proceedings, ACM Press, 2009.<br />
<br />
<br />
==Type classes==<br />
<br />
;[http://homepages.inf.ed.ac.uk/wadler/papers/class/class.ps.gz How to make ad-hoc polymorphism less ad hoc]<br />
:Philip Wadler and Stephen Blott. 16'th Symposium on Principles of Programming Languages, ACM Press, Austin, Texas, January 1989.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/classhask.ps.gz Type classes in Haskell, CV Hall, K Hammond, SL Peyton Jones, and PL Wadler]<br />
:European Symposium On Programming, LNCS 788, Springer Verlag, pp. 241-256, April 1994. (Cited by 131)<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/pldi93.html Implementing Type Classes]<br />
:John Peterson and Mark P. Jones, In Proceedings of ACM SIGPLAN Symposium on Programming Language Design and Implementation, ACM SIGPLAN, June 1993. (Cited by 40)<br />
<br />
;[http://www.cs.chalmers.se/pub/cs-reports/papers/overload-fpca-93.ps.Z Implementing Haskell overloading]<br />
:Lennart Augustsson, 1993. FPCA. 65-73<br />
<br />
;[http://web.cecs.pdx.edu/~mpj/pubs/springschool.html Functional Programming with Overloading and Higher-Order Polymorphism]<br />
:Mark P. Jones, First International Spring School on Advanced Functional Programming Techniques, Baastad, Sweden, Springer-Verlag Lecture Notes in Computer Science 925, May 1995.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/type-class-design-space Type classes: exploring the design space]<br />
:Simon Peyton Jones, Mark Jones, Erik Meijer, Haskell Workshop 1997.<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/fpca93.html A system of constructor classes: overloading and implicit higher-order polymorphism]<br />
:Mark P. Jones, In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhagen, Denmark, June 1993.<br />
<br />
;[http://homepages.inf.ed.ac.uk/wadler/papers/overload2/overload2.ps.gz A second look at overloading]<br />
:Martin Odersky, Philip Wadler, Martin Wehr. 7'th International Conference on Functional Programming and Computer Architecture, ACM Press, San Diego, California, June 1995.<br />
<br />
;[http://citeseer.ist.psu.edu/laufer94combining.html Combining Type Classes and Existential Types]<br />
:Konstantin Laufer, Proceedings of the Latin American Informatic Conference (PANEL), 1994<br />
<br />
;[http://citeseer.ist.psu.edu/aufer95type.html Type Classes with Existential Types]<br />
:Konstantin Laufer, Journal of Functional Programming, 1996, May<br />
<br />
;[http://www.cse.unsw.edu.au/~chak/papers/DHCK06.html Modular Type Classes]<br />
:Derek Dreyer, Robert Harper, Manuel M.T. Chakravarty and Gabriele Keller, 2006<br />
<br />
;[http://www.informatik.uni-bonn.de/~ralf/hw2001/4.pdf Named instances for Haskell type classes]<br />
:W Kahl, J Scheffczyk - Proc. Haskell Workshop, 2001 (Cited by 12)<br />
<br />
===Deriving type classes===<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/derive.htm Derivable Type classes] <br />
:Ralf Hinze and Simon Peyton Jones, Haskell Workshop 2000.<br />
<br />
;[http://www.cis.upenn.edu/~sweirich/RepLib/ RepLib: A Library for Derivable Type Classes]<br />
:Stephanie Weirich 2006<br />
<br />
===Applications of type classes===<br />
<br />
;[http://okmij.org/ftp/Haskell/number-parameterized-types.html Number-parameterized types]<br />
:Oleg Kiselyov, The Monad.Reader. IssueFive. Oct 2nd, 2005<br />
<br />
;[http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/typecase.pdf TypeCase: a design pattern for type-indexed functions]<br />
:Bruno C. d. S. Oliveira, Jeremy Gibbons. Proceedings of the 2005 ACM SIGPLAN workshop on Haskell. Tallinn, Estonia. 98 - 109, 2005 ISBN:1-59593-071-X<br />
<br />
;[http://okmij.org/ftp/Haskell/types.html#Prepose Functional pearl: implicit configurations--or, type classes reflect the values of types]<br />
:Oleg Kiselyov, Chung-chieh Shan, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, Snowbird, Utah, USA, 2004 ISBN 1-58113-850-4<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/extract-typeclassproofs.pdf Extracting Programs from Type Class Proofs]<br />
:Martin Sulzmann, 2006<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.ps Co-induction and Type Improvement in Type Class Proofs]<br />
:Martin Sulzmann, Jeremy Wazny and Peter J. Stuckey. 2005<br />
<br />
;[http://www.cs.nott.ac.uk/~ctm/faking.ps.gz Faking It (Simulating Dependent Types in Haskell)]<br />
:Conor McBride, Journal of Functional Programming, 12(4&5):375-392, July 2002<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/aophaskell.ps.gz Aspect-Oriented Programming with Type Classes]<br />
:Martin Sulzmann and Meng Wang, 2006.<br />
<br />
;[http://wwwtcs.inf.tu-dresden.de/~voigt/mpc08.pdf Asymptotic Improvement of Computations over Free Monads]<br />
:Janis Voigtländer. Mathematics of Program Construction (MPC'08), Proceedings, LNCS 5133:388-403, Springer-Verlag, 2008.<br />
<br />
<br />
==Undecidable instances==<br />
<br />
;[http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html#undecidable-instances Undecidable instances]<br />
:GHC User's Guide.<br />
<br />
==Multi-parameter type classes==<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/ghc-mptc-inf.ps Principal Type Inference for GHC-Style Multi-Parameter Type Classes]<br />
:Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey. In APLAS'06.<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/mptc-inf-old.pdf Type Inference for Multi-Parameter Type Classes]<br />
:Martin Sulzmann and Peter J. Stuckey. 2005<br />
<br />
;[http://ostrich.lcs.mit.edu/cgi-bin/pickbib?jfp::DugganO2002 Type-checking multi-parameter type classes]<br />
:Dominic Duggan and John Ophel, Journal of Functional Programming, 12(2):133-158, March 2002<br />
<br />
==Functional dependencies==<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/fundeps.html Type Classes with Functional Dependencies]<br />
:Mark P. Jones, In Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany, March 2000, Springer-Verlag LNCS 1782.<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/fd-chr/index.htm Sound and Decidable Type Inference for Functional Dependencies]<br />
:Gregory J. Duck, Simon Peyton Jones, Peter J. Stuckey, and Martin Sulzmann, European Symposium on Programming 2004 (ESOP'04).<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/jfp-fds-revised.pdf Understanding Functional Dependencies via Constraint Handling Rules]<br />
:Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones and Peter J. Stuckey.j To appear in Journal of Functional Programming. 2006<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/afds.ps Associated Functional Dependencies]<br />
:Martin Sulzmann and Edmund Soon Lee Lam. 2005<br />
<br />
==Constraint Handling Rules==<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/aplas06-invited.pdf Type Processing by Constraint Reasoning]<br />
:Peter J. Stuckey, Martin Sulzmann and Jeremy Wazny, In APLAS'06.<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/chr-stm.ps A Concurrent Constraint Handling Rules Implementation in Haskell with Software Transactional Memory]<br />
:Edmund S.L. Lam and Martin Sulzmann<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/chr06-observable.ps Observable Confluence for Constraint Handling Rules]<br />
:Gregory J. Duck, Peter J. Stuckey and Martin Sulzmann<br />
<br />
==Generalised Algebraic Data Types (GADTs)==<br />
<br />
;[http://research.microsoft.com/~simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs]<br />
:Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. Submitted to PLDI 2005<br />
<br />
;[http://www.cis.upenn.edu/~geoffw/research/papers/MS-CIS-05-26.pdf Wobbly types: type inference for generalised algebraic data types]<br />
:S Peyton Jones, G. Washburn, and S. Weirich. 2004.<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/simple-translate-gadts.ps Translating Generalized Algebraic Data Types to System F]<br />
:Martin Sulzmann and Meng Wang. 2005<br />
<br />
;[http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf Stratified type inference for generalized algebraic data types]<br />
:François Pottier and Yann Régis-Gianas, 2006<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/gadt-short.ps Type Inference for GADTs via Herbrand Constraint Abduction]<br />
:Martin Sulzmann, Tom Schrijvers and Peter J. Stuckey, 2006 <br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/publications/tr-eadt.ps.gz A Framework for Extended Algebraic Data Types]<br />
:Martin Sulzmann, Jeremy Wazny and Peter J. Stuckey, 2006<br />
<br />
;[http://www.cs.kuleuven.be/~toms/Research/papers/implication_constraints.pdf Complete and Decidable Type Inference for GADTs]<br />
:Tom Schrijvers, Simon Peyton-Jones, Martin Sulzmann and Dimitrios Vytiniotis, 2009.<br />
<br />
See also the [[GADT]] page.<br />
<br />
==Parametric Regular Data Types==<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/parametric-regular.ps Type Inference and Compilation for Parametric Regular Data Types]<br />
:Martin Sulzmann and Kenny Zhuo Ming Lu, 2006<br />
<br />
;[http://www.cs.mu.oz.au/~sulzmann/manuscript/haskell-xduce.ps The Marriage of Haskell and XDuce]<br />
:Martin Sulzmann and Kenny Zhuo Ming Lu<br />
<br />
==Type Families and Associated types==<br />
<br />
;[http://www.haskell.org/~simonmar/papers/assoc.pdf Associated types with class]<br />
:Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, Simon Marlow) POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pages 1--13, Long Beach, California, USA, ACM Press, 2005<br />
<br />
;[http://www.cse.unsw.edu.au/~chak/papers/CKP05.html Associated Type Synonyms]<br />
:Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. In Proceedings of The Tenth ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 241-253, 2005.<br />
<br />
;[http://www.informatik.uni-freiburg.de/~wehr/diplom ML Modules and Haskell Type Classes: A Constructive Comparison]<br />
:Stefan Wehr Diplomarbeit. Albert-Ludwigs-Universitt Freiburg, Fakultt fr Angewandte Wissenschaften, Institut fr Informatik, November 2005. <br />
<br />
;[http://www.cse.unsw.edu.au/~chak/papers/SCP06.html System F with Type Equality Coercions]<br />
:Martin Sulzmann, Manuel M. T. Chakravarty, and Simon Peyton Jones.<br />
<br />
;[http://www.cs.kuleuven.be/~toms/Research/papers/type_functions.pdf Towards Open Type Functions for Haskell]<br />
:Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, and Manuel Chakravarty. In Proceedings of IFL' 07, Freiburg, Germany, 2007.<br />
<br />
;[http://www.cs.kuleuven.be/~toms/Research/papers/draft_type_functions_2008.pdf Type Checking with Open Type Functions for Haskell]<br />
:Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. In Proceedings of ICFP' 08, Victoria, Canada, 2008.<br />
<br />
<br />
==Arbitrary-rank polymorphism==<br />
<br />
;[http://www.ubka.uni-karlsruhe.de/vvv/1996/informatik/81/81.pdf.gz Putting type annotations to work]<br />
:Martin Odersky and Konstantin Läufer. Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. St. Petersburg Beach, Florida, United States. 54 - 67 1996 ISBN 0-89791-769-3<br />
<br />
;[http://journals.cambridge.org/production/action/cjoGetFulltext%3Ffulltextid%3D445910 Practical type inference for arbitrary-rank types]<br />
:SP Jones, M Shields - Submitted to the Journal of Functional Programming, 2005<br />
<br />
==Phantom types==<br />
<br />
;[http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901 First-class phantom types]<br />
:James Cheney and Ralf Hinze. Technical Report TR2003-1901, Cornell University, 2003.<br />
<br />
;[http://ttic.uchicago.edu/~fluet/research/phantom-subtyping/jfp06/jfp06.pdf Phantom Types and Subtyping]<br />
:Matthew Fluet and Riccardo Pucella. Submitted to the Journal of Functional Programming, 2006.<br />
<br />
==Implicit parameters==<br />
<br />
;[http://www.cse.ogi.edu/~mbs/pub/implicit_parameters/implicit.ps Implicit Parameters: Dynamic Scoping with Static Types]<br />
:Jeffrey Lewis, Mark Shields, Erik Meijer and John Launchbury. POPL'00. 2000.<br />
<br />
;[http://www.cs.chalmers.se/~rjmh/Globals.ps Global variables in Haskell]<br />
:John Hughes. J. Funct. Program. 14(5): 489-502 (2004) <br />
<br />
;[http://www.cs.uu.nl/pub/RUU/CS/techreps/CS-2004/2004-059.pdf Explicit Implicit Parameters]<br />
:A. Dijkstra and S. D. Swierstra. UU-CS 2004-059, 2004.<br />
<br />
==Object oriented Haskell==<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/oo-haskell/index.htm Object-Oriented Style Overloading for Haskell] <br />
:Mark Shields and Simon Peyton Jones; BABEL workshop '01.<br />
<br />
;[http://www.cse.unsw.edu.au/~chak/papers/PC03.html Interfacing Haskell with Object-Oriented Languages]<br />
:Andr T. H. Pang and Manuel M. T. Chakravarty. In Greg Michaelson and Phil Trinder, editors, Implementation of Functional Languages: 15th International Workshop, IFL 2003, Edinburgh, UK, September 8-11, 2003, Revised Papers, LNCS 3145, Springer-Verlag, pages 20-36, 2004. <br />
<br />
;[http://citeseer.ist.psu.edu/118134.html Haskell++: An Object-Oriented Extension of Haskell]<br />
:Jan Sparud and John Hughes. Haskell Workshop 1995<br />
<br />
;[http://homepages.cwi.nl/~ralf/OOHaskell/ Haskell's overlooked object system]<br />
:Oleg Kiselyov and Ralf Lämmel, submitted for journal publication; online since 30 Sep. 2004;<br />
<br />
==Restricted Datatypes==<br />
<br />
;[http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps Restricted datatypes]<br />
:John Hughes. 1999 Haskell workshop<br />
<br />
==Patterns==<br />
<br />
;[http://www.cs.yale.edu/homes/tullsen/patterns.ps First Class Patterns]<br />
:Mark Tullsen. Practical Aspects of Declarative Languages, Second International Workshop, PADL 2000. volume 1753 of Lecture Notes in Computer Science. January 2000. <br />
<br />
===Pattern guards===<br />
<br />
;[http://research.microsoft.com/~simonpj/Papers/pat.htm Pattern Guards and Transformational Patterns]<br />
:Martin Erwig and Simon Peyton Jones; Haskell Workshop 2000.<br />
<br />
;[http://research.microsoft.com/Users/simonpj/Haskell/guards.html A new view of guards]<br />
:Simon Peyton Jones, April 1997<br />
<br />
===Views===<br />
<br />
;[http://www.haskell.org/development/views.html Views: An Extension to Haskell Pattern Matching]<br />
:Warren Burton, Erik Meijer, Patrick Sansom, Simon Thompson and Phil Wadler.<br />
<br />
;[http://homepages.inf.ed.ac.uk/wadler/papers/view/view.ps.gz Views: A way for pattern matching to cohabit with data abstraction]<br />
:POPL 14 (1987), 307-313.<br />
<br />
==Qualified types==<br />
<br />
;[http://haskell.readscheme.org/servlets/cite.ss?pattern=mpj-jones1994a Qualified Types: Theory and Practice]<br />
:Mark P. Jones. PhD. Thesis. Yale University. November 1994.<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/fpca95.ps Simplifying and Improving Qualified Types]<br />
:Mark P. Jones. FPCA '95: Conference on Functional Programming Languages and Computer Architecture. June 1995.<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/RR-1040.ps Simplifying and Improving Qualified Types]<br />
:Mark P. Jones. Yale University. Research Report YALEU/DCS/RR-1040. June 1994.<br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/RR-989.ps Coherence for qualified types]<br />
:Mark P. Jones. Yale University. Research Report YALEU/DCS/RR-989. September 1993. <br />
<br />
;[http://www.cse.ogi.edu/~mpj/pubs/rev-qual-types.ps A theory of qualified types]<br />
:Mark P. Jones. ESOP '92: European Symposium on Programming. Lecture Notes in Computer Science, 582. February 1992. (Cited by 68)<br />
<br />
==Polymorphic recursion==<br />
<br />
;[http://portal.acm.org/citation.cfm%3Fcoll%3DGUIDE%26dl%3DGUIDE%26id%3D169692 Type inference with polymorphic recursion]<br />
:F Henglein - ACM Transactions on Programming Languages and Systems (1993)<br />
<br />
;[http://www.jucs.org/jucs_9_8/practical_type_inference_for/paper.pdf Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell]<br />
:C Vasconcellos, L Figueiredo, C Camarao - Journal of Universal Computer Science, 2003<br />
<br />
;[http://www.dcc.ufmg.br/~camarao/ml0-impl.ps Type Inference for Polymorphic Recursive Definitions: a Specification in Haskell]<br />
:L Figueiredo, C Camarao<br />
<br />
[[Category:Research]]<br />
[[Category:Type-level programming]]</div>Sulzmannhttps://wiki.haskell.org/index.php?title=Generalised_algebraic_datatype&diff=29127Generalised algebraic datatype2009-07-17T20:16:50Z<p>Sulzmann: </p>
<hr />
<div>== Papers ==<br />
<br />
See also [[Research papers/Type systems#Generalised Algebraic Data Types|research papers on type systems]].<br />
<br />
* A short description on generalised algebraic datatypes here [http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt as GHC language features].<br />
* Another description with links on [http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs Haskell' wiki].<br />
* [http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901 First-Class Phantom Types] by James Cheney and Ralf Hinze<br />
* [http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf Stratified type inference for generalized algebraic data types] by François Pottier and Yann Régis-Gianas. It contains also a lot of links to other papers on GADTs.<br />
* [http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs] by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. (Revised April 2006.)<br />
* [http://www.cs.mu.oz.au/~sulzmann/manuscript/simple-translate-gadts.ps Translating Generalized Algebraic Data Types to System F] written by [http://www.cs.mu.oz.au/~sulzmann/ Martin Sulzmann] and Meng Wang. [http://www.cs.mu.oz.au/~sulzmann/2005.html Many other papers]. The talk mentions also the notion of [[phantom type]], and [[existential type]], and [[type witness]].<br />
<br />
== Motivating example ==<br />
<br />
Generalised Algebraic Datatypes (GADTs) are datatypes for which a constructor has a non standard type. Indeed, in type systems incorporating GADTs, there are very few restrictions on the type that the data constructors can take. To show you how this could be useful, we will implement an evaluator for the typed SK calculus. Note that the K combinator is operationally similar to<br />
<math>\lambda\;x\;y\;.\;x</math><br />
and, similarly, S is similar to the combinator<br />
<math>\lambda\;x\;y\;z\;.\;x\;z\;(\;y\;z\;)</math><br />
which, in simply typed lambda calculus, have types<br />
<math>a \rightarrow b \rightarrow a </math><br />
and<br />
<math>(a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c </math><br />
Without GADTs we would have to write something like this:<br />
<haskell><br />
data Term = K | S | Term :@ Term <br />
infixl 6 :@<br />
</haskell><br />
With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so:<br />
<haskell><br />
data Term x where<br />
K :: Term (a -> b -> a)<br />
S :: Term ((a -> b -> c) -> (a -> b) -> a -> c)<br />
Const :: a -> Term a<br />
(:@) :: Term (a -> b) -> (Term a) -> Term b<br />
infixl 6 :@<br />
</haskell><br />
now we can write a small step evaluator:<br />
<haskell><br />
eval::Term a -> Term a<br />
eval (K :@ x :@ y) = x<br />
eval (S :@ x :@ y :@ z) = x :@ z :@ (y :@ z)<br />
eval x = x<br />
</haskell><br />
Since the types of the so-called object language, being the typed SK calculus, are mimicked by the type system in our meta language, being Haskell, we have a pretty convincing argument that the evaluator won't mangle our types. We say that typing is preserved under evaluation (preservation.) Note that this is an argument and not a proof.<br />
<br />
This, however, comes at a price: let's see what happens when you try to convert strings into our object language:<br />
<haskell><br />
parse "K" = K<br />
parse "S" = S<br />
</haskell><br />
you'll get a nasty error like so:<br />
<br />
Occurs check: cannot construct the infinite type: c = b -> c<br />
Expected type: Term ((a -> b -> c) -> (a -> b) -> a -> b -> c)<br />
Inferred type: Term ((a -> b -> c) -> (a -> b) -> a -> c)<br />
In the definition of `foo': foo "S" = S<br />
<br />
One could, however, reason that parse has type: <hask>String -> exists a. Term a</hask>, see also [[Existential type]].<br />
<br />
== Example with lists ==<br />
<br />
here's another, smaller example:<br />
<haskell><br />
data Empty<br />
data NonEmpty<br />
data List x y where<br />
Nil :: List a Empty<br />
Cons:: a -> List a b -> List a NonEmpty<br />
<br />
safeHead:: List x NonEmpty -> x<br />
safeHead (Cons a b) = a<br />
</haskell><br />
<br />
now safeHead can only be applied to non empty lists, and will never evaluate to bottom. This too comes at a cost; consider the function:<br />
<br />
<haskell><br />
silly 0 = Nil<br />
silly 1 = Cons 1 Nil<br />
</haskell><br />
<br />
yields an objection from ghc:<br />
Couldn't match `Empty' against `NonEmpty'<br />
Expected type: List a Empty<br />
Inferred type: List a NonEmpty<br />
In the application `Cons 1 Nil'<br />
In the definition of `silly': silly 1 = Cons 1 Nil<br />
<br />
== Parsing Example ==<br />
<br />
Note that GADTs provide a rather nice platform for embedded domain specific languages. In particular, they allow an [[EDSL]] to use Haskell's type system for its own purposes. As a simple example, we might have an EDSL for simple (regexp-like) parsers that looks something like:<br />
<br />
<haskell><br />
data Parser tok a where<br />
Zero :: Parser tok ()<br />
One :: Parser tok ()<br />
Check :: (tok -> Bool) -> Parser tok tok<br />
Satisfy :: ([tok] -> Bool) -> Parser tok [tok]<br />
Push :: tok -> Parser tok a -> Parser tok a<br />
Plus :: Parser tok a -> Parser tok b -> Parser tok (Either a b)<br />
Times :: Parser tok a -> Parser tok b -> Parser tok (a,b)<br />
Star :: Parser tok a -> Parser tok [a]<br />
</haskell><br />
<br />
An evaluator/parser is then straightforward. Below it's written monadically for<br />
convenience, but this also means that we could generalise the return type to being in any MonadPlus. Note that an advantage of this representation which we don't show here is that we could also write a function which applies algebraic rules to the structure to try to simplify the parser before running it. (Though if we were really concerned with efficiency, we'd probably also need a couple more primitives.)<br />
<br />
<haskell><br />
parse :: Parser tok a -> [tok] -> Maybe a<br />
<br />
-- Zero always fails.<br />
parse Zero ts = mzero<br />
<br />
-- One matches only the empty string.<br />
parse One [] = return ()<br />
parse One _ = mzero<br />
<br />
-- Check p matches a string with exactly one token t such that p t holds.<br />
parse (Check p) [t] = if p t then return t else mzero<br />
parse (Check p) _ = mzero<br />
<br />
-- Satisfy p any string such that p ts holds.<br />
parse (Satisfy p) xs = if p xs then return xs else mzero<br />
<br />
-- Push t x matches a string ts when x matches (t:ts).<br />
parse (Push t x) ts = parse x (t:ts)<br />
<br />
-- Plus x y matches when either x or y does.<br />
parse (Plus x y) ts = liftM Left (parse x ts) `mplus` liftM Right (parse y ts)<br />
<br />
-- Times x y matches the concatenation of x and y.<br />
parse (Times x y) [] = liftM2 (,) (parse x []) (parse y [])<br />
parse (Times x y) (t:ts) = <br />
parse (Times (Push t x) y) ts `mplus`<br />
liftM2 (,) (parse x []) (parse y (t:ts))<br />
<br />
-- Star x matches zero or more copies of x.<br />
parse (Star x) [] = return []<br />
parse (Star x) (t:ts) = do<br />
(v,vs) <- parse (Times x (Star x)) (t:ts)<br />
return (v:vs)<br />
</haskell><br />
<br />
Finally, we might define some examples:<br />
<br />
<haskell><br />
token x = Check (== x)<br />
string xs = Satisfy (== xs)<br />
<br />
p = Times (token 'a') (token 'b')<br />
p1 = Times (Star (token 'a')) (Star (token 'b'))<br />
p2 = Star p1<br />
<br />
blocks :: (Eq tok) => Parser tok [[tok]]<br />
blocks = Star (Satisfy allEqual)<br />
where allEqual xs = and (zipWith (==) xs (drop 1 xs))<br />
<br />
evenOdd = Plus (Star (Times (Check even) (Check odd)))<br />
(Star (Times (Check odd) (Check even)))<br />
<br />
</haskell><br />
<br />
Testing this in ghci:<br />
<pre><br />
*Main> parse p "ab"<br />
Just ('a','b')<br />
*Main> parse p "ac"<br />
Nothing<br />
*Main> parse p1 "aaabbbb"<br />
Just ("aaa","bbbb")<br />
*Main> parse p2 "aaabbbbaabbbbbbbaaabbabab"<br />
Just [("aaa","bbbb"),("aa","bbbbbbb"),("aaa","bb"),("a","b"),("a","b")]<br />
*Main> :t p2<br />
p2 :: Parser Char [([Char], [Char])]<br />
*Main> parse blocks "aaaabbbbbbbbcccccddd"<br />
Just ["aaaa","bbbbbbbb","ccccc","ddd"]<br />
*Main> parse evenOdd [0..9]<br />
Just (Left [(0,1),(2,3),(4,5),(6,7),(8,9)])<br />
*Main> parse evenOdd [1..10]<br />
Just (Right [(1,2),(3,4),(5,6),(7,8),(9,10)])<br />
<br />
</pre><br />
<br />
== Projects containing GADTs ==<br />
<br />
Papers on [[Libraries and tools/Database interfaces/HaskellDB|HaskellDB]] describe problems when GADTs can help (but HaskellDB solves these problems with [[phantom type]]s).<br />
<br />
[[Darcs]] represents motivating examples for GADTs, too -- and uses them.<br />
The motivations are described in David Roundy's FOSDEM slides (Implementing the Darcs Patch Formalism and Verifying It) (see p. 11, 13--14.). The talk mentions also the notions of [[phantom type]], and [[existential type]], and [[type witness]] (see p. 15).<br />
<br />
== See also ==<br />
<br />
* [[Algebraic data type]]<br />
* [[GADTs for dummies]]<br />
<br />
<br />
[[Category:Glossary]]<br />
[[Category:Language extensions]]</div>Sulzmannhttps://wiki.haskell.org/index.php?title=Generalised_algebraic_datatype&diff=29126Generalised algebraic datatype2009-07-17T20:16:09Z<p>Sulzmann: </p>
<hr />
<div>== Papers ==<br />
<br />
See also [[Research papers/Type systems#Generalised Algebraic Data Types|research papers on type systems]].<br />
<br />
* A short description on generalised algebraic datatypes here [http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt as GHC language features].<br />
* Another description with links on [http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs Haskell' wiki].<br />
* [http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901 First-Class Phantom Types] by James Cheney and Ralf Hinze<br />
* [http://cristal.inria.fr/~fpottier/publis/pottier-regis-gianas-05.pdf Stratified type inference for generalized algebraic data types] by François Pottier and Yann Régis-Gianas. It contains also a lot of links to other papers on GADTs.<br />
* [http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm Simple unification-based type inference for GADTs] by Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn. (Revised April 2006.)<br />
* [http://www.comp.nus.edu.sg/~sulzmann/manuscript/simple-translate-gadts.ps Translating Generalized Algebraic Data Types to System F] written by [http://www.cs.mu.oz.au/~sulzmann/ Martin Sulzmann] and Meng Wang. [http://www.cs.mu.oz.au/~sulzmann/2005.html Many other papers]. The talk mentions also the notion of [[phantom type]], and [[existential type]], and [[type witness]].<br />
<br />
== Motivating example ==<br />
<br />
Generalised Algebraic Datatypes (GADTs) are datatypes for which a constructor has a non standard type. Indeed, in type systems incorporating GADTs, there are very few restrictions on the type that the data constructors can take. To show you how this could be useful, we will implement an evaluator for the typed SK calculus. Note that the K combinator is operationally similar to<br />
<math>\lambda\;x\;y\;.\;x</math><br />
and, similarly, S is similar to the combinator<br />
<math>\lambda\;x\;y\;z\;.\;x\;z\;(\;y\;z\;)</math><br />
which, in simply typed lambda calculus, have types<br />
<math>a \rightarrow b \rightarrow a </math><br />
and<br />
<math>(a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c </math><br />
Without GADTs we would have to write something like this:<br />
<haskell><br />
data Term = K | S | Term :@ Term <br />
infixl 6 :@<br />
</haskell><br />
With GADTs, however, we can have the terms carry around more type information and create more interesting terms, like so:<br />
<haskell><br />
data Term x where<br />
K :: Term (a -> b -> a)<br />
S :: Term ((a -> b -> c) -> (a -> b) -> a -> c)<br />
Const :: a -> Term a<br />
(:@) :: Term (a -> b) -> (Term a) -> Term b<br />
infixl 6 :@<br />
</haskell><br />
now we can write a small step evaluator:<br />
<haskell><br />
eval::Term a -> Term a<br />
eval (K :@ x :@ y) = x<br />
eval (S :@ x :@ y :@ z) = x :@ z :@ (y :@ z)<br />
eval x = x<br />
</haskell><br />
Since the types of the so-called object language, being the typed SK calculus, are mimicked by the type system in our meta language, being Haskell, we have a pretty convincing argument that the evaluator won't mangle our types. We say that typing is preserved under evaluation (preservation.) Note that this is an argument and not a proof.<br />
<br />
This, however, comes at a price: let's see what happens when you try to convert strings into our object language:<br />
<haskell><br />
parse "K" = K<br />
parse "S" = S<br />
</haskell><br />
you'll get a nasty error like so:<br />
<br />
Occurs check: cannot construct the infinite type: c = b -> c<br />
Expected type: Term ((a -> b -> c) -> (a -> b) -> a -> b -> c)<br />
Inferred type: Term ((a -> b -> c) -> (a -> b) -> a -> c)<br />
In the definition of `foo': foo "S" = S<br />
<br />
One could, however, reason that parse has type: <hask>String -> exists a. Term a</hask>, see also [[Existential type]].<br />
<br />
== Example with lists ==<br />
<br />
here's another, smaller example:<br />
<haskell><br />
data Empty<br />
data NonEmpty<br />
data List x y where<br />
Nil :: List a Empty<br />
Cons:: a -> List a b -> List a NonEmpty<br />
<br />
safeHead:: List x NonEmpty -> x<br />
safeHead (Cons a b) = a<br />
</haskell><br />
<br />
now safeHead can only be applied to non empty lists, and will never evaluate to bottom. This too comes at a cost; consider the function:<br />
<br />
<haskell><br />
silly 0 = Nil<br />
silly 1 = Cons 1 Nil<br />
</haskell><br />
<br />
yields an objection from ghc:<br />
Couldn't match `Empty' against `NonEmpty'<br />
Expected type: List a Empty<br />
Inferred type: List a NonEmpty<br />
In the application `Cons 1 Nil'<br />
In the definition of `silly': silly 1 = Cons 1 Nil<br />
<br />
== Parsing Example ==<br />
<br />
Note that GADTs provide a rather nice platform for embedded domain specific languages. In particular, they allow an [[EDSL]] to use Haskell's type system for its own purposes. As a simple example, we might have an EDSL for simple (regexp-like) parsers that looks something like:<br />
<br />
<haskell><br />
data Parser tok a where<br />
Zero :: Parser tok ()<br />
One :: Parser tok ()<br />
Check :: (tok -> Bool) -> Parser tok tok<br />
Satisfy :: ([tok] -> Bool) -> Parser tok [tok]<br />
Push :: tok -> Parser tok a -> Parser tok a<br />
Plus :: Parser tok a -> Parser tok b -> Parser tok (Either a b)<br />
Times :: Parser tok a -> Parser tok b -> Parser tok (a,b)<br />
Star :: Parser tok a -> Parser tok [a]<br />
</haskell><br />
<br />
An evaluator/parser is then straightforward. Below it's written monadically for<br />
convenience, but this also means that we could generalise the return type to being in any MonadPlus. Note that an advantage of this representation which we don't show here is that we could also write a function which applies algebraic rules to the structure to try to simplify the parser before running it. (Though if we were really concerned with efficiency, we'd probably also need a couple more primitives.)<br />
<br />
<haskell><br />
parse :: Parser tok a -> [tok] -> Maybe a<br />
<br />
-- Zero always fails.<br />
parse Zero ts = mzero<br />
<br />
-- One matches only the empty string.<br />
parse One [] = return ()<br />
parse One _ = mzero<br />
<br />
-- Check p matches a string with exactly one token t such that p t holds.<br />
parse (Check p) [t] = if p t then return t else mzero<br />
parse (Check p) _ = mzero<br />
<br />
-- Satisfy p any string such that p ts holds.<br />
parse (Satisfy p) xs = if p xs then return xs else mzero<br />
<br />
-- Push t x matches a string ts when x matches (t:ts).<br />
parse (Push t x) ts = parse x (t:ts)<br />
<br />
-- Plus x y matches when either x or y does.<br />
parse (Plus x y) ts = liftM Left (parse x ts) `mplus` liftM Right (parse y ts)<br />
<br />
-- Times x y matches the concatenation of x and y.<br />
parse (Times x y) [] = liftM2 (,) (parse x []) (parse y [])<br />
parse (Times x y) (t:ts) = <br />
parse (Times (Push t x) y) ts `mplus`<br />
liftM2 (,) (parse x []) (parse y (t:ts))<br />
<br />
-- Star x matches zero or more copies of x.<br />
parse (Star x) [] = return []<br />
parse (Star x) (t:ts) = do<br />
(v,vs) <- parse (Times x (Star x)) (t:ts)<br />
return (v:vs)<br />
</haskell><br />
<br />
Finally, we might define some examples:<br />
<br />
<haskell><br />
token x = Check (== x)<br />
string xs = Satisfy (== xs)<br />
<br />
p = Times (token 'a') (token 'b')<br />
p1 = Times (Star (token 'a')) (Star (token 'b'))<br />
p2 = Star p1<br />
<br />
blocks :: (Eq tok) => Parser tok [[tok]]<br />
blocks = Star (Satisfy allEqual)<br />
where allEqual xs = and (zipWith (==) xs (drop 1 xs))<br />
<br />
evenOdd = Plus (Star (Times (Check even) (Check odd)))<br />
(Star (Times (Check odd) (Check even)))<br />
<br />
</haskell><br />
<br />
Testing this in ghci:<br />
<pre><br />
*Main> parse p "ab"<br />
Just ('a','b')<br />
*Main> parse p "ac"<br />
Nothing<br />
*Main> parse p1 "aaabbbb"<br />
Just ("aaa","bbbb")<br />
*Main> parse p2 "aaabbbbaabbbbbbbaaabbabab"<br />
Just [("aaa","bbbb"),("aa","bbbbbbb"),("aaa","bb"),("a","b"),("a","b")]<br />
*Main> :t p2<br />
p2 :: Parser Char [([Char], [Char])]<br />
*Main> parse blocks "aaaabbbbbbbbcccccddd"<br />
Just ["aaaa","bbbbbbbb","ccccc","ddd"]<br />
*Main> parse evenOdd [0..9]<br />
Just (Left [(0,1),(2,3),(4,5),(6,7),(8,9)])<br />
*Main> parse evenOdd [1..10]<br />
Just (Right [(1,2),(3,4),(5,6),(7,8),(9,10)])<br />
<br />
</pre><br />
<br />
== Projects containing GADTs ==<br />
<br />
Papers on [[Libraries and tools/Database interfaces/HaskellDB|HaskellDB]] describe problems when GADTs can help (but HaskellDB solves these problems with [[phantom type]]s).<br />
<br />
[[Darcs]] represents motivating examples for GADTs, too -- and uses them.<br />
The motivations are described in David Roundy's FOSDEM slides (Implementing the Darcs Patch Formalism and Verifying It) (see p. 11, 13--14.). The talk mentions also the notions of [[phantom type]], and [[existential type]], and [[type witness]] (see p. 15).<br />
<br />
== See also ==<br />
<br />
* [[Algebraic data type]]<br />
* [[GADTs for dummies]]<br />
<br />
<br />
[[Category:Glossary]]<br />
[[Category:Language extensions]]</div>Sulzmann