Formal semantics of the FLINT intermediate languag

FormalSemanticsoftheFLINTIntermediateLanguage(Yale-CS-TR1171)ChristopherLeagueZhongShaoMay5,1998Contents1Overview31.1FormalSemanticsofFLINT.....................41.2TypeCheckerforFLINT......................52FLINTAbstractSyntax82.1TypeLanguage............................82.2TermLanguage............................102.3DiscrepanciesintheImplementation................133StaticSemantics153.1Notation................................153.2TypeLanguage............................163.2.1ConstructorFormation....................163.2.2ConstructorReduction....................183.2.3ConstructorEquivalence...................203.2.4TypeFormation.......................213.3TermLanguage............................224DynamicSemantics284.1TheFramework............................284.2TheAbstractMachine........................304.3Expressions..............................304.4ImperativePrimops.........................344.5First-ClassContinuations......................344.6Properties...............................342Chapter1OverviewAllmoderncompilerstranslateasourcelanguagetosomeintermediatelanguageinwhichtransformationsaremadeandfromwhichmachinecodeisgenerated.Somecompilersareabletotranslatemultiplesourcelanguagestothesameintermediatelanguage.Forexample,thepopularfreecompilergcc[Sta]usesanintermediatelanguagecalledRTLandshipswithfront-endstosupportC,C++,andObjectiveC.Front-endsforAda9X,Fortran,Modula-3,andPascalareunderdevelopment[Sta].Thisisquiteadvantageousbecausethecodethatoperatesontheintermediatelanguage(the“middle”end)andthattranslatesittomachinecode(thebackend)canbesharedbyallthedifferentcompilers.Recently,compilersforpolymorphically-typedfunctionallanguageshavebe-gunusingstrongly-typedintermediatelanguages.ExamplesareSML/NJ[SA95],TIL/ML[TMC+96],ML-Kit[Tof98],andGHC[Pey92].Thesecompilerstype-checkthesourceprogram,thentranslateboththeprogramandthetypesintotheintermediatelanguage.Thenthemiddleendcanusethetypestoguidead-vancedoptimizations(especiallythoserelatedtodatarepresentation)[PL91,Ler92,Mor95,Sha97a,Dan96]andtohelpgenerateprovablysecureobjectcode[GJS96,Nec97,LY97,MWCG98,LR98].Sofar,however,typedintermediatelanguageshaveonlybeenusedinacom-pilerforasinglesourcelanguage.Oneofthelong-termgoalsofmyresearchistobuildacompilerinfrastructurethatmakesthebenefitsoftype-preservingcompilationavailabletoavarietyofsourcelanguages.Moreover,suchanin-frastructurewouldallowrelativelyquickgenerationofsophisticatedcompilersforhigher-orderdomain-specificlanguagesaswell.[Sha97b].Webelievetypedintermediatelanguageswillbringevenmorebenefitstoanenvironmentinwhichmultiplelanguagesmustinteroperate.Whentwopiecesofintermediatecodeareproducedbytwodifferentfrontends,wecanusethetypestoreasonaboutfine-graininteroperabilityand,forexample,compatibilityofdatarepresentations.FLINT[Sha97b]isatypedintermediatelanguagebasedonapredicativevariantofFω,theGirard-Reynoldspolymorphicλ-calculus[Gir72,Rey74].ItistheintermediatelanguageusedinthelatestreleaseoftheSML/NJcom-34CHAPTER1.OVERVIEWpiler[SA95].TypeinferenceforFωisundecidable,soourlanguagehasexplicittypeannotations.Wealsohaveexplicittypeabstractionandapplicationwithwhichtoachievepolymorphism,andwesupportawiderangeofprimitivetypesandoperations.Themaincontributionsofmyworkareasfollows:•IformulatedthestaticanddynamicsemanticsoftheFLINTlanguage.•IhelpedimplementanefficienttypeandkindcheckerfortheFLINTlanguage.Ithasbeenincludedinthelatestdevelopers’releaseofSML/NJ.•Iclassifiedandorganizedtheprimitivetypesandoperationssupportedbythecompiler,andshowedhowthesecouldbemademoreeasilyextensible.ThiswaspresentedinmyOGSTonFebruary17,1998.•IformulatedthestaticanddynamicsemanticsoftheTigerlanguage[App97],asmallbutsufficientlyinterestingimperativelanguagethatwewilluseasatest-bedforinteroperationwithSML.Thisworkisdescribedin[Lea97].Inthenextfewsections,Iwilldescribethefirsttwocontributionsinmoredetail,tellingwhytheyareinterestingandnon-trivial,andhowtheyrelatestoothers’work.Theremainingchaptersofthisdocument(fromatechnicalreportinpreparation)describethefullformalsemanticsoftheFLINTlanguage.1.1FormalSemanticsofFLINTAformally-specifiedsemanticsisinvaluableforspecifyingtranslationsinto(andtransformationswithin)theintermediatelanguage.Forexample,flexiblerepre-sentationanalysis[Sha97a]isdefinedasatransformationonaformallydefinedcoreFLINTcalculus,andthetranslationoftheSMLmodulelanguagetoaFLINT-likecalculuswasformalizedin[Sha97c].Theseformalizations,however,dealonlywithasmallsubsetoftheactuallanguage.Restrictiontoasubsetisquitereasonableinthesepapers,sincenotallFLINTconstructsposeanyparticularchallengefor,say,representationanalysis.Likewise,notallthefeaturesareusedbytheSMLmodulelanguage.Furthermore,simplificationhelpsachieveaclearpresentation.Nevertheless,manyfeaturesomittedinthesecoreformulationshaveaddedconsiderablecomplexitytoboththeimplementationofFLINTanditstheoret-icalfoundations.Furthermore,mostofthesefeaturesarerequiredtosupportSML‘97[MTHM97].Inotherwords,theyquitefundamental:•Multiplefunctionargumentsandresults.•[Mutually]recursiveandsumtype