Proceedings of the 1999 Haskell Workshop Erik Meijer (editor) UU-CS-1999-28 FridayOctober 9th, 1999, Paris,France Proceedings of the 1999 Haskell Workshop UU-CS-1999-28 Erik Meijer (editor) Friday October 1st, 1999, Paris, France 1999 Haskell Workshop Thepurposeoftheworkshopistodiscussexperiencewith Haskell,andpossible future developments of the language. The lively discussions at the 1997 Haskell Workshop in Amsterdam about the future of Haskell led to the de(cid:12)nition of Haskell’98, giving Haskell the stability that has sofarbeen lacking. Theroadaheadto Haskell-2has manyopportuni- ties for developing and enhancing Haskell in new and exciting ways. The third Haskellworkshoppresentssixpapersonthedesign,implementation, anduseof Haskell. The programcommittee consisted of (cid:15) Koen Claessen (Chalmers) (cid:15) Byron Cook (OGI) (cid:15) GregoryHager (The Johns Hopkins University) (cid:15) Graham Hutton (Nottingham) (cid:15) Alexander Jacobson (shop.com) (cid:15) Fergus Henderson (Melbourne) (cid:15) Sigbjorn Finne (Glasgow) (cid:15) Erik Meijer (Utrecht) { chair (cid:15) Colin Runciman (York) (cid:15) Philip Wadler (Bell Labs, Lucent Technologies) The Haskell Workshop was held in conjuction with PLI’99 and was sponsored byINRIA, CNRS, MicrosoftResearch,TrustedLogic, FranceTelecom,and the FrenchMinist(cid:18)eredel’EducationNationaledelaRechercheet delaTechnology. AdditionalsponsoringwasreceivedbytheUniversityResearchProgramsgroup of Microsoft Research Cambridge for the Jake project. The goal of Jake is to develop a set of Perl and Tcl free conference management tools completely programmed in Haskell. Erik Meijer September 1999 Workshop Program 8:30 - 9:30 PLI Invited talk Mobility in the Join-Calculus Georges Gonthier (INRIA Rocquencourt, France) 9:45 - 10:45 Session 1 Typing Haskell In Haskell Mark Jones (Oregon Graduate Institute, USA) Haskell library template e(cid:11)ort (10 minute slot) Andy Gill (Oregon Graduate Institute, USA) 10:45 - 11:15 Co(cid:11)ee break 11:15 - 12:45 Session 2 Embedding Prolog in Haskell Silvija Seres and Mike Spivey (Oxford University, UK) Logical Abstractions in Haskell Nancy A. Day, John Launchbury and Je(cid:11) Lewis (Oregon Graduate Institute, USA) 12:45 - 14:30 Lunch 14:30 - 16:00 Session 3 The Syntactical Subtleties of Haskell (Invited Talk) Simon Marlow (Microsoft Research Cambridge, UK) Lightweight Extensible Records for Haskell Mark Jones (Oregon Graduate Institute, USA) and Simon Peyton Jones (Mi- crosoft Research Cambridge, UK) 16:00 - 16:30 Tea time 16:30 - 18:00 Session 4 A Generic Programming Extension for Haskell Ralf Hinze (Bonn University, Germany) Restricted Datatypes in Haskell John Hughes (Chalmers University, Sweden) 18:00 - 18:30 Session 5 Dependent types: Doing without them (10 minute slot) Daniel Fridlender (BRICS, Denmark) and Mia Indrika (Chalmers University, Sweden) The future of Haskell (Open-mike session) Typing Haskell In Haskell Mark Jones (Oregon Graduate Institute, USA) Typing Haskell in Haskell Mark P. Jones Oregon Graduate Institute of Science and Technology [email protected] Haskell Workshop Version: September 1, 1999 Abstract with prototype implementations. The existing Haskell implementationsarenotsuitableforthis(andwerenot intended to be): the nuts and bolts of a type system Haskell bene(cid:12)ts from a sophisticated type system, but im- areeasilyobscuredbytheuseofspeci(cid:12)cdatastructures plementors, programmers, and researchers su(cid:11)er because it andoptimizations,orbytheneedtointegratesmoothly has no formal description. To remedythis shortcoming, we with other parts of an implementation. present a Haskell program that implementsa Haskell type- checker,thusprovidingamathematicallyrigorousspeci(cid:12)ca- tioninanotationthatisfamiliartoHaskellusers. Weexpect ThispaperpresentsaformaldescriptionoftheHaskelltype this program to (cid:12)ll a serious gap in current descriptions of systemusingthenotationofHaskellitselfasaspeci(cid:12)cation Haskell, both as a starting point for discussions about ex- language. Indeed,the source code for this paperis itself an isting features of the type system, and as a platform from executableHaskellprogramthatispassedthroughacustom A which to explore new proposals. preprocessor and then through LTEX to obtain the typeset version. The type checker is available in source form on the Internet at http://www.cse.ogi.edu/~mpj/thih/. We 1 Introduction hopethatthiswillserveasaresourceforHaskellimplemen- tors,programmersandresearchers,andthatitwillbea(cid:12)rst 1 step ineliminating mostof theproblemsdescribed above. Haskell bene(cid:12)ts from one of the most sophisticated type systems of any widely used programming language. Unfor- Oneaudiencewhoseneedsmaynotbeparticularlywellmet tunately,it also su(cid:11)ersbecausethere isnoformalspeci(cid:12)ca- bythispaperareresearchersinprogramminglanguagetype tion of what thetypesystemshould be. As a result: systemswhodonothaveexperienceof Haskell. (Wewould, however, encourage anyone in that position to learn more (cid:15) ItishardforHaskellimplementorstobesurethattheir about Haskell!) Indeed, we do not follow the traditional compilers and interpreters accept the same programs route in such settings where the type systemmight(cid:12)rst be as other implementations. The informal speci(cid:12)cation presented in its purest form, and then related to a more in the Haskell report [10] leaves too much room for concrete type inference algorithm by soundness and com- confusionandmisinterpretation. Thisleadstogenuine pleteness theorems. Here, wedeal onlywithtypeinference. discrepancies between implementations, as many sub- Itdoesn’tevenmakesensetoaskifouralgorithmcomputes scribers to theHaskell mailing list will haveseen. ‘principal’ types: suchaquestionrequiresacomparisonbe- tween two di(cid:11)erent presentations of a type system, and we (cid:15) It is hard for Haskell programmers to understand the only have one. Nevertheless, we believe that the speci(cid:12)ca- details of the type system, and to appreciate why tioninthispapercouldeasilyberecastinamorestandard, someprogramsare acceptedwhenothersarenot. For- type-theoreticmannerandusedtodevelopapresentationof mal presentations of most aspects of the type system Haskell typingin a more traditional style. are available in the research literature, but often ab- The code presented here can be executed with any Haskell stractonspeci(cid:12)cfeaturesthatareHaskell-like,butnot system,butourprimarygoalshavebeenclarityandsimplic- Haskell-exact, and do not describe the complete type ity,andtheresulting code is notintendedto bean eÆcient system. Moreover,thesepapersoftenusedisparateand implementation of type inference. Indeed, in some places, unfamiliartechnicalnotationandconceptsthatmaybe our choice of representation may lead to signi(cid:12)cant over- hard for some Haskell programmersto understand. heads and duplicated computation. It would be interesting (cid:15) It is hard for Haskell researchers to explore new type totrytoderiveamoreeÆcient,butprovablycorrectimple- systemextensions,oreventostudyusabilityissuesthat mentation from the speci(cid:12)cation given here. We have not arise with the present type system such as the search attempted to do this because we expect that it would ob- for better type error diagnostics. Work in these areas scurethekeyideas thatwe wanttoemphasize. Ittherefore requires a clearunderstandingofthetypesystemand, remains as a topic for future work, and as a test to assess ideally, a platform on which to build and experiment theapplicabilityofprogramtransformationandsynthesisto 1 complex,butmodestlysized Haskell programs. Throughout,weuse‘Haskell’asanabbreviationfor‘Haskell98’. 1 Another goal for this paper was to give as complete a de- Description Symbol Type scription of the Haskell type system as possible, while also kind k; ::: Kind aiming for conciseness. For this to be possible, we have typeconstructor tc; ::: Tycon assumed that certain transformations and checks will have typevariable v; ::: Tyvar been made prior to typechecking, and hence that we can { ‘(cid:12)xed’ f; ::: work with a much simpler abstract syntax than the full { ‘generic’ g; ::: source-level syntax of Haskell would suggest. As we ar- type t; ::: Type gue informally at various points in the paper, we do not class c; ::: Class believe that there would be any signi(cid:12)cant diÆculty in ex- predicate p; q; ::: Pred tendingoursystemtodealwiththemissingconstructs. All { ‘deferred’ d; ::: of the fundamentalcomponents,including the thorniest as- { ‘retained’ r; ::: pectsofHaskelltyping,areaddressedintheframeworkthat quali(cid:12)ed type qt; ::: QualType wepresenthere. Ourspeci(cid:12)cationdoes notattempttodeal scheme sc; ::: Scheme with all of the issues that would occur in the implementa- substitution s; ::: Subst tion of afull Haskell implementation. Wedo nottackle the uni(cid:12)er u; ::: Subst problems of interfacing a typechecker with compiler front assumption a; ::: Assump ends (to track source code locations in error diagnostics, identi(cid:12)er i; ::: Id for example) or back ends (to describe the implementation literal l; ::: Literal of overloading, for example), nor do we attempt to formal- pattern pat; ::: Pat ize any of the extensions that are implemented in current expression e; f; ::: Expr Haskell systems. This isone of things thatmakesourspec- alternative alt; ::: Alt i(cid:12)cation relativelyconcise; bycomparison, thecore partsof binding group bg; ::: BindGroup the Hugstypecheckertakes some 90+ pages of C code. Regrettably, length restrictions have prevented us from in- Figure 1: Notational Conventions cludingmanyexamplesinthispapertoillustratethede(cid:12)ni- tionsateachstage. Forthesamereason,de(cid:12)nitionsofafew constantsthatrepresententitiesinthestandardprelude,as we have tried to keep the de(cid:12)nitions and code as clear and well as the machinery that we use in testing to display the simple as possible, and although we have made some use resultsoftypeinference,arenotincludedinthetypesetver- of Haskell overloading and do-notation, we have generally sionofthispaper. Apartfromthosedetails,thispapergives avoided using the more esoteric features of Haskell. In ad- the full source code. dition, some experience with the basics of Hindley-Milner We expect the program described here to evolve in at least style type inference [5, 9, 2] will be needed to understand three di(cid:11)erentways. the algorithms presented here. Although we have aimed to keepourpresentationassimpleaspossible, someaspectsof (cid:15) Formal speci(cid:12)cations are not immuneto error, and so the problems that we are trying to address have inherent it is possible that changes will be required to correct complexity or technical depth that cannot be side-stepped. bugs in the code presented here. On the other hand, Inshort,thispaperwillprobablynotbeusefulasatutorial by writing our speci(cid:12)cation as a program that can be introduction to Hindley-Milnerstyle typeinference! typecheckedandexecutedwithexistingHaskell imple- mentations, we have a powerful facility for detecting simple bugs automatically and for testing to expose 2 Preliminaries deeper problems. (cid:15) As it stands, this paper just provides one more inter- For simplicity, we present the code for our typechecker as pretationoftheHaskelltypesystem. Webelievethatit a single Haskell module. The program uses only a handful isconsistentwiththeoÆcialspeci(cid:12)cation,butbecause of standard prelude functions, like map, concat, all, any, the latter is given only informally, we cannot establish mapM, etc., and a few operations from the List library: thecorrectnessofourpresentationhereinanyrigorous manner. We hope that this paper will stimulate dis- module TypingHaskellInHaskell where cussionintheHaskellcommunity,andwouldexpectto import List (nub; (nn); intersect; union; partition) make changes to the speci(cid:12)cation as we work towards some kind of consensus. For the most part, our choice of variable names follows the (cid:15) There is no shortage of proposed extensions to the notational conventions set out in Figure 1. A trailing s on Haskell type system, some of which have already been avariablenameusuallyindicatesalist. NumericsuÆcesor implemented in one or more of the available Haskell primes are used as further decoration where necessary. For 0 0 systems. Some of the better known examples of example, we use k or k for a kind, and ks or ks for a list thisincludemultiple-parametertypeclasses,existential of kinds. The types and terms appearing in the table are types, rank-2 polymorphism, extensible records. We described more fully in later sections. To distinguish the wouldliketoobtainformaldescriptionsforasmanyof code for the typechecker from program fragments that are theseproposals aspossiblebyextendingthecorespec- used to discuss its behavior, we typeset the former in an i(cid:12)cation presentedhere. italic font, andthelatter in a typewriter font. It will come as no surprise to learn that some knowledge Throughoutthis paper,we implementidenti(cid:12)ers asstrings, of Haskell will be required to read this paper. That said, andassumethatthereisasimplewaytogeneratenewiden- 2