An Introduction to Category Theory for the working

IThisbookiscurrentlyoutofprint.UponkindpermissionoftheM.I.T.-Press,itisavailableonftp.ens.fr/pub/dmi/users/longo/CategTypesStructuresAllreferencesshouldbemadetothepublishedbook.CATEGORIESTYPESANDSTRUCTURESAnIntroductiontoCategoryTheoryfortheworkingcomputerscientistAndreaAspertiGiuseppeLongoFOUNDATIONSOFCOMPUTINGSERIESM.I.T.PRESS,1991IIINTRODUCTIONThemainmethodologicalconnectionbetweenprogramminglanguagetheoryandcategorytheoryisthefactthatboththeoriesareessentially“theoriesoffunctions.”Acrucialpoint,though,isthatthecategoricalnotionofmorphismgeneralizestheset-theoreticaldescriptionoffunctioninaverybroadsense,whichprovidesaunifiedunderstandingofvariousaspectsofthetheoryofprograms.Thisisoneofthereasonsfortheincreasingroleofcategorytheoryinthesemanticinvestigationofprogramsifcompared,say,totheset-theoreticapproach.However,theinfluenceofthismathematicaldisciplineoncomputersciencegoesbeyondthemethodologicalissue,asthecategoricalapproachtomathematicalformalizationseemstobesuitableforfocusingconcernsinmanydifferentareasofcomputerscience,suchassoftwareengineeringandartificialintelligence,aswellasautomatatheoryandothertheoreticalaspectsofcomputation.Thisbookismostlyinspiredbythisspecificmethodologicalconnectionanditsapplicationstothetheoryofprogramminglanguages.Moreprecisely,asexpressedbythesubtitle,itaimsataself-containedintroductiontogeneralcategorytheory(partI)andatacategoricalunderstandingofthemathematicalstructuresthatconstituted,inthelasttwentyorsoyears,thetheoreticalbackgroundofrelevantareasoflanguagedesign(partII).Theimpactonfunctionalprogramming,forexample,ofthemathematicaltoolsdescribedinpartII,iswellknown,asitrangesfromtheearlydialectsofLisp,toEdinburghML,tothecurrentworkinpolymorphismsandmodularity.Recentapplications,suchasCAML,whichwillbedescribed,usecategoricalformalizationforthepurposesofimplementation.Inadditiontoitsdirectrelevancetotheoreticalknowledgeandcurrentapplications,categorytheoryisoftenusedasan(implicit)mathematicaljargonratherthanforitsexplicitnotionsandresults.Indeed,categorytheorymayproveusefulinconstructionofasound,unifyingmathematicalenvironment,oneofthepurposesoftheoreticalinvestigation.Aswehaveallprobablyexperienced,itisgoodtoknowinwhich“category”oneisworking,i.e.,whicharetheacceptablemorphismsandconstructions,andthelanguageofcategoriesmayprovideapowerfulstandardizationofmethodsandlanguage.Inotherwords,manydifferentformalismsandstructuresmaybeproposedforwhatisessentiallythesameconcept;thecategoricallanguageandapproachmaysimplifythroughabstraction,displaythegeneralityofconcepts,andhelptoformulateuniformdefinitions.Thishasbeenthecase,forexample,intheearlyapplicationsofcategorytheorytoalgebraicgeometry.Thefirstpartofthisbookshouldencourageeventhereaderwithnospecificinterestinprogramminglanguagetheorytoacquireatleastsomefamiliaritywiththecategoricalwayoflookingatformaldescriptions.Theexplicituseofdeeperfactsisafurtherstep,whichbecomeseasierwithaccesstothisinformation.PartIIandsomechaptersinpartIaremeanttotakethisfurtherstep,atIIIleastinoneofthepossibledirections,namelythemathematicalsemanticsofdatatypesandprogramsasobjectsandmorphismsofcategories.WewereurgedtowritethegeneralintroductioncontainedinpartI,sincemostavailablebooksincategorytheoryarewrittenforthe“workingmathematician”and,asthesubjectisgreatlyindebtedtoalgebraicgeometryandrelateddisciplines,theexamplesandmotivationscanbeunderstoodonlybyreaderswithsomeacquaintancewithnontrivialfactsinalgebraorgeometry.Formostcomputerscientists,itisnotmuchhelpintheunderstandingof“naturaltransformations”toseeaninvolvedexamplebasedontensorproductsincategoriesofsheaves.Thusourexampleswillbebasedonelementarymathematicalnotions,suchasthedefinitionofmonoid,group,ortopologicalspace,say,andonstructuresfamiliarforreaderswithsomeacquaintancewiththetoolsinprogramminglanguagesemantics.Inparticular,partialordersandthevariouscategoriesofdomainsfordenotationalsemanticswilloftenbementionedorintroduced,aswellasbasicresultsfromcomputabilitytheory.Forexample,wewilltrytopresentthefundamentaloperationof“currying”forcartesianclosedcategorieswithreferencetotheconnectionbetweentheuniversalfunctionandthegdel-numberingofthepartialrecursivefunctions.Partialmorphismswillbepresentedasageneralizationofacommonnotionintheoryofcomputation.Categorytheorymaybepresentedinaveryabstractway:asapuregameofarrowsanddiagrams.Itisusefultoreachthepointwhereacquaintancewiththeformal(essentially,equational)approachissofirmthatitmakessenseindependentlyofany“structural”understanding.Inthisbook,though,wewillstresstheroleofstructures,andwewillalwaystrytogiveanindependentmeaningtoabstractnotionsandresults.Eachdefinitionandfactwillbeexemplified,orevenderived,fromapplicationsorstructuresinsomewayindebtedtocomputing.However,inordertostresstheroleofthepurelyequationalview,thelastchaptersofeachpart(essentiallychapters7and11)willbelargelybasedonaformal,computationalapproach.Indeed,evenifmathematicallyveryabstract,theequationalargumentsturnouttobeparticularlyrelevantfromacomputerscienceperspective.Theearl