MarkP.Jones
DepartmentofComputerScience,UniversityofNottingham,
UniversityPark,NottinghamNG72RD,England.
mpj@cs.nott.ac.uk
http://www.cs.nott.ac.uk/Department/Staff/mpj/
Abstract
Modulesystemsareapowerful,practicaltoolformanag-ingthecomplexityoflargesoftwaresystems.Previousat-temptstoformulateatype-theoreticfoundationformodularprogramminghavebeenbasedonexistential,dependent,ormanifesttypes.Theseapproachescanbedistinguishedbytheiruseofdifferentquantifierstopackagetheoperationsthatamoduleexportstogetherwithappropriateimplemen-tationtypes.Ineachcase,theunderlyingtypetheoryissimpleandelegant,butsignificantandsometimescomplexextensionsareneededtoaccountforfeaturesthatareim-portantinpracticalsystems,suchasseparatecompilationandpropagationoftypeinformationbetweenmodules.
Thispaperpresentsasimpletype-theoreticframeworkformodularprogrammingusingparameterizedsignatures.Theuseofquantifiersistreatedasanecessary,butinde-pendentconcern.Usingfamiliarconceptsofpolymorphism,theresultingmodulesystemiseasytounderstandandad-mitstrueseparatecompilation.Itisalsoverypowerful,supportinghigh-order,polymorphic,andfirst-classmoduleswithoutfurtherextension.
1Introduction
Largescalesoftwaredevelopmentobtainssignificantbene-fitsfromtheabilitytobreakprogramsintocollectionsofmodules,eachofwhichcanbedesigned,implementedandunderstoodasindividual,oftenreusable,components.For-malstudiesofthetheoreticalfoundationsformodularpro-grammingprovidevaluableinsightsintothedesignofmorepowerful,andmoreeffectivemodulesystemsforpracticalprogramminglanguages.
Duringthepastdecade,therehavebeenseveralattemptstoprovidetype-theoreticfoundationsformodularprogram-ming[23,16,21,7,22,27,1,6,13,15,3].Themainpropos-alscanbedistinguishedbytheiruseofdifferentconstructstodescribethetypeofamodule.Toillustratethesealterna-tives,supposethatwewishtoconstructacomplexnumber
ToappearintheTwentyThirdAnnualACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,St.PetersburgBeach,Florida,January21-24,1996.
Copyright
c1996bytheAssociationforComputingMachinery,Inc.Permissiontomakedigitalorhardcopiesofpartorallofthisworkforpersonalorclass-roomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributedforprofitorcommercialadvantageandthatcopiesbearthisnoticeandthefullcitationonthefirstpage.Copyrightsforcomponentsofthisworkownedbyoth-ersthanACMmustbehonored.Abstractingwithcreditispermitted.Tocopyotherwise,torepublish,topostonserversortoredistributetolists,requirespriorspecificpermissionand/orafee.RequestpermissionsfromPublicationsDept.,ACMInc.,Fax+1(212)869-0481,orpermissions@acm.org.
packagethatprovidesacollectionofoperations:typeComplexc
={mkCart,mkPolar
::Float→Float→c;re,im
::c→Float;
mag,phase
::
c→Float;...}
Therearethreeestablishedmethodsforpackagingacollec-tionofoperationslikethistogetherwithasuitableimple-mentationtype:
•Existentialtypes(opaque,orweaksums)[23,5].Inamoduleoftype∃c.Complexc,theexistentialquantifierconcealstheidentityoftheimplementationtypecbymakingitabstract.Thisapproachallowspackagestobetreatedasfirst-classvaluesandisfullycompatiblewithseparatecompilation.However,forthepurposesofmodularprogramming,existentialsareoftentoogoodathidingimplementationtypesbecausetheydonotallowadequatepropagationoftypeinfor-mationbetweenpackages[16].•Dependenttypes(transparent,orstrongsums)[18,16,21].AmoduleoftypeΣc.Complexcisrep-resentedbyapairτ,McontainingthetypeτusedtorepresentcomplexnumbersandanimplementationMoftypeComplexτforthecomplexnumberopera-tors.Theabilitytoincludetypecomponentsinmod-ulesmakesthisapproachverypowerful—toopowerfulinfacttopermitcompile-timetypecheckingwithoutcarefulrestrictionsandextensionstoensureasuitablephasedistinction[7]andtosupportfeatureslikeshar-ing[14].Eventhen,itisstillnotpossibletosupporttrueseparatecompilation[2]ortousemodulesasfirst-classvalues[22,12].•Manifesttypes(transluscentsums)[6,13]areanattempttobridgethegapbetweentheweakandstrongsumapproachesdescribedabove.Amoduletype∃c=τ.Complexcismuchlikeanexistential,ex-ceptthatitexposesthefactthataparticularimple-mentationtypeτwaschosen.Anextraruleinthetypesystemcanbeusedtomaketheimplementationtypeabstractbycoercingamanifesttypetoastan-dardexistential.WeshouldalsomentionthetreatmentofmodulesinStan-dardML(SML)whichprovidesoneofthemostpowerfulmodulesystemsinwidespreaduse.Theoveralldesignisof-tenexplainedintermsofdependenttypes,butitisnoteasy
todiscerntheiruseintheformaldefinition[20].Instead,thedefinitionusesasemanticsbasedonfreshlygeneratedtokenscalledstampstoaccountfortheconceptsofsharingandgenerativity.Thisapproachworkswellasamethodforthespecificationandimplementationofatypechecker,butseemstoooperationalforotherpurposes.Inaddition,ithasprovedtobe“remarkablydifficulttomodifyorextend”[6].
Theadvantagesanddisadvantagesofeachofthethreeapproachesdescribedabovewillbedescribedinmoredetailinthefollowingsection.Theimportantpointtonotefornowisthat,ineachcase,thetypeofamodule,packageorstructureisgivenbyanexpressionoftheformQt.f(t)forsomeparameterizedsignaturef(t)andsomequantifierQ.Manyofthecomplicationsthatwehavereferredtoabovearecausedbythefactthatthesequantifierscanbe‘overlyprotective’,limitingtheabilitytopropagatetypeinforma-tionbetweenmodules.
Inthispaper,weshowhowparameterizedsignaturessuchasComplexccanbeusedasthetypesofmodules,treatingquantifiersasaseparateconcern.Theresultisasimple,yetpowerfultypesystemformodularprogram-ming.Ofcourse,westillneedamechanismlikeexistentialquantificationtosupportthedefinitionanduseofabstractdatatypes,butthiscanbedealtwithindifferentwaysandneednotbesocloselytiedtoindividualmodules.Polymor-phism,representedbyuniversalquantification,isanotherimportantpartofthetypesystemthatallowsus:
•Toexpresssharingconstraintsandtodescribetheprop-agationoftypeinformation.•Toreflecttheindependenceoftheimplementationofaparameterizedmodulefromtheimplementationofitsparameters.•Toallowthedefinitionofpolymorphicmodules,ause-fulfeaturethatisnotpermittedinSML[11].Webelievethattheuseofpolymorphismisnaturalandeasytounderstand,particularlyforprogrammerswhoarealreadyfamiliarwiththetypesystemsofthecorelanguagesofSML,Haskell,orsimilarlanguages.
Anotherimportantbenefitofparameterizedsignaturesisthattheyensureaclearseparationbetweenstaticanddynamicsemantics;thetypesystemallowsaprogrammertoassociateagivenmodulewithaparticularcollectionoftypes,butmodulevaluesdonotincludetypecomponents.Asaresult,wedonothavetoworryabouttheproblemsofestablishingaphasedistinction,andtrueseparatecompila-tionispossiblebecausethewaythatamodulecanbeusediscompletelyspecifiedbyitssignature.Thisalsomeansthatmodulescanbetreatedasfirst-classvalues.
Theremainingsectionsofthispaperareasfollows.WebegininSection2withamoredetailedanalysisofprevi-ousattemptstoprovideatype-theoreticbasisformodularprogramming.Thishelpstounderstandthestrengthsandweaknessesofthedifferentapproachesandtoclarifyourowngoalsinthedesignofamodulesystem.Section3describeshowparameterizedsignaturesfitintothepictureandgivessomeexamplestoillustratetheiruse.AformalpresentationofthetypesystemispresentedinSection4.Concernsaboutthesuitabilityofatypesystemusingparameterizedsigna-turesasabasisformodularprogrammingareaddressedinSection5.Finally,Section6concludeswithpointerstofu-turework.
2
2Backgroundandmotivation
Inourintroductorycomments,wehavealreadymentionedseveralpreviousattemptstoprovideatype-theoreticfoun-dationformodularprogramming.Inthissection,wetakeamoredetailedlookateachoftheseproposals,explaininghowthedesignofeachsystemhasbeenmotivatedbythestrengthsandweaknessesofitsancestors.Ouraimistoprovideasurveyofrelatedwork,andmotivationfortheuseofparameterizedsignatures.
Allofthisworkrestsonfundamentalassumptionsaboutthenatureandpurposeofmodulesystems.Certainly,itwouldbewrongtoregardaparticulartypesystemasabasisformodularprogrammingunlessitprovidessome,ifnotall,ofthefollowing:
•Amechanismtosupportseparatecompilationandsomeformofnamespacemanagement.•Amechanismtoenablethedecompositionoflargepro-gramsintosmall,reusableunitsinawaythatisresis-tanttosmallchangesintheprogram.•Amechanismfordefiningabstractions.
Throughoutthispaper,wearguethattheuseofparame-terizedsignaturesisconsistentwithsuchgoals.Supportforseparatecompilationisensuredbymaintainingaclearsep-arationbetweentypesandvalues,whileeffectiveprogramdecompositionissupportedbytheuseofhigher-orderandnestedpolymorphism.Powerfulabstractionscanbedefinedusingparameterizedstructures.Thesystemdoesnotpro-videabuilt-innotionofabstractdatatypesbut,instead,allowsthistobedealtwithusingothermethods.
2.1Existentialtypes
Onewaytoformalizetheprocessofhidingtheimplemen-tationofanabstractdatatypeistouseanexistentialtype[23,5]:
typeComplexPkg
=
∃c.Complexc.
Informally,theexistentialtypingindicatesthatthereisatypecwithoperationsoftypeComplexcdefinedonit.Atthesametime,itprohibitsaprogrammerfrommakinganyassumptionsabouttheimplementationtype.Formally,thepropertiesofexistentialsaredescribedbytypingrules,basedonstandardlogicalrulesforexistentialquantifiers.Thefollowingruleisoftendescribedasanintroductionrulebecauseitintroducesanewoccurrenceofthe∃quantifierintheconclusion:
ΓM:[τ/t]τΓM:(∃t.τ)
Notethattheimplementationtypeτfortheabstracttypeisdiscardedanddoesnotappearanywhereintheconclusion.
TherequirementthatNhasapolymorphictypeinthefollowingeliminationruleensuresthatwedonotmakeanyassumptionsaboutthenow-hiddenimplementationtype;Nbehavesuniformlyforallchoicesoft:
ΓM:∃t.τ
ΓN:∀t.τ→τ
t∈TV(τ)
ΓopenMinN:τ
Existentialtypescompletelyhidetheidentityofimplemen-tationtypes.Forexample,thetypescandcinthebodyofthefollowingexpressioncannotbeidentified,eventhoughtheycomefromthesametermcpxoftypeComplexPkg:
opencpxinΛc.λx:Complexc.
opencpxinΛc.λy:Complexc....
Tofurtheremphasizethisbehaviour,supposethatwewanttodefineapackageofcomplexnumberarithmetic,con-structedfromanarbitraryimplementationofcomplexnum-bers.Theobviouswaytodescribethisistouseafunction:compArithcompArithcpxwhere:
typeArithPkgtypeAritha
=∃a.Aritha={add
neg
::::
a→a→a;a→a;...}.
::=
ComplexPkg→ArithPkg
opencpxinΛc.λp:Complexc.{add=...}
conclusion.Theeliminationruleontherightindicatesthat,ifMisastructureoftypeΣt.f(t),thenthesecondcompo-nent,sndM,ofMhastypef(fstM),wherefstMisthefirstcomponentofM.Informally,dependentsumsaremorepowerfulthanexistentialsbecauseofthisabilitytonamethetypecomponentfstMofastructureM.However,thisalsomeansthatthetypecomponentofastructureisnolongerabstract.
Inasense,asimpletreatmentofmodulesusingdepen-denttypesisactuallytoopowerfulforpracticalsystemsbecauseitinterfereswithseparatecompilation.Morepre-cisely,itmakesitmoredifficulttoseparatecompile-timetype-checkingfromrun-timeevaluation.Toillustratethis,werecastthepreviousdefinitionsofcomplexnumberandarithmetictypesusingdependentsumstoobtain:
typeComplexPkgtypeArithPkgcompArithcompArithc
=Σcpx.Complexcpx=Σa.Aritha::=
ComplexPkg→ArithPkgfstc,{add=...}
GivenanimplementationcpxoftypeComplexPkg,wecanusetheexpressioncompArithcpxtoobtainapackageforarithmeticoncomplexnumbers.Unfortunately,thishasnopracticalusebecausethetypingrulesforexistentialsmakeitimpossibletoconstructanyvaluestowhichtheaddandnegfunctionsoftheresultingpackagecanbeapplied!ThetypesystemdoesnotcapturetheequivalenceofthetypeofcomplexnumbersusedincpxandthetypeofvaluesthatcanbemanipulatedbycompArithcpx.
Analternativeapproachtoexistentialtyping,usingdotnotationinplaceoftheopenconstructdescribedabove,hasbeeninvestigatedbyCardelliandLeroy[4].Thedotnotationallowsustoidentifytheimplementationtypesoftwopackagesiftheyhavethe‘samename’.Thisavoidsthefirstproblemillustratedabove,butnotthesecond.Dotnotationisalsolimitedbytheunavoidablyconservativeno-tionsof‘samename’thatareneededtoensuredecidabilityoftypechecking,andisnotverywell-behavedundersimpleprogramtransformations.
ThecompArithfunctionisanexampleofaparameterizedmodule,orafunctorintheterminologyofSML.Atfirstglance,thisdefinitionsuffersfromthesameproblemsasthepreviousversionusingexistentials;thetypeComplexPkg→ArithPkgdoesnotreflectthefactthatthetypecomponentsoftheargumentandresultstructuresarethesame.How-ever,thisinformationcanbeobtainedbycarryingoutalimiteddegreeofevaluationduringtypechecking.Forex-ample,ifc=τ,M,then:
fst(compArithc)=fstτ,{add=...}=τ.
Toensurethatstatictypecheckingispossible,itisim-portanttodistinguishcompile-timeevaluationofthiskindfromarbitraryrun-timeexecutionofaprogram.Unfortu-nately,treatingafunctorasafunctionoftype(Σs.f(s))→(Σt.g(t))doesnotreflectthisseparation;ingeneral,atypeofthisformmayincludeelementsinwhichthetypecom-ponentoftheresultdependsonthevaluecomponentoftheargument.Asanalternative,Harper,MitchellandMoggi[7,24]haveshownthatasuitablephasedistinctioncanbeestablishedbymodellingfunctorsfromΣs.f(s)toΣt.g(t)asvaluesoftypeΣh.(∀s.f(s)→g(h(s)))wherehrangesoverfunctionsfromtypestotypes,anddescribesthecompile-timepartofthefunctor.
Astheexampleaboveshows,itissometimesnecessarytoinspecttheimplementationofastructuretofindthevalueofatypecomponent.Notsurprisingly,thismeansthatitisimpossibletoprovidetrueseparatecompilationforSML[2].EventhesmartestrecompilationschemeproposedbyShaoandAppel[26]doesnotpermittrueseparatecompi-lationbecauseitdelayssometypechecking,andhencethedetectionofsometypeerrors,tolink-time.
Theneedfortypesharingconstraintsinfunctordefini-tionsismotivatedbysimilarproblems.Formalparameterscannotbeinspectedatcompile-timebecausetheiractualvaluesarenotknownuntilcompiletime.Instead,identitiesbetweentypecomponentsmustbewrittenexplicitlyusingsharingequations.Furtherextensionstothebasictheoryofdependenttypesareneededtodealwiththisandotherideasincludinggenerativity,polymorphism,abstraction,higher-ordermodules,andmodulesasfirst-classvalues.
2.2Dependenttypes
Motivatedbyproblemswithexistentialtypes,MacQueen[16]arguedthatdependenttypesprovideabetterbasisformodularprogramming.Inthisframework,structuresarerepresentedbypairsτ,Mcontainingbothatypecompo-nentτandatermMwhosetypemaydependonthechoiceofτ.Structuresofthisformcanbeviewedaselementsofadependentsumtype,describedinformallyby:
Σt.f(t)={τ,M|Mhastypef(τ)}.
Thetypingrulesfordependentsumsarestandard(see[18],forexample)andcanbewrittenintheform:
ΓM:[τ/t]τΓτ,M:(Σt.τ)
ΓM:(Σt.f(t))ΓsndM:f(fstM)
Theintroductionruleontheleftisverysimilartothecor-respondingruleforexistentialsexceptthattheimplemen-tationtype,τ,iscapturedinthestructureτ,Minthe
3
2.3Manifesttypes
RecentproposalsfortranslucentsumsbyHarperandLillib-ridge[6]andmanifesttypesbyLeroy[13]provideacompro-misebetweenexistentialtypinganddependentsums,allow-ingtheprogrammertoincludeadditionaltypeinformationinthesignatureforastructure.Forthesesystems,weuseanintroductionruleoftheform:
ΓM:[τ/t]τΓM:(∃t=τ.τ)
Noticethat,unlikethepreviouscases,theimplementationtypeτappearsintheinferredtypealthoughthiscanbehiddenbycoercingittoastandardexistentialtype:
ΓM:(∃t=τ.τ)ΓM:(∃t.τ)
Manifesttypesprovidegoodsupportforabstractionandseparatecompilation,althoughtheunderlyingtheoriesseemquitecomplex.Oneofthemaintechnicalproblemshasbeenthedifficultyinprovidingsufficientlygeneralandaccuratetypestocapturethefullytransparentbehaviourofhigher-orderfunctorsthatispredictedbyoperationalframeworks[27,17].Inrecentwork,Leroyhasshownhowacalculusofmanifesttypescanbemodifiedtoavoidthisproblem[15].Hissolutionrequiresanextensionofthetypelanguagetoincludefunctorapplication,furtherblurringthedistinctionbetweentypesandterms;thatis,betweenstaticanddy-namicsemantics.Thiswork,andanalternativesolution,arediscussedinmoredetailinthenextsection.
values;forexample,asfunctionarguments.Itiswellknownthatstandardtechniquesfortypeinferencedonotallowfunctionargumentswithpolymorphictypes.Fortunately,itisfairlyeasytodealwiththisinoursystem,first,byallowingtheprogrammertosupplyexplicittypeinformation,andsecond,becausetheuseofpolymorphismisclearlysignaledbythepresenceofrecordtypes.ThissubjectisdiscussedinmoredetailinSection4.4.
Wecanillustratetheuseofbothofthesefeatureswiththefollowingsignaturewhichprovidesarepresentationformon-ads[28]:
typeMonadm={bind::
unit::
∀a.∀b.ma→(a→mb)→mb;∀a.a→ma}
NotethatthekindinferencemechanismsreferredtoabovecanbeusedtoinferthattheparametermoftheMonadsignatureisaunarytypeconstructor,whiletheuniversallyquantifiedvariablesaandbinthetypeofbindrepresentarbitrarytypes.
3.1Polymorphismandsharing
Withtheexamplesofprevioussectionsinmind,wemightuseastructureoftypeComplexcasanimplementationofcomplexnumbers,andstructureswithtypesoftheformArithatodescribetheimplementationofarithmeticopera-tionsonvaluesoftypea.ThecompArithfunctiondiscussedinsomedetailabovecannowbetreatedasapolymorphicfunction:
compArithcompArithcpx
::=
∀t.Complext→Aritht...
3ParameterizedSignatures
Ineachoftheapproachesdescribedabove,thetypeofamoduleisgivenbyanexpressionoftheformQt.f(t)wheref(t)isasignature,parameterizedbyt,andQisaquantifier.Thegoalofthispaperistoshowthatwecanuseparame-terizedsignatureslikef(t)asbuildingblocksforamoduletypesystemandtreatquantifiersasaseparateissue.
Forpracticalreasons,itiscommontogrouprelatedfunc-tionstogetherinasinglestructuremappingvariablestovalues.Itfollowsthataparameterizedsignaturef(t)willusuallybearecordtypepairingvariablenameswithappro-priatetypeschemes.Therearetwoimportantaspectsofourapproachthatdistinguishitfromotherattemptstouserecordtypestoexplainmodularstructure(forexample,theworkofAponte[1]):
•Higher-orderpolymorphism:Inthegeneralcase,wewillwanttousebothtypesandtypeconstructorsassignatureparameters.ThisiseasilydealtwithusingakindsystemaswillbediscussedinSection4.Thereisnoadditionalburdenontheprogrammertosupplyexplicitkindinformation,becausethiscanbeinferredautomaticallyfromaprogramtext.Wealreadyhaveconsiderableexperiencewithsuchsystemsfromworkwithconstructorclasses[10]whichusesthesameideas;weknowthattheyworkwellinpractice.•Nestedpolymorphism:Inthegeneralcase,wewillwanttobeabletodefinestructureswithpolymorphiccomponentsandtousethesestructuresasfirst-class
4
Becausethesamevariable,t,appearsasaparametertoboththeComplexandArithsignatures,itisclearthatthetypeofvaluesthatthearithmeticoperationsintheresultcanbeappliedtoisthesameasthetypeofcomplexnum-bersthatareprovidedasanargument;thisachievesmuchthesameresultasatypesharingconstraintinSML.Inad-dition,thefactthattisuniversallyquantifiedensuresthatwedonotmakeanyassumptionsabouttheimplementationofcomplexnumbers.Thuspolymorphismisusefulasawayofexpressingtheindependenceoftheimplementationofamodulefromtheimplementationofitsimports.
Parameterizedsignaturescanalsobeusedtoexpressin-formationaboutthepropagationoftypeinformationinwaysthatarenotpossiblewithsharingequationsinSML.Forexample,inhisoriginalworkonmanifesttypes[13],Leroycommentsonthedifficultyofhandlingahigher-orderfunc-tor:
signatureS
=
sigtypet;...end
functorapply(functorf(x:S):S
structurea:S):S=fa
Theproblemhereisfindingawaytopropagateinformationabouttherelationshipbetweenthetcomponentsofthear-gumentandresultstructuresoff.Thisexamplehasbeenfurtheraddressedinrecentworkonfulltransparencyandhigher-ordermodules[3,15].Leroy’ssolutionistousea
manifesttypetospecifythatthetcomponentofastructureapplyfaisthesameasthetcomponentoffa;thisrequiresanextensiontoallowtheuseoffunctorapplicationsintypeexpressions.
Thereisactuallyanotherwaytosolvethisproblem,ascanbeseenusingparameterizedsignatures:
signatureSt
=
sig...end
functorapply(functorf(x:St):Su
structurea:St):Su=fa
Here,thetcomponentfromtheoriginalcodeisrepresentedbyaparameterofthesignatureS.Thedefinitionoftheapplyfunctorispolymorphicinthevariablestandu,andthiscapturesthedesiredrelationshipbetweenthetypesoftheargumentsandresultofapplyinadirectandconcisemanner.Asafurthercomment,noticethat,becausestruc-turescannowbeusedasfirst-classvalues,thereisnoneedtomakeadistinctionbetweenfunctorsandordinaryfunc-tiondefinitions.Infact,wecouldhavedefinedapplyasanordinaryfunction:
apply::∀a.∀b.(a→b)→a→bapplyfx
=
fx
Ifwehavealreadydefinedstructuresiandb,oftypesSIntandSBool,respectively,thenwecanuseeitherversionofapplytodeterminethatapply(λx.x)ihastypeSInt,andthatapply(λx.b)ihastypeSBool.
Anotheradvantageofamodulesystembasedonparam-eterizedsignaturesistheabilitytoprovideasimpletreat-mentforthedefinitionanduseofmoduleswithpolymorphictypes.RecentworkbyKahrs[11]showsthatsimpleformsofpolymorphismthatcanbeusedinthecorelanguageofSMLarenotpermittedinthemodulelanguage.Kahrsgivesexamplestoshowwhypolymorphismatthemodulelevelisusefulandshowshowitcanbesupportedbyextendingthelanguagewithanew,generalconstructfordescribingthebindingpositionoftypevariables.(Infact,thissamecon-structcouldalsobeusedasanotheralternativetoLeroy’srecentproposals[15]tohandletheapplyfunctordiscussedabove.)WecanillustratethebasicideabyobservingthatthetypecomponenttinanySMLstructurematchingthesignature:
signatureI=sig
typetid::t→tendmustbefixedtosomespecifictype,t.Asaresult,itisimpossibletodefineastructuresthatmatchesIandsuchthats.idisthepolymorphicidentityfunction.
Fortunately,thisproblemdoesnotoccurinourframe-workandadirecttranslationoftheexamplehere(andofthoseinKahrs’paper)yieldsthedesiredformofpolymor-phismwithoutanyfurtherwork.Thecorrespondingparam-eterizedsignatureisjust:
typeIt
=
{id::t→t}
andwecandefineastructure:
s::∀t.It
s
=
structid=λx.xend
5
Notonlydoesthisstructurehaveapolymorphictype—wecanalsousethevalues.idasapolymorphicidentityfunctionoftype∀t.t→t.Forreasonsofspace,wehavebeenforcedtorestrictourattentiontoaverysimpleexample;wereferthereadertoKahrs’paper[11]formorecompellingapplicationsofthisformofpolymorphism.
3.2Relationshipwithmanifesttypes
TheuseofparameterizedsignaturesiscloselyrelatedtothesystemofmanifesttypesdescribedinSection2.3.Toun-derstandthiscomment,weshouldthinkofamanifesttypeoftheform∃t=τ.τasakindof‘localdefinition’,muchasifithadbeenwrittenlett=τinτ,orasaconvenientnotationfortheresultofasubstitution[τ/t]τ.Nowletusrepeattherulefor∃-introductionandtheruleforcoercingamanifesttypetoanexistential,bothofwhichwerediscussedinprevioussections:
ΓM:(∃t=τ.τ)ΓM:[τ/t]τΓM:(∃t.τ)
ΓM:(∃t.τ)
Fromourcurrentperspective,theserulesarethesame!Withthisobservationinmind,itmightappearthatwehavenoth-ingtogainbyaddingmanifesttypestoatypesystemthatalreadyincludesexistentials.However,therearetworeasonswhysuchaclaimcouldbeconsideredasmisleading:•Forthepurposesoftheunderlyingtypetheory,someformofquantificationisnecessaryintheproposedcal-culiformanifesttypesandtransluscentsumstoac-countfortheinclusionoftypecomponentsinmodulevalues.Thisisatoddswithourapproach,whichdoesnotallowmodulestocontaintypecomponents.•Onemayarguethatthesyntaxformanifesttypesisbettersuitedtomodularprogrammingbecauseitavoidstheawkwardnessoflargenumbersofparame-ters,andmayrequirefewerchangestothesourceofaprogramifaparticularmoduleischanged,forexam-ple,byaddingtypecomponents.However,aswede-scribeinSection5.1,exactlythesamebenefitscanbeobtainedinasimpleandelegantfashionwithparam-eterizedsignaturesbypackaginggroupsofparametersintorecord-likestructures.Anotheradvantage,intheory,ofthemanifesttypeno-tationisthatatypelike∃t=τ.τmightbemuchmoreconciseandreadablethantheexpandedform[τ/t]τifτisacomplextypeexpressionoriftappearsseveraltimesinτ.Again,inpractice,thisisnotaseriousissuebecausethelanguagesthatweareinterestedin(forexample,SMLandHaskell)alreadyincludefacil-itiesfordefiningtypeabbreviationsorsynonyms,andthesecanbeusedtoachievethedesiredeffect.
3.3SimpleExamples
Sofar,wehavediscussedthemotivationandtheoreticalas-pectsofparameterizedsignatureswithoutmanyexamplestoshowhowcorrespondingstructuresmightbedefined.Notsurprisingly,thereareseveraldifferentnotationsthatwemightchosefrom.Forthepurposesofthispaper,andtofacilitateeasycomparison,wewilladoptaSML-likesyn-tax.However,toemphasizethedistinctionbetweenstatic
anddynamicsemantics,weseparateouttypedeclarationsandvaluedefinitions,inthestyleofHaskell.Also,becausestructuresarefirst-classvaluesandthereisnodistinctionbetweenthemoduleandcorelanguages,wecanomitthe(nowredundant)structureandfunctorkeywords.
Itisusefultostartwithacomparisonbetweenlocaldef-initions(letbindings)andstructures:
letdeclsinexpr
structdeclsend
4.1Kindsandconstructors
Tosupporthigher-orderpolymorphism,weneedtoallowtheuseofvariablesintypeexpressionstorepresent,notjustarbitrarytypes,butalsotypeconstructors.Followingstandardtechniques,weuseasystemofkinds,κ,todistin-guishbetweendifferentformsoftypeconstructor:
κ
::=|
∗
κ1→κ2
thekindofall(mono)typesfunctionkinds
Thecollectionofdeclarations,decls,introducedineachoftheseexpressionswillbetype-checkedinexactlythesameway.Theonlydifferenceisthat,inaletconstructthedeclaredvaluesareusedimmediatelyinthebodyexpr,whileinastructuretheyarepackagedupforlateruse.
First,hereisanimplementationofcomplexnumbersus-ingthestandardCartesianrepresentation:rectCpxrectCpx
::=
Complex(Float,Float)struct
mkCartxy=(x,y)
mkPolarrθ=(rcosθ,rsinθ)re(x,y)=x...end
Intuitively,thekindκ1→κ2representsconstructorsthattakeaconstructorofkindκ1andreturnaconstructorofkindκ2.
Foreachkindκ,wehaveacollectionofconstructorsCκ(includingconstructorvariablesακ)ofkindκgivenby:
Cκ
::=|||
χκακ
Cκ→κCκ{xi::σi}
constantsvariablesapplications
signatures,κ=∗
Otherthanrequiringthatthefunctionspaceconstructor→beincludedasanelementofC∗→∗→∗,wedonotmakeanyassumptionabouttheconstructorconstantsχκinthegrammarabove.
Thesymbolσrangesoverthesetoftypeschemesde-scribedbythegrammar:
τσ
::=::=|
C∗
∀ακ.στ
monotypes
polymorphictypes
Asitstands,theimplementationtypeofrectCpxiscapturedexplicitlyinitstype.Later,inSection5.3,wewilldescribehowtomakethistypeabstract,eithercompletelybyus-inganexistential,orpartiallybygivingitanamewithoutrevealinghowitisimplemented.
ThenextexampleisafragmentofthedefinitionofthecompArithfunction,whichcanbeusedtoconstructacom-plexarithmeticpackagefromanarbitrarycomplexnumberpackage:
compArith::Complext→ArithtcompArithc
=struct
plusz1z2=c.mkCart(c.rez1+c.rez2)
(c.imz1+c.imz2)
...endFinally,thefollowingdefinitionspecifiesthestructureofthelistmonad:
listMonad::MonadListlistMonad
=struct
unitx=[x](x:xs)‘bind‘f=fx++(xs‘bind‘f)[]‘bind‘f=[]endAlloftheexamplesgivenhereshouldseemstraightforward—and,ofcourse,thatisjustwhatwewant!
4Formaldevelopment
Thissectionprovidesabriefformaldescriptionofthetypesystemthatisputforwardinthispaperasabasisformod-ularprogramming.
6
NotethatthiscorrespondsverycloselytothewaythatmosttypeexpressionsarealreadywritteninHaskell.Forexam-ple,ListaisanapplicationoftheconstructorconstantListtotheconstructorvariablea.Inaddition,eachconstructorconstanthasacorrespondingkind.Forexample,writing(→)forthefunctionspaceconstructorand(,)forpairingwehave:
Int,Float,()::∗List::∗→∗(→),(,)::∗→∗→∗
Thesyntaxforconstructorsalsoincludesexpressionsoftheform{xi::σi}ofkind∗,whichisintendedasaconvenientab-breviationforrecordtypesoftheform{x1::σ1;...;xn::σn}.Thesewillbeusedprimarilytoassigntypestostructureval-ues.Notetheuseoftypeschemesratherthansimpletypes;thisallowsthesystemtosupportstructureswithpolymor-phiccomponents.Weshouldalsomentionthatitwouldbepossible,intheory,toencodemoduletypesastupleswithoutintroducingtheextrasyntaxforrecords.However,labelledtuplesareperhapsmoreconvenientinpractice,andwehavechosentoreflectthisdirectlyinourformulationofthetypesystem.
Typecheckerimplementationsusuallyincludeteststoensurethattypeexpressionsarewell-formed,forexample,thataparticularconstructorissuppliedwithanappropri-atenumberofarguments.Inthecurrentsetting,thiscanbereformulatedasthetaskofcheckingthataconstructorexpressionhaskind∗.Theapparentmismatchbetweentheexplicitlykindedconstructorexpressionsspecifiedaboveandtheimplicitkindingusedinexamplescanberesolvedbyaprocessofkindinference;thatis,byusingstandardtech-niquestoinferkindsforuserdefinedconstructorswithouttheneedforprogrammer-suppliedkindannotations.Thesameapproachhasbeenusedwithconsiderablesuccessinboththetheoryandpracticeofconstructorclasses[10].
4.2Terms
Forthepurposesofthispaper,itissufficienttorestrictourattentiontoasimpleλ-calculus,extendedwithtwocon-structs,oneforbuildingstructures,andanotherforselectingstructurecomponents:
M
::=|||||
xMMλx.M
letx=MinNM.x
structxi=Miend
variablesapplicationabstractionlocaldefinitionselectionstructures
typeinference.Infact,thefirstofthese,doesnotcauseanydifficultyatallbecausewehaveusedaweakformofhigher-orderpolymorphismthatavoidstheundecidabilityofhigher-orderunification.Thesecond,nestedpolymorphism,requiressomeformofexplicittypeinformation(althoughnothingmorethanwouldberequiredinanappropriateex-tensionofSML).
4.4.1Useofexplicittypeinformation
Theindexnotationinthelastlineofthisgrammarisusedtoreflectthefactthatastructuremayhavemultiplecom-ponents.
4.3Typingrules
Withthedefinitionsoftheprevioussectionsinplace,wecanusestandardnotationtospecifythetypingrulesofoursysteminFigure1.Notetheuseofthesymbolsτandσtorestricttheapplicationofcertainrulestotypesortypeschemes,respectively.Theconditionthatακ∈CV(A)in
TheneedforexplicittypeinformationinprogramsusingrecordswillalreadybefamiliartoSMLprogrammers;thedefinitionofSMLrequiresthattheshapeofanyrecord—acompletelistofitsfields—canbedeterminedatcompile-time.Whatwehavedescribedhereisanaturalgeneraliza-tionofthis;werequirenotonlythenamesofallofthefields,butalsothetypesforeveryfieldthatisreferenced.
Typeannotationsarenotnecessaryinmanysimpleex-amples.Forexample,thefollowingprogramtypecheckswithoutanyadditionaltypeinformation:
fx
=
struct
hz=[z]u=xend
m.h(m.hm.u)wherem=fy
vy
(var)(→E)(→I)(let)({}E)({}I)(∀E)(∀I)
(x:σ)∈A
Ax:σ
AE:τ→τAF:τ
AEF:τAx,x:τE:τAλx.E:τ→τ
AE:σAx,x:σF:τA(letx=EinF):τ
AE:{xi::σi}AE.xj:σjAEj:σj
forallj
Astructxi=Eiend:{xi::σi}
AE:∀ακ.σC∈Cκ
AE:[C/ακ]σAE:σ
ακ∈CV(A)
κ
=
Inthiscase,wecancalculatethefollowingtypesforthecomponentsinthestructurevalueinthedefinitionoff:
hu
::::
∀t.t→[t]a
whereaisthetypeoftheargumentx.Thus:
f
::
∀a.a→{h::∀t.t→[t];u::a}
anditfollowsthatvhastype∀a.a→[[a]].
Inpractice,explicittypeannotationsareonlyrequiredforthedefinitionofrecursiveormutuallyrecursivestruc-tures(whicharenotpermittedbytheSMLmodulesys-tem)orforfunctionsthatmanipulatestructurevalues(cor-respondingtoSMLfunctordefinitionswhereexplicittypeinformationisalsorequiredinSML,ortohigher-orderorfirst-classmoduleswhicharenotsupportedbySML).Forexample,thetypesignatureaccompanyingthefollowingdef-initioncannotbeomitted:
makeUnitmakeUnitxu
::=
a→Monadm→mau.unitx
AE:∀α.σ
Figure1:Typingrules
rule(∀I)isnecessarytoavoiduniversalquantificationoveravariablethatisconstrainedbythetypeassignmentA;theexpressionCV(A)denotesthesetofallconstructorvari-ablesappearingfreeinA.
Ontheotherhand,wearefreetostorevaluesofsometypeMonadmindatastructuressuchaslistsandtousemanyhigherorderfunctions,forexampleλz.map(makeUnitz),withoutfurthertypeannotations.
SomemayquestiontheneedforexplicittypeinformationinalanguagethatisbasedonaHindley-Milnertypesystem,butwedonotbelievethatthiswillhaveanysignificantimpactonprogrammers:
•Someformofexplicittypeinformationisalreadynec-essaryinmanylanguagesbasedonHindley-Milnertyp-ing.Forexample,thisincludestheoverloadingmecha-nismsofHaskell;thetreatmentofrecords,arithmetic,andstructuresinSML;andthenotationsusedtode-finenewdatatypesineachlanguage.
7
4.4Typeinference
Althoughitreallyhaslittletodowiththedesignofamod-ulesystemitself,somereadersmaybeconcernedabouttheeffectsofaddinghigher-orderandnestedpolymorphismtothetypesystemofalanguagethatisbasedontheuseof
•Explicittypeannotationsareonlyrequiredinsitua-tionswheretheywouldalreadyberequiredbypro-gramsusingtheSMLmodulesystem,orinprogramsthatcannotbewrittenwithSMLmodules.•Despitethefactthatitisnotnecessary,theuseoftypeannotationsinimplicitlytypedlanguageslikeMLandHaskelliswidelyrecognizedas‘goodprogrammingstyle’,andmanyprogrammersalreadyroutinelyin-cludetypedeclarationsintheirsourcecode.Thetypeassignedtoavalueservesasausefulformofprogramdocumentation.Inaddition,thisgivesasimplewaytocheckthattheprogrammer-suppliedtypesignatures,reflectingintentionsaboutthewayanobjectwillbeused,areconsistentwiththetypesobtainedbytypeinference.Itisimportanttofindaformalmechanismthatcanbeusedtodescribewhenadditionaltypeinformationisre-quiredforagivenprogram,andtoindicatewhatformitshouldtake.Thiscanalreadybeachievedbyselectingaparticularimplementationofthetypeinferencealgorithm.However,thisrisksover-specificationandwewouldprefertofindamoreabstract,andlessoperationalalternative.
whichcanappearintypes;thisisreflectedbythefactthatthetwoexpressionswillbeassigneddifferentkinds.
Withthisapproach,sharingconstraintscanbeunder-stoodasaformofqualifiedtype[9]:
prog
::(r.x=s.y)⇒SIGr→SIGs
Theconstraint(r.x=s.y)appearinghereindicatesthatthexandyfieldsofrands,respectively,mustbeequal.Notethatwedonotneedtomentionanyotherfieldsoftherandsrecords,oreventoknowthatthereareanyotherfields.
Anotherinterestingobservationisthatthetypeofprogdoesnotmakeanyreferencestotermlanguageconstructs.ThiswouldnotbetrueinSMLwherethenamesoffunctorparametersserveanadditionalroleaslabelsforthesigna-turesappearinginatype.ThisalsohelpstoexplaintheproblemsoftypingtheapplyfunctorinSection3.1becausethereisnoobviouslabelforthesignatureoftheresultofapplyingftoxinthedefinition:
functorapply(functorf(x:S):S
structurea:S):S
=fa
Withourapproach,eachsignaturehasanobviouslabel;therecordofconstructorsthatareusedasitsparameters.Aswehavealreadyseen,thismakesiteasytoassignausefulandgeneraltypetoapplywithoutanyextensionstothelanguage.
5Concernsaboutmodularity
Inadditiontoformalconcerns,thereareanumberofprag-maticissuesthatmustbeaddressedinthedesignofamod-ulesystem.Weclaimthatthesystemofparameterizedstructurespresentedhereissuitableasamodulesystem,butourcurrentprototypeisnotsufficientlycompletetohaveallowedustoobtainpracticalexperiencewithitonalargescaleprogrammingproject.Theaimofthissectionistodo‘thenextbestthing’bydiscussinganumberofis-suesthathavebeensuggestedasimportantpropertiesformodulesystems,andshowinghowtheyaredealtwithintheframeworkofthispaper.
5.2Typecomponents
5.1Signatureparametersandsharing
ItiseasytofindapplicationsofSMLthatusemoduleswithfairlylargenumbersoftypecomponents;beingforcedtospecifyavalueforeveryparameterofthecorrespondingsignatureinourframeworkwouldbeawkwardandincon-venient.TheSMLnotation,andinparticularsharingcon-straints,arealsomorerobustinthesensethat,ifextratypecomponentsareaddedtoasignature,thenwedonotneces-sarilyhavetomodifytheprogramaswemight,forexample,toaddanextraparametertoeachuseofaparameterizedsignature.
Infact,ifwepackageparameterstogetherinrecords,thenparameterizedsignaturescanofferthesameadvan-tages.TheonlychangethatweneedtomaketotheformaldevelopmentinSection4istoaddnewsyntaxforrecordsofconstructors:
κCκ
::=...|{ti::κi}::=...|C{ti::κi}.tj|{ti=Cκi}
recordkinds
selection,ifκ=κj
construction,κ={ti::κi}
Inthesystemthatwehavebeendescribinginthispaper,modulesdonotincludetypecomponents.Instead,weusesignatureparameterstocapturerelationshipsbetweenstruc-turecomponentsandimplementationtypes.Thisisasignif-icantdeparturefromsomeofthepreviouswork,forexam-ple,insystemsbasedondependenttypeswheretypecom-ponentsplayacentralrole.However,wearguethatmuchcanbeaccomplishedwithouttypecomponents.This,webe-lieve,isalsomoreinthespiritoftheHindley-Milnertypesystem.Forexample,inMilner’soriginalwork[19],typesareusedasapurelysemanticnotion,representingsubsetsofasemanticdomain,notasanyconcreteformofvalue.
Akeyobservationisthattypedefinitionswithinamod-ulecanbeliftedtothetop-level.Forexample,considerthefollowingSMLfragment:
structures=struct
typeTdataLista...end
==Int
Nil|Consa(Lista)
Despiteappearances,thetypesynonymTandthetypecon-structorListarenotlocaltothedefinitionofs.Atanypointintheprogramwheresisinscope,thesetypeconstructorscanbeaccessedbythenamess.Tands.List,respectively.Renaminganyreferencestothesetypesandtheirconstruc-torsinthebodyofs,wecanliftthesedefinitionstothetop-level,toobtainthefollowingdefinitions:
types.Tdatas.Listastructures
8
===
Int
s.Nil|s.Consa(s.Lista)...
Itisimportanttounderstandthedifferencebetweenrecordsofconstructors{ti=Cκi}andsignatures{xi::σi},bothof
Ineffect,allthatthedatatypedefinitionsintheoriginalSMLprogramaccomplishistodefinetop-leveldatatypesinwhichthetypeandvalueconstructornamesaredecoratedwiththenameofthestructureinwhichtheyaredefined.
Insomesituations,renamingisnotsufficienttoallowtypedefinitionstobeliftedtothetop-level.Forexample,theListdatatypeinthefollowingfunctordefinitioninvolvesa‘freevariable’,thetypex.T,acomponentoftheargumentstructurex:
functorf(x:SIG):SIG=struct
dataList=Nil|Consx.TList...end
Thesolutioninthiscaseistoaddanextraparametertothedatatypedefinitionbeforemovingittothetop-level,asshowninthefollowingcodefragment.Thisisjustaformofλ-lifting[8,25]:
dataf.Listtffx
=|::=
f.Nil
f.Constf.List
SIGt→SIG(f.Listt)...
Noticehowtheparameterizedsignaturesinthetypeforfcapturetherelationshipbetweenthetypesinvolvedintheargumentxandthoseinvolvedintheresultfx.Becausetheformofhigher-orderpolymorphismdescribedinSection4.1allowstypeconstructorstobeusedasbothsignatureanddatatypeparameters,thesametechniquecanbeusedtodealwithtypeconstructorcomponentsoffunctorarguments.
InSML,thetwofunctordefinitionsabovearenotequiv-alent;SMLadoptsanotionofgenerativity,producinganewtypeconstructoreachtimethefunctorisappliedtoanar-gument.Thustwodefinitions:
structures1structures2
==
f(x)f(x)
Infact,weregardthisasadistinctadvantagebecauseitallowsustotreattheissueofabstractionasaseparateconcern.Forexample,onepossibilityistoincludesupportforexistentialtypes,perhapsusingtheapproachdescribedinSection2.1,orthedot-notation[4],orthecombinationoftypeinferenceandexistentialtypingthathasbeenexploredbyL¨aufer[12].
However,wehavealsoseenthatexistentialtypesarenotalwaysappropriate.Fortunately,itisalsopossibletoextendthelanguageinamodularfashionwithconstructsthatal-lowtheprogrammertoprovideanameforadatatypebuttorestrictthescopeofitsconstructorsandselectorstoaparticularcollectionofbindings.Thisisessentiallywhattheabstypeconstructusedinseveraldifferentlanguagesachieves,andiscloselyrelatedtotheconceptofSkolemiza-tioninpredicatelogic.Notethatthisdoesnotrequireanychangestotheunderlyingtypetheoryandisperhapsbestdealtwithatthelevelofcompilationunitsratherthanthecorelanguage.
Webelievethatbothoftheseapproachesareusefulintheirownright.However,neithercoincidesexactlywiththeformofabstractdatatypesprovidedbygenerativityinSMLwhichfallssomewherebetweenthetwoextremesofnamedandexistentiallyquantifiedabstractdatatypes.ItseemsunlikelythatthereisamodularextensionofoursystemthatprovidesexactlythesameformofabstractionasSML.
6Conclusion
willproducestructureswithincomparabletypecomponents.Intruth,whenweuseanSMLfunctorto‘generate’anewdatatype,weareinfactconstructinganewinstanceofafixeddatatype,whichisthenhidden,inessence,byaformofexistentialquantification.ThereisnowaytoexpresstheListtypeproducedbyapplyingftoanappropriateargu-mentstructureinthenotationofSML,soweareforcedtopackageupinstantiationoftheactualimplementationtype,f.List,andhidingoftheresultingtypeasasingleoperation.
Liftingtypedefinitionstothetop-levelallowsustoex-pressthetypecomponentsoftheresultoffunctorapplica-tions;fortheexampleabove,ifxhastypeSIGt,thenboths1ands2havetypeSIG(f.Listt).Wearethenfreetotreatthequestionofwhetherwewishtoconcealtheseim-plementationtypesasaseparateconcern.Variousmethodsforachievingthisaredescribedinthenextsection.
Thereareanumberofproposalsfortype-theoreticfounda-tionsofmodularprogramming.Someofthesesystemsareverypowerful,butrequiresignificantandcomplexextensionandmodificationtoaccountforfeaturesthatareusefulinpractice.
Ourworkshowsthattheever-increasingcomplexitythatwehaveseeninrecentworktoformalizemodulesystemscanbeavoidedandthatother,simple,expressive,andviableoptionsareavailable.
Inthispaper,wehavepresentedasimpletypesystemthatprovides:
•Supportforhigher-orderpolymorphism.
•Supportforstructureswithpolymorphiccomponents.•Aclearseparationbetweenstaticanddynamicseman-tics.Thisleadstoamodulesysteminwhich:•Structuresarefirst-classvalues.
•Higher-ordermodules(i.e.,first-classfunctors)aread-mitted.•Polymorphicmodulesandstructuresmaybedefined.•Trueseparatecompilationispossible.
•Parametricpolymorphismplaysamajorrole,makingthesystemeasiertolearnforprogrammerswhoareal-readyfamiliarwiththecorelanguagesofSML,Haskellorsimilarlanguages.Bycontrast,noneoftheseispossiblewiththeSMLmodulesystem.
Oneofthemaintopicsforfutureresearchistoinvesti-gatetheroleofimplicitsubsumption;thatis,theabilityto9
5.3Abstraction
Inthecontextofmodulesystems,thetermabstractionisusedtotodescribetheabilitytohideinformationabouttheimplementationofamoduleandtoprotectitagainstmisuse.Thisisanimportantfeatureinpracticalsystemsbuttheuseofparameterizedsignaturesdescribedinthispaperdoesnotitselfprovideanywayofconstructinganabstractdatatype.
discardelementsfromastructureasaresultofsignaturematchinginSML.Webelievethatthiscanbeaccomplishedusingasimpleformofsubtyping,guidedbytypeannota-tions,orotherwisebyextendingthesystemwithamech-anismforcontrollingthesetofbindingsthatareexportedfromastructure.
[9]MarkP.Jones.QualifiedTypes:TheoryandPrac-tice.PhDthesis,ProgrammingResearchGroup,Ox-fordUniversityComputingLaboratory,July1992.Pub-lishedbyCambridgeUniversityPress,November1994.[10]MarkP.Jones.Asystemofconstructorclasses:over-loadingandimplicithigher-orderpolymorphism.Jour-nalofFunctionalProgramming,5(1),January1995.[11]StefanKahrs.First-classpolymorphismforML.In
D.Sannella,editor,Programminglanguagesandsys-tems–ESOP’94,NewYork,April1994.Springer-Verlag.LectureNotesinComputerScience,788.[12]KonstantinL¨auferandMartinOdersky.Anexten-sionofMLwithfirst-classabstracttypes.InACM
SIGPLANWorkshoponMLanditsApplications,SanFrancisco,June1992.[13]XavierLeroy.Manifesttypes,modulesandseparate
compilation.InConferencerecordofPOPL’94:21stACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages109–122,Portland,OR,January1994.[14]XavierLeroy.Asyntactictheoryoftypegenerativity
andsharing.InRecordofthe1994ACMSIGPLANWorkshoponMLanditsApplications,Orlando,FL,June1994.[15]XavierLeroy.Applicativefunctorsandfullytrans-parenthigher-ordermodules.InConferencerecordofPOPL’95:22ndACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages.ACM,Jan-uary1995.[16]DavidMacQueen.Usingdependenttypestoexpress
modularstructure.In13thAnnualACMSymposiumonPrinciplesofProgramminglanguages,pages277–286,St.PetersburgBeach,FL,January1986.[17]DavidB.MacQueenandMadsTofte.Asemanticsfor
higher-orderfunctors.InD.Sannella,editor,Program-minglanguagesandsystems–ESOP’94,NewYork,April1994.Springer-Verlag.LectureNotesinCom-puterScience,788.[18]PerMartin-L¨of.Constructivemathematicsandcom-puterprogramming.InLogic,MethodologyandPhilos-ophyofScience,VI.NorthHolland,Amsterdam,1982.[19]R.Milner.Atheoryoftypepolymorphisminprogram-ming.JournalofComputerandSystemSciences,17(3),
1978.[20]RobinMilner,MadsTofte,andRobertHarper.The
definitionofStandardML.TheMITPress,1990.[21]JohnMitchellandRobertHarper.TheessenceofML.
InFiftheenthACMSymposiumonPrinciplesofPro-grammingLanguages,SanDiego,CA,January1988.[22]JohnMitchell,SigurdMeldal,andNeelMadhav.An
extensionofStandardMLmoduleswithsubtypingandinheritance.InConferencerecordoftheEighteenthAn-nualACMSymposiumonPrinciplesofProgrammingLanguages,Orlando,FL,January1991.
Acknowledgements
SomeoftheideaspresentedinthispaperweredevelopedwhiletheauthorwasamemberoftheDepartmentofCom-puterScience,YaleUniversity,supportedinpartbyagrantfromARPA,contractnumberN00014-91-J-4043.
ThankstoPaulHudak,ShengLiang,BobHarper,ColinTaylorand,inparticular,DanRabin,XavierLeroy,andGrahamHuttonfortheirvaluablecommentsandsugges-tionsduringthedevelopmentoftheideaspresentedinthispaper.ThanksalsotoPaulHudak,LindaJoyceandChih-PingChenfortheirhelpinpreparingtheoriginalsubmis-sion.
References
[1]Mar´ıaVirginiaAponte.Extendingrecordtypingto
typeparametricmoduleswithsharing.InProceedings20thSymposiumonPrinciplesofProgrammingLan-guages.ACM,January1993.[2]AndrewW.AppelandDavidB.MacQueen.Separate
compilationforStandardML.InConferenceonPro-grammingLanguageDesignandImplementation,Or-lando,FL,June1994.[3]SandipK.Biswas.Higher-orderfunctorswithtranspar-entsignatures.InConferencerecordofPOPL’95:22ndACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages.ACM,January1995.[4]LucaCardelliandXavierLeroy.Abstracttypesandthe
dotnotation.TechnicalReportreport56,DECSRC,1990.[5]LucaCardelliandPeterWegner.Onunderstanding
types,dataabstraction,andpolymorphism.ComputingSurveys,17(4),December1985.[6]RobertHarperandMarkLillibridge.Atype-theoretic
approachtohigher-ordermoduleswithsharing.InCon-ferencerecordofPOPL’94:21stACMSIGPLAN-SIGACTSymposiumonPrinciplesofProgrammingLanguages,pages123–137,Portland,OR,January1994.[7]RobertHarper,JohnC.Mitchell,andEugenioMoggi.
Higher-ordermodulesandthephasedistinction.InConferencerecordoftheSeventeenthAnnualACMSymposiumonPrinciplesofProgrammingLanguages,pages341–354,SanFrancisco,CA,January1990.[8]T.Johnsson.Lambdalifting:transformingprograms
torecursiveequations.InJouannaud,editor,Proceed-ingsoftheIFIPconferenceonFunctionalProgrammingLanguagesandComputerArchitecture,pages190–205,NewYork,1985.Springer-Verlag.LectureNotesinComputerScience,201.
10
[23]JohnC.MitchellandGordonD.Plotkin.Abstract
typeshaveexistentialtype.ACMTransactionsonPro-grammingLanguagesandSystems,10(3):470–502,July1988.[24]EugenioMoggi.Acategory-theoreticaccountofpro-grammodules.InSummerconferenceoncategorythe-oryandcomputerscience,pages101–117,NewYork,1989.Springer-Verlag.LectureNotesinComputerSci-ence,389.[25]S.L.PeytonJones.Theimplementationoffunctional
programminglanguages.PrenticeHall,1987.[26]Z.ShaoandA.Appel.Smartestrecompilation.InPro-ceedings20thSymposiumonPrinciplesofProgrammingLanguages.ACM,January1993.[27]MadsTofte.Principalsignaturesforhigher-orderpro-grammodules.InConferencerecordoftheNineteenthannualACMSIGPLAN-SIGACTsymposiumonPrin-ciplesofProgrammingLanguages,January1992.[28]P.Wadler.Theessenceoffunctionalprogramming(in-vitedtalk).InConferencerecordoftheNineteenthan-nualACMSIGPLAN-SIGACTsymposiumonPrinci-plesofProgrammingLanguages,pages1–14,Jan1992.
11
因篇幅问题不能全部显示，请点此查看更多更全内容