Type and behaviour reconstruction for higher-order

TypeandBehaviourReconstructionforHigher-OrderConcurrentProgramsTorbenAmtoft,FlemmingNielson,HanneRiisNielsonDAIMI,AarhusUniversityNyMunkegade,DK-8000˚ArhusC,Denmark{tamtoft,fn,hrn}@daimi.aau.dkNovember13,1995AbstractInthispaperwedevelopasoundandcompletetypeandbehaviourinferencealgorithmforafragmentofCML(StandardMLwithprimitivesforconcur-rency).Behavioursresembletermsofaprocessalgebraandyieldaconciserepresentationofthecommunicationstakingplaceduringexecution;typesaremostlyasusualexceptthatfunctiontypesand“delayedcommunicationtypes”arelabelledbybehavioursexpressingthecommunicationsthatwilltakeplaceifthefunctionisappliedorthedelayedactionisactivated.Thedevelopmentofthepresentpaperimprovesapreviouslypublishedalgorithminachievingcompletenessaswellassoundness;thisisduetoanalternativestrategyforgeneralisingovertypesandbehaviours.Chapter1IntroductionItiswell-knownthattestingcanonlydemonstratethepresenceofbugs,nevertheirabsence.Thishasmotivatedavastamountofsoftwarerelatedactivitiesonguaranteeingstatically(thatis,atcompile-timeratherthanrun-time)thatthesoftwarebehavesincertainways;aprimeexampleistheformal(andusuallymanual)verificationofsoftware.Inthislineofactivitiesvariousnotionsoftypesystemshavebeenputforwardbecausetheseallowstaticchecksofcertainkindsofbugs:whileatrun-timetheremaystillbeaneedtocheckfordivisionbyzerotherewillneverbeaneedtocheckfortheadditionofbooleansandfiles.Asprogramminglanguagesevolveintermsoffeatures,likemodulesystemsandtheintegrationofdifferentprogrammingparadigms,theresearchon“typesystems”isconstantlypressedfornewproblemstobetreated.Ourresearchhasbeenmotivatedbytheintegrationofthefunctionalandconcurrentprogrammingparadigms.ExampleprogramminglanguagesareCML[Rep91]thatextendsStandardMLwithconcurrency,Facile[PGM90]thatfollowsasimilarapproachbutmoredirectlycontainssyntaxforex-pressingCCS-likeprocesscomposition,andLCS[BS94].Theoverallcom-municationstructureofsuchprogramsmaynotbeimmediatelyclearandhenceonewouldliketofindcompactwaysofrecordingthecommunicationstakingplaceduringexecution.Onesuchrepresentationisbehaviours,akindofprocessalgebraexpressions.In[NN93]and[NN94a]inferencesystemsaredevelopedthatextendtheusu-alnotionoftypeswithbehaviours.Applicationsofsuchinformationare1demonstratedin[NN94a]and[NN94c].Thequestionremains:howtoimplementtheinferencesystem,i.e.howtoreconstructthetypesandbehaviours?ItseemssuitabletouseamodifiedversionofalgorithmW[Mil78].Thisalgorithmworksbyunification,butsinceourbehavioursconstituteanon-freealgebra(duetothelawsimposedonthem)thisapproachisnotimmediatelyfeasibleinourframework.Insteadweemploythetechniqueofalgebraicreconstruction[JG91,TJ92];thatisthealgorithmunifiesthefreepartofthetypestructureandgeneratesconstraintstocaterforthenon-freeparts.Thisideaiscarriedoutin[NN94b],whereareconstructionalgorithmispre-sentedwhichissoundbutnotcomplete.Thealgorithmreturnstwokindofconstraints:C-constraintsandS-constraints.TheC-constraintsrepresentthe“monomorphic”aspectsoftheanalysiswhereastheS-constraintsareneededtocopewithpolymorphism:theyexpressthatinstancesofpolymor-phicvariablesshouldremaininstancesevenafterapplyingasolutionsubsti-tution.UsingS-constraintsisnotastandardtoolwhenanalysingpolymor-phiclanguages;theyseemtobeneededbecausetheC-constraintsapparentlylacka“principalsolutionproperty”(aphenomenonwell-knowninunifica-tiontheory).Findinga“canonical”solutiontoC-constraintsisfeasibleasshownin[NN94b];insufficientlysimplecasesthissolutioncanbeshowntobe“principal”.Thepresentpaperimproveson[NN94b]by(i)achievingcompletenessinadditiontosoundness,bymeansofanothergeneralisationstrategy(madepossiblebyadifferentformulationofS-constraints);(ii)avoidingsomere-dundancyinthegeneratedconstraints(andinthecorrectnessproofs).Forsimplecasesweshowhowtosolvetheconstraintsgenerated,butitremainsanopenproblemhowtosolvetheconstraintsingeneralandhowtocharac-terisethesolutionas“principal”.ThisisrelatedtothefactthatS-constraintscanbeviewedasaspecialcaseofsemi-unification.OverviewofpaperChapter2and3setupthebackgroundforthepresentwork:inChapter2wegiveabriefmotivatingintroductiontoCMLandbehaviours,andinChapter3wepresenttheinferencesystemfrom[NN94a].Chapter4containsade-tailedmotivationforourdesignofthereconstructionalgorithmW.Chapter25elaboratesonourchoiceofgeneralisationstrategy.InChapter6and7thealgorithmisshowntobesoundandcomplete;theproofscanbefoundinAppendixBandC.InChapter8weshowhowtosolvetheconstraintsgeneratedforsomespecialcases.Chapter9concludes.ExampleoutputfromourprototypeimplementationisshowninAppendixA.3Chapter2CML-expressionsandbehavioursCML-expressionsearebuiltfromidentifiersx,constantsc,applicationse1e2,monomorphicabstractionsλx.e0,polymorphicabstractionsletx=e1ine0,conditionalsife0thene1elsee2,recursivefunctiondefinitionsrecf(x)⇒e0,andsequentialcompositione1;e2.ThisismuchlikeML,theconcurrentaspectsbeingtakencareofbytheconstantscsomeofwhichwillappearintheexamplebelow:Example2.1ThefollowingCML-programmap2isaversionofthewell-knownmapfunctionexceptthataprocessisforkedforeachtailwhiletheforkingprocessitselfworksonthe