Generic Haskell practice and theory

GenericHaskell:practiceandtheoryRalfHinze1andJohanJeuring2,31Institutf¨urInformatikIII,Universit¨atBonnR¨omerstraße164,53117Bonn,[e-mail]~ralf/2InstituteofInformationandComputingSciences,UtrechtUniversityP.O.Box80.089,3508TBUtrecht,[e-mail]~johanj/3OpenUniversity,Heerlen,TheNetherlandsAbstract.GenericHaskellisanextensionofHaskellthatsupportstheconstructionofgenericprograms.TheselecturenotesdescribethebasicconstructsofGenericHaskellandhighlighttheunderlyingtheory.Genericprogrammingaimsatmakingprogrammingmoreeffectivebymak-ingitmoregeneral.Genericprogramsoftenembodynon-traditionalkindsofpolymorphism.GenericHaskellisanextensionofHaskell[38]thatsupportstheconstructionofgenericprograms.GenericHaskelladdstoHaskellthenotionofstructuralpolymorphism,theabilitytodefineafunction(oratype)byinductiononthestructureoftypes.Suchafunctionisgenericinthesensethatitworksnotonlyforaspecifictypebutforawholeclassoftypes.Typicalexamplesincludeequality,parsingandprettyprinting,serialising,ordering,hashing,andsoon.ThelecturenotesonGenericHaskellareorganizedintotwoparts.Thisfirstpartmotivatestheneedforgenericity,describesthebasicconstructsofGenericHaskell,putsGenericHaskellintoperspective,andhighlightstheunderlyingtheory.Thesecondpartentitled“GenericHaskell:applications”delvesdeeperintothelanguagediscussingthreenon-trivialapplicationsofGenericHaskell:genericdictionaries,compressingXMLdocuments,andagenericversionofthezipperdatatype.Thefirstpartisorganizedasfollows.Section1providessomebackgrounddiscussingtypesystemsingeneralandthetypesystemofHaskellinparticular.Furthermore,itmotivatesthebasicconstructsofGenericHaskell.Section2takesacloserlookatgenericdefinitionsandshowshowtodefinesomepopulargenericfunctions.Section3highlightsthetheoryunderlyingGenericHaskellanddiscussesitsimplementation.Section4concludes.1IntroductionThissectionmotivatesandintroducesthebasicconstructsofGenericHaskell.Westartbylookingattypesystems.2R.Hinze,J.JeuringAbasicknowledgeofHaskellisdesirable,asalltheexamplesaregiveneitherinHaskellorinGenericHaskell.1.1TypesystemsSafelanguagesMostprogrammersprobablyagreethatlanguagesafetyisagoodthing.Languagesafetyisquiteacolorfultermmeaningdifferentthingstodifferentpeople.HereareafewdefinitionstakenfromPierce’sexcellenttextbook“TypesandProgrammingLanguages”[40].–Asafelanguageisonethatmakesitimpossibletoshootyourselfinthefootwhileprogramming.–Asafelanguageisonethatprotectsitsownabstractions.–Asafelanguageisonethatthatpreventsuntrappederrorsatruntime.–Asafelanguageiscompletelydefinedbyitsprogrammer’smanual.Thedefinitionsputemphasisondifferentaspectsoflanguagesafety.Quiteclearly,allofthesearedesirablepropertiesofaprogramminglanguage.Now,languagesafetycanbeachievedbystatictypechecking,bydynamictypechecking,or—andthisisthemostcommoncase—byacombinationofstaticanddynamicchecks.ThelanguageHaskellservesasanexampleofthelatterapproach:passinganintegertoalist-processingfunctioniscapturedstaticallyatcompiletimewhiletakingthefirstelementoftheemptylistresultsinarun-timeerror.StaticanddynamictypingItiswidelyacceptedthatstatictypesystemsareindispensableforbuildinglargeandreliablesoftwaresystems.Themostcitedbenefitsofstatictypinginclude:–Programmingerrorsaredetectedatanearlystage.–Typesystemsenforcedisciplinedprogramming.–Typespromoteabstraction(abstractdatatypes,modulesystems).–Typesprovidemachine-checkabledocumentation.However,typesystemsarealwaysconservative:theymustnecessarilyrejectprogramsthatbehavewellatruntime.Inasense,genericprogrammingisaboutextendingtheboundariesofstatictypesystems.Thisisthereasonwhytheselecturenoteshavelittletoofferforaddictsofdynamicallytypedlanguages.Aswewillsee,mostgenericprogramscanbereadilyimplementedinadynamicallycheckedlanguage.(Conceptually,adynamiclanguageoffersoneuniversaldatatype;programmingafunctionthatworksforaclassofdatatypesisconsequentlyanon-issue.)PolymorphictypesystemsPolymorphismcomplementstypesecuritybyflex-ibility.PolymorphictypesystemsliketheHindley-Milnersystem[33]allowtheGenericHaskell:practiceandtheory3definitionoffunctionsthatbehaveuniformlyoveralltypes.Astandardexampleisthelengthfunctionthatcomputesthelengthofalist.dataLista=Nil|Consa(Lista)length::∀a.Lista→IntlengthNil=0length(Consaas)=1+lengthasThefirstlinedeclaresthelistdatatype,whichisparametricinthetypeoflistelements.Thefunctionlengthhappenstobeinsensitivetotheelementtype.Thisissignalledbytheuniversalquantifierinlength’stypesignature(read:Lista→Intisavalidtypeoflengthforalltypesa).ThoughthisisnotHaskell98syntax,wewillwritepolymorphictypesalwaysusingexplicitqualifiers.Mostreadersprobablyknowtheuniversalquantifierfrompredicatelogic.Indeed,thereisaclosecorrespondencebetweenpolymorphictypesystemsandsystemsofhigher-orderlogic,see[47].Inlightofthiscorrespondencewenotethatthequantifierinlength’stypesignatureissecond-orderasitrangesoversets(ifwenaivelyequatetypeswithsets).However,evenpolymorphictypesystemsaresometimeslessflexiblethanonewouldwish.Forinstance,itisnotpossi