Projections for polymorphic first-order strictness

Math.Struct.inComp.Science(1991),vol.1,pp.1{20ProjectionsforPolymorphicFirst-OrderStrictnessAnalysis:JohnHughesandJohnLaunchburyDepartmentofComputingScienceUniversityofGlasgowReceivedAugust1990Weapplythecategoricalpropertiesofpolymorphicfunctionstocompile-timeanalysis,specicallyprojection-basedstrictnessanalysis.Firstweinterpretparameterisedtypesasfunctorsinasuitablecategory,andshowthattheypreservemonicsandepics.Thenwedene\strongand\weakpolymorphism,thelatteradmittingcertainprojectionsthatarenotpolymorphicintheusualsense.Weprovethat,undertherightconditions,aweaklypolymorphicfunctionischaracterisedbyasingleinstance.Itfollowsthatthestrictnessanalysisofonesimpleinstanceofapolymorphicfunctionyieldsresultsthatapplytoall.Weshowhowthistheorymaybeapplied.Incomparisontoearlierpolymorphicstrictnessanalysismethods,ourscanapplypolymorphicinformationtoaparticularinstanceverysimply.Thecategoricalapproachsimpliesourproofs,enablingthemtobecarriedoutatahigherlevel,andmakingthemindependentofthepreciseformoftheprogramminglanguagetobeanalysed.Themajorlimitationofourresultsisthattheyapplyonlytorst-orderfunctions.1.IntroductionThisisnotapaperaboutcategorytheory.Ratheritisaboutusingcategoricalideastodevelopbetteroptimisingcompilersforfunctionallanguages.Thecategoricalfactweuseisthateveryrst-orderpolymorphicfunctionisanaturaltransformation[28,36].Thissemanticpropertyenablesustodevelopasemanticanalysismethodforpolymorphicfunctions;itguidesourintuitionsandgreatlysimpliesourproofs,replacingstructuralinductionsovertermsbysemanticarguments.Thesecategoricalproofsarenotonlyatahigherlevelthanthecorresponding\syntacticproofswouldbe,theyareunspecicabouttheprogramminglanguageinwhichpolymorphicfunctionsareexpressed.The\parametricitycapturedbynaturalityisastrongcondition,muchstrongerthananythatcouldbeinferredfrommanyothermodelsofpolymorphism.Itisthisgreaterstrengththatmakesourapproachfeasible.Theparticularsemanticanalysistechniqueweareinterestedinisprojection-based:ThisisacompletelyrevisedversionofapaperthatoriginallyappearedintheSymposiumonCategoryTheoryandComputerScience,Manchester1989.Wehaveaddedmanyproofsmissingintheoriginalandreworkedtheexistingproofstobemorecategoricaland,hopefully,moreelegant.2strictnessanalysis.Weproveanewresultinthispaper,thatresultsfromthiskindofanalysisare,inasense,polymorphic.Thisconrmsanearlierconjecture[19],andshowshowthetechniquecanbeappliedtorst-orderpolymorphicfunctions.Thepaperisorganisedasfollows.Inthenextsection,wereviewprojection-basedstrictnessanalysisverybriey.InSection3weintroducethetypeswewillbeworkingwith:theyaretheobjectsofacategory.Weshowthatparameterisedtypesarefunctors,withcertaincancellationproperties.InSection4wedenestrongandweakpolymor-phism:polymorphicfunctionsinprogramminglanguagesarestronglypolymorphic,butwewillneedtouseprojectionswithaslightlyweakerproperty.Weprovethat,undercertainconditions,weaklypolymorphicfunctionsarecharacterisedbyanynon-trivialinstance.Wecanthereforeanalyseonemonomorphicinstanceofapolymorphicfunctionusingexistingtechniques,andapplytheresultstoeveryinstance.InSection5wechooseanitesetofprojectionsforeachtype,suitableforuseinapracticalcompiler.Wecallthesespeciallychosenprojectionscontexts,andweshowexamplesoffactorisingcontextsforcompoundtypesinordertofacilitateapplicationoftheresultsofSection4.Wegiveanumberofexamplesofpolymorphicstrictnessanalysis.Finally,inSection6wediscussrelatedworkanddrawsomeconclusions.2.ProjectionsforStrictnessAnalysisEarlystrictnessanalysismethodscoulddiscovernothinginformativeaboutfunctionsonlazydata-structures,andprojectionbasedstrictnessanalysiswasdevelopedinanattempttosolvethisproblem.Recallthat,indomaintheory,aprojectionisafunctionsuchthat=andvID(=x:x).Theessentialintuitionisthataprojectionperformsacertainamountofevaluationofalazydata-structure.Forexample,theprojection:NatNat!NatNat(x;y)=(?;?)ifx=?=(x;y)ifx6=?maybethoughtofasevaluatingtherstcomponentofapair,while:NatNat!NatNat(x;y)=(?;?)ifx=?ory=?=(x;y)otherwiseevaluatesboth.Nowwecanregardafunctionas-strict|performingasmuchevaluationas|ifevaluatingitsargumentwithbeforethecalldoesnotchangeitsresult.Forexample,thefunction+:NatNat!Natevaluatesbothitsarguments,andso+=+Moregenerally,theremaybepartsofafunction’sargumentthatareevaluatedonlyifcertainpartsofitsresultareevaluated|afunctionmayevaluatemoreorlessofits3argumentdependingoncontext.Forexample,swap:NatNat!NatNatswap(x;y)=(y;x)isnot-strict,butitis-strictina-strictcontextsinceswap=swapThus,ifbothcomponentsofswap’sresultwillbeevaluated,thenthecomponentsofitsargumentcanbeevaluatedbeforethecallwithoutchangingthemeaning.Wemakethefollowingdenition:Denition1.Letfbeafunctionandandbeprojections.Wesayfis-strictina-strictcontextiff=f(orequivalently,fvf).Inthiscasewewritef:)2Projectionscapturethenotionofevaluatingacomponentofadata-structure;tocaptureevaluationofasinglevaluewemustembeditina\data-structurewithasinglecom-ponent,whichwecanthinkofasrepresentinganunevaluatedclosure.Thuswethinkofaclo