Two-level types and parameterized modules

J.FunctionalProgramming14(5):547-587,September20041Two-LevelTypesandParameterizedModules∗TimSheardandEmirPasalicPacificSoftwareResearchCenterOregonGraduateInstitute{sheard,pasalic}@cse.ogi.eduAbstractInthispaper,wedescribetwotechniquesfortheefficient,modularizedimplementationofalargeclassofalgorithms.Weillustratethesetechniquesusingseveralexamples,includingefficientgenericunificationalgorithmsthatusereferencecellstoencodesubstitutions,andhighlymodularlanguageimplementations.Wechosetheseexamplestoillustratethefollowingimportanttechniquesthatwebelievemanyfunctionalprogrammerswouldfinduseful.First,definingrecursivedatatypesbysplittingthemintotwolevels:astructuredefininglevel,andarecursiveknot-tyinglevel.Second,theuseofrank-2polymorphisminsideHaskell’srecordtypestoimplementakindoftype-parameterizedmodules.Finally,weexploretechniquesthatallowustocombinealreadyexistingrecursiveHaskelldata-typeswiththehighlymodularstyleofprogrammingproposedhere.1IntroductionProgrammodularizationandgenericprogrammingaretwopracticesdevelopedtomakethetasksofconstructingandmaintaininglargeprogramseasier.Programmodularizationbreaksprogramsintosmaller,potentiallyreusablefragments,eachofwhichisolatesasinglekeyprogramaspect.Thiscreatesaseparationofconcernswhichallowstheprogrammertoseparatelycreateandchangeeachprogramaspect.Genericprogrammingistheconstructionofasinglealgorithmthatworksovermultipledatastructures.Thisallowstheprogrammertowriteanalgorithmonceandtoreuseitonmanydifferentdatastructures.Thispaperdemonstratestwodifferenttechniquestoimplementthesepractices.Thesetechniquesare:two-leveltypes,andtype-parameterizedmodules.Two-leveltypesdefinerecursivedatatypesbysplittingthemintotwolevels:astructuredefin-inglevel,andarecursiveknot-tyinglevel.Theycanbeusedtobothbreakprogramsintomodularpieces,andtosupportgenericprogramming.Atype-parameterizedmoduleisacollectionof(possiblypolymorphic)algorithmsorfunctionsparam-eterizedbyasetoftypes.Thisallowsasinglemoduletobereused,simplybyinstantiatingitatdifferenttypes.Type-parameterizedmodulessupportprogrammodularityinadimensionorthogonaltotwo-leveltypes.∗Extendedversionof(Sheard,2001)2TimSheardandEmirPasalicBoththesetechniquesshouldbeinthebag-of-tricksofanyseriousfunctionalprogrammer.WeillustratethesetechniquesusingHaskellanditsextensions.Two-leveltypessupportgenericprogramminginstandardHaskellwithoutusinganyextensions.Type-parameterizedmodulesrequirethecommonlyavailableextensionsofrank-2polymorphism,andmulti-parametertypeclasses.InthispaperweusethestandardextensionstoHaskellavailableinthemostpopularHaskelldialectsofHugsandGHC.1.1ContributionsThispaperisanextensionafunctionalpearl(Sheard,2001)thatappearedintheproceedingsofICFP’01.Itgoesbeyondthatpaperinseveraldimensions.First,itismoreexplicitaboutwhatconstitutesatwo-leveltype,andillustratesthistechniqueusingseveralsimpleexamplesthatweremissingfromtheoriginalpaper.Second,itaddsanotherlargeexample,namelytheconstructionoflanguageimplementationsfrommodularlanguagefragments.Third,itdemonstrateshowtwo-leveltypescancoexistharmoniouslywiththeirone-levelcounterparts,sothistechniquecanberetrofittedintoexistingprograms.Theheartofthispaperconsistsofillustratingthetechniquesoftype-parameterizedmodules,andtwo-leveltypeswithtwolargeexamples.Theseexamplesarebothratherdetailed,butthatisbyintention.Wewantedtooutlineingreatdetailhowourtechniquescouldbeused.Afterreadershavefinishedthepaper,wewantthemtofeelconfidentthattheycanapplythesetechniquestotheirowndomains.Wewantedtoleavenodetailtothereaders’imagination.Thefirstexampleisthemodularizationofawholeclassofalgorithmsthatcom-paretwoinstancesofthesamedatastructure.Thisclasscontainsalgorithmsforunification,matching,andequalityamongothers.Thesecondexampleisthecon-structionofhighlymodularlanguageimplementations.RoadmapSection2describesthetechniqueoftwoleveltypes.Section3devel-opsthefirstlargeexample:agenericunificationalgorithm.Alongtheway,relevanttechniquesweadvocatearegivenfullexposition.Section4presentsthesecondlargeexample:modularsyntax.Asimpleprogramminglanguageimplementation(inter-preter,parserandpretty-printer)isdevelopedandpresentedinahighlymodularstyle.Section5addressesthepracticalissueofcombiningtwo-leveltypeprogram-mingtechniqueswithexistingprogramsthatwerenotwrittenwiththesetechniquesinmind.Section6distillsanddiscussesrelevantissuespresentedinthepaper.Fi-nally,weconcludeinSection7,andgiveahistoricalnoteonthedevelopmentofthetechniquespresentedinthepaperinSection8.2Two-LevelTypesSeveraladvantagesaccruefromsplittingarecursivedatatypeintotwolevels.Tosplitadatatypeintotwolevels,asinglerecursivedatatypeisreplacedbytworelateddatatypes.Forexample:Two-LevelTypesandParameterizedModules13dataTree=Tip|LeafInt|ForkTreeTreedataTx=Tip|LeafInt|ForkxxdataTree=Wrap(TTree)unwrap::Tree-TTreeunwrap(Wrapx)=xTheordinaryrecursivedatatypeTreeontheleftisreplacedwiththetwodatatypesTandTreeontheright.Thenon-recursivedatatypeTiscalledthestructureoperator,sinceitcapturesthestructureoftheoriginalTreedatatype.Itdoesthisbyabstractingtherecursivesub-treesintothetypep