Pets & Animals

9 pages
7 views

Concrete syntax for data objects in functional languages

of 9
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Share
Description
Concrete syntax for data objects in functional languages
Transcript
  ConcreteSyntaxforDataObjects  inFunctionalLanguages   AnnikaAasaKentPeterssonDanSynek  ProgrammingMethodologyGroup Dept.ofComputerScience, Univ.ofG oteborgandChalmers, S-41296G oteborg, Sweden  1Introduction  Manyfunctionallanguageshaveaconstruction todeneinductivedatatypesHoa75](also calledgeneralstructuredtypesPJ87],struc- turesLan64],datatypesMil84]andfreealge- brasGTWW77]).Aninductivedenitionofa datatypecanalsobeseenasagrammarfor alanguageandtheelementsofthedatatype asthephrasesofthelanguage.Sodeningan inductivedatatypecanbeseenasintroduc- inganembeddedlanguageofvaluesintothe programminglanguage.Thiscorrespondenceis howevernotfullyexploitedinexistingfunctional languages.Theelementscanpresentlyonlybe writteninaveryrestrictedform.Theyarejust theparsetreesoftheelementswritteninprex form.Ageneralization,thatwewillconsiderin thispaper,istoallowtheelementstobewritten inamoregeneralform.Insteadofdirectlywrit- ingtheparsetreesoftheembeddedlanguage, wewouldliketouseamoreconcretesyntactical formandletanautomaticallygeneratedparser translatetheconcretesyntacticalformtothe correspondingparsetree.Wethinkthatthisis especiallyusefulwhenwemanipulatelanguages inprograms,forexample,whenimplementing compilers,interpreters,programtransformation systems,andprogramminglogics.Itisalsocon- venientifwewanttousetheconcretesyntaxfor otherkindsofdatainaprogram. Byallowingdistxoperatorsinaprogramming languagePJ86],itispossibletoachievesomeof thegoalswehavepresentedabove.Theprob- lemisthatthesymbolscomprisingthedistx operatormustnotinterferewiththeconstruc- tionsoftheprogramminglanguageitself.Ifwe wanttorepresentprogramsofalanguageinthe languageitself,thisproblembecomesacute.For example,torepresentarithmeticexpressionsin- sideafunctionallanguage,itisdicult,butnot impossible,tolet`x+23'inonesituationbean expressionwhichevaluatestoanintegerandin anotheravaluethatrepresentsanarithmeticex- pression.Wecansolvethisprobleminatleast twodierentways.Wecaneithersaythatthe distxoperatormustbebuiltupfromidenti- ersoftheprogramminglanguageorwecan makeacleardistinctionbetweentheprogram- minglanguage,the  metalanguage  ,andtherepre- sentedlanguage,the  objectlanguage  .Ofcourse wecanrelaxthesituationintherstcasealittle byallowingoverloadedidentiersandoperators inthemetalanguage,butitishardtoimagine howpuresyntacticalconstructionsofthemeta- language,forexamplereservedwords,couldbe overloaded.  2ConcreteDataTypes  Westartbyintroducingasyntacticalconstruc- tionintoourfavoritefunctionallanguage(ours isML),todeneaconcretedatatypeofbinary numbers  1  as:  conctypeBinNumber=|0|] ||1|] ||<BinNumber>0|] ||<BinNumber>1|]  Comparethetypedenitionwiththecontext freegrammarforbinarynumbers  1  Weignorethatbinarynumbersarenotafreedata type.  1   <BinNumber>::=0 |1 |<BinNumber>0 |<BinNumber>1  Sincewemustnotconfusethesymbolsofthe denedlanguage(theObjectLanguage{OL) withthesymbolsoftheprogramminglanguage (theMetaLanguage{ML),weenclosetheel- ementsin  quotationbrackets  ,  |...|]  .Notice thatthenonterminalsinthegrammarcorre- spondtotypesinthetypedenition.Theinten- tionistointroduceadatatypeforbinarynum- bersandlettheelementsbewritteninthefamil- iarway.Soinaprogramwewouldliketowrite theelementsas  |101|]  and  |101001010|]  . Weusethename  quotationexpression  forthis newformofexpression. Wealsowanttobeabletodenecomputations overtheelements,soweneedaconstructionthat separatesthedierentformsabinarynumber cantakeandselectsthecomponentsofapar- ticularform.Themodernwaytodothisina functionallanguageistousepatternmatching. Wethereforeintroduceapatternmatchingform fortheelementsofatypedenedbyournew constructor.Apatternisasententialformof thelanguagedenedbytheconcretedatatype withordinaryML-patternsoftype  A  insteadof nonterminals  A  .Sinceourpatternsmaycontain MLpatterns,weusean  antiquotationsymbol  , `  ^  ',towriteMLvariablesandpatternsinthe objectlanguagephrases.Variablescanbewrit- tenjustfollowingtheantiquotationsymbolbut morecomplicatedpatternsmustbeenclosedin parentheses.Blanksafteravariableareignored. Examplesofpatternsfortheconcretedatatype ofbinarynumbersare  |101|]  ,  |^x|]  ,  |^x 101|]  and  |^(|10|])1|]  .Weusethename  quotationpattern  forthisnewformofpattern. Byusingthisconstructionitispossibletowrite afunctionthattakesabinarynumberasargu- mentandgivesitssuccessorasresult:  funsucc|0|]=|1|] |succ|1|]=|10|] |succ|^b0|]=|^b1|] |succ|^b1|]=|^(succb)0|]  Noticethatwehaveusedtheantiquotationsym- bolalsointhequotationexpressionsintheright handsidesofthefunctiondenition.Intheex- ample,thereisrstaquotationexpression  |^b 1|]  whichisintendedtoconstructaphrase fromthevalueboundtotheML-variable  b  and thesymbol  1  .Thevariablemust,ofcourse, beboundtoavalueoftype  BinNumber  since suchavalueisexpectedinthisposition.Sec- ondly,thereisthemorecomplicatedexpression  |^(succb)0|]  wheretheML-expression  succ b  isevaluatedtoavalueoftype  BinNumber  and thisnumberisthencomposedwiththesymbol  0  toproduceabinarynumber.AllML-expressions insideaquotationmustevaluatetocomplete phrasesofthelanguageandnottostringsof characters. Patternsinafunctiondenitionneednotdi- rectlycorrespondtothecasesinthedenition oftheconcretedatatype,ascanbeseenbythe followingexample:  fundiv4|^x00|]=true |div4y=false  Thepatternmatchingusingtheconcretesyn- taxisimportantinourapproachtorepresenting objectlanguages.Withoutit,onehastointro- ducesomewhatarbitrarynamesfortheopera- tionsthatdecideswhatformanelementhasand fortheoperationsthatselectsthecomponents ofacompoundelement.Compareourquotation bracketsandantiquotationsymbolwiththecor- respondingconstructionsintheEdinburghLCF systemGMW79]andalsowithQuine'squasi- quotationQui81]. Asasecondexampleconsiderimplementingthe denotationaldescriptionofaverysimpleimper- ativelanguage.Werstdenethelanguage  conctypePgm =|program<Cmds>end|] andCmds =|<Cmd>|] ||<Cmd>;<Cmds>|] andCmd =|if<Bexp>then<Cmds>else<Cmds>fi|] ||while<Bexp>do<Cmds>end|] ||<Var>:=<Exp>|] andExp =|<Var>|] ||<Integer>|] ||<Exp>+<Exp>|] ||<Exp>*<Exp>|] ||(<Exp>)|] andBexp =|<Exp>=<Exp>|] ||<Bexp>|<Bexp>|] ||<Bexp>&<Bexp>|] ||(<Bexp>)|]  whereweassumewealreadyhavedenedtwo concretedatatypes  Var  and  Integer  andafunc- tion  toint  thatmapsaconcreteintegertothe correspondingMLvalue.Usingtheconcrete 2   datatypedenedabove,wecandeneaninter- preterinanaturalway.Noticethatthedeni- tionisveryclosetohowGordondescribesthe denotationalsemanticsofalanguageinGor79]. Weassumewealreadyhaveimplementedan abstractdatatypeforstates,withoperations  sinit  ,  update  and  valof  .  funP|program^(cs)end|]=Cscssinit andCs|^c|]s=Ccs |Cs|^c;^cs|]s=Cscs(Ccs) andC |if^(b)then^(s1)else^(s2)fi|]s =ifBbsthenCss1selseCss2s |C|while^(b)do^(cs)end|]s= letfunfs=ifBbs thenf(Cscss) elses infs end |C|^x:=^e|]s=update(x,Ees,s) andE|^x|]s=valof(x,s) |E|^n|]s=tointn |E|^e1+^e2|]s=Ee1s+Ee2s |E|^e1*^e2|]s=Ee1s*Ee2s |E|(^e)|]s=Ees andB|^e1=^e2|]s=Ee1s=Ee2s |B|^b1|^b2|]s =Bb1sorelseBb2s |B|^b1&^b2|]s =Bb1sandalsoBb2s |B|(^b)|]s=Bbs  Thisexampleraisesaproblemofhowtodecide whatdierentpatternsmeans.Therstand secondcasesinthedenitionof  E   justconsistof ML-variablesandtheproblemishowtodecide thattherstisthevariablecaseandthesecond theintegercase.Weuseinformationfromthe typeinferencemechanismtochoosebetweenthe twopossibilities.Thepatternisnotparsedun- tilthetypecheckeralreadyhastypecheckedthe righthandsidesofthedenitionandthenwe knowthat  x  intherstcasemustbeoftype  Var  and  n  inthesecondmustbeoftype  Integer  . Fromthisinformationitispossibletodistin- guishwhichcaseapatternissupposedtode- note.Itisofcoursepossibletotrytodenea functionwhereonecannotdecidewhatcases twopatternsaresupposedtodenote.Takefor examplethedenitionofafunctionthatcounts thenumberofvariablesinanexpression:  funVars|^x|]=1 |Vars|^n|]=0 |Vars|^e1+^e2|]=Varse1+Varse2 |Vars|^e1*^e2|]=Varse1+Varse2 |Vars|(^e)|]=Varse  Inthisexampleitisimpossibletochoosebe- tweenthetwocasesifwedonotusethevariable nametoindicateitstype,aswedoindenota- tionaldescriptionsandFortran(!!).Oursolution istoallowtheusertoexplicitlytypethevari- ables.Sothersttwocasesinthedenition mustbewrittenas:  funVars|^(x:Var)|]=1 |Vars|^(n:Integer)|]=0 ...  Weconsiderittobeanerrorifwedonothave enoughinformationtoparseaquotationpattern unambiguously. Wehaveanotherproblemifwewanttodenea function  funisadd|^x+^y|]=true |isaddz=false  becausethetypecheckerandquotationparser cannotgiveauniquetypetothevariables  x  and  y  .Theycaneitherbeoftype  Var  ,  Integer  or  Exp  ,sothepatternisambiguousandthere- foreerroneous.Tomakeitunambiguousthe usermustprovidetypeinformation.Noticethat thetypeinformationdistinguishesthemorere- strictivepattern  |^(x:Var)+^(y:Var)|]  from  |^(x:Exp)+^(y:Exp)|]  . Problemswithambiguitiesinpatternsaredis- cussedinapaperDGKLM84]. Theconcretedatatypestnicelyintotheordi- narytypesysteminMLandwecanforexample denepolymorphicconcretedatatypessuchas treeswithinformationinthenodes.  conctype'ATree=|o|] ||{<'ATree>-<'A>-<'ATree>}|]  withelementslike  |{o-^("HEJA")-{o-^("BARACKEN")-o}}|] :StringTree  and  |{o-1010-o}|]:BinNumberTree  andafunctionthatswapstheleftandrightpart ofatree  funswaptree|o|]=|o|] |swaptree|{^x-^y-^z}|]=|{^z-^y-^x}|]  AscanbeseenfromtheStringTreeexample above,itispossibletouseordinaryMLtypes whendeningconcretetypes. 3   3LexicalAnalysis  Itisnotobviouswhatshouldbetreatedasalex- icaltokenintheembeddedlanguages.Inorder tobeexibleandallowasmanyandasdier- entconcretedatatypesaspossible,wehavede- cidedtovieweverycharacterasalexicaltoken. Theonlyexceptionstothisarethatasequence ofblanksistreatedasoneblankandthatthe escapecharacter`  n  'givesthefollowingcharac- teritsliteralmeaning.Theresultofthisisthat blanksarenothandlednicely.Ifwewanttohave blanksinaquotationexpressionthentheremust beablankcharacterinthecorrespondingposi- tioninthegrammar,andifablankispresentin thegrammartheremustbeatleastoneblank inthequotation. Havingamoresophisticatedlexicalanalyzer giveusanotherproblem.Wecannotuseparts ofalexicaltokeninthegrammar.Forexam- pleifweuseML:slexicalanalyzer,astheydoin theLeMLsystemINR85],wecannotdenethe binarynumbersaswedoinsection2sincease- quenceofzerosandonesistreatedasaninteger inML. Thebestsolutionwouldprobablybetogivethe userthepossibilitytodeneherownlexicalan- alyzer.  4ParsingandTypeDeriva- tion  Inthissectionwedescribehowthenewcon- structionsaretranslatedduringthecompilation toordinarydatatypesandconstructors. Afterthecompilationnothingofthenewcon- structionsremainsandtheyhavethereforeno eectontheexecutionspeedofthenewsyn- tacticalconstructions.Aprogramwithconcrete datatypes,quotationsandanti-quotationsruns atthesamespeedasonewithoutthem. Letusgiveanoverviewofthetranslationpro- cess.Aconcretedatatypeistranslatedintothe followingobjects.    Adatatypedenition,whichcouldbeseen asthetypeofparsetreesforthelanguage denedbythegrammarintheconcrete datatype.    Aparserthatrecognizesthelanguagede- scribedbythegrammarandtranslatesa phraseofthelanguageintotheparsetree.    A(pretty?)printerthatprintselements oftheconcretedatatypeusingtheconcrete syntax. Thetypedenitionofbinarynumbers,  conctypeBinNumber =|0|] ||1|] ||<BinNumber>0|] ||<BinNumber>1|]  willbetranslatedintothefollowingdatatype denition.  datatypeBinNumber =BinNumber1 |BinNumber2 |BinNumber3ofBinNumber |BinNumber4ofBinNumber  andaparserthat,forexample,translates  |101|]  to  BinNumber4(BinNumber3(BinNumber2))  Theparserisusedinthecompilertotranslate quotationpatternsandquotationexpressionsto ordinarypatternsandexpressions.Forexample, thefunction  funsucc|0|]=|1|] |succ|1|]=|10|] |succ|^b0|]=|^b1|] |succ|^b1|]=|^(succb)0|]  istranslatedto  funsucc(BinNumber1) =BinNumber2 |succ(BinNumber2) =BinNumber3BinNumber2 |succ(BinNumber3b) =BinNumber4b |succ(BinNumber4b) =BinNumber3(succb)  UsuallythesyntaxofanMLprogramischecked intwodistinctsteps.Firstitisparsedwitha contextfreeparserandthentypecheckedwitha typecheckerutilizingMilner'salgorithmMil78]. Thissimplesequenceisnolongerpossiblewhen concretedatatypesareaddedtoMLsincethe parsingofaconcreteelementdependsofitstype. Thatis,ifaconcreteexpressionisinacontext whereanelementoftype  A  isexpecteditshould beparsedwith  A  asthestartsymbol.Cor- respondingly,thetypeofanMLexpressionin aquotationisdependentontheparsingofthe quotation.Toachievethis,wehavetointegrate 4   theparsingoftheconcreteelementswithMil- ner'stypederivationalgorithm.Wehavebuilt theparseraroundageneralizedversionofEar- ley'salgorithmEar70].Itisgeneralizedfortwo reasons:    Concretedatatypesseenasgrammarsare morepowerfulthancontextfreegrammars forwhichEarley'salgorithmisconstructed. Thisstemsfromthefactthatwecanhave polymorphicconcretedatatypes.Asimple exampleofalanguagethatcanbedened byapolymorphicdatatypebutnotwith acontextfreegrammararethetreesintro- ducedinsection2.    AparserdenedwithEarley'salgorithm usuallytakesasequenceoflexicaltokens asinputandgivesaparsetreeasoutput. However,theparserthatwewantshould takeasequenceoflexicaltokens  andun- quotedMLobjects  asinputandgiveanML expressionasoutput. Thealgorithmwehavedevelopeddiersfrom Earley'sinthatwecanhavetypevariablesin thenonterminalsandthesecanbeinstantiated duringparsing.Forexample,giventheconctype  conctype'AList =|$|] ||<'A><'AList>|] and conctypeD =|0|] ||1|]  andtheinput  |0$|]  ,  'A  willbeinstantiatedto  D  .Tosupportthis,eachiteminEarley'salgo- rithmcontains,apartfromthedottedproduc- tionandtheitemsetpointer,atypesubstitu- tion.Thesubstitutionsarehandledinthefol- lowingwaybytheparsingoperations:    InthepredictoperationinEarley'salgo- rithmanitemisaddedonlyonceeven thoughitmightbepredictedfrommore thanoneitem.Inourversioneachnewitem iscreatedwithaninitialsubstitution.The moreinformationweletthissubstitution inheritfromthepredictingitemthelessis thechancethatwecanshareit.Toassure maximalsharingweleteachitemstartwith theemptysubstitution.Whenthedotisto theleftofanuninstantiatedtypevariable allconctypesknowninthecontextarepre- dicted.    Inthecompletionofanitem  I  ,wereturn totheitemsetpointedtoandaddupdated versionsofallitems  I  0  whichhaveatype  T  0  totherightofthedotthatcanbeunied withthetype  T  wehavejustcompleted. Sincetherecanbemorethanoneitemwith thispropertywehavetomakesurethatwe usefreshvariablesforthetypevariablesin  T  beforeunication.Weupdate  I  0  bymov- ingthedotonesteptotherightandcom- posethesubstitutionwiththesubstitution in  I  . Letusillustratethiswithanexample:Corre- spondingtotheinput  |$$|]  andtheconctype  conctype'AList=|$|] ||<'A><'AList>|]  wegettheitemsets:  I  0  <  S  >  ::=    <  0  A  List  >  ,  s  0  ,0(1)  <  0  A  List  >  ::=    $,],0  <  0  A  List  >  ::=    <  0  A><  0  A  List  >  ,],0  I  1  <  0  A  List  >  ::=$    ,],0(2)  <  S  >  ::=  <  0  A  List  >    ,  s  0    0  A  7!  0  X  1  ],0(3)  <  0  A  List  >  ::=  <  0  A>    <  0  A  List  >  ,   0  A  7!  0  X  2  List],0  <  0  A  List  >  ::=    $,],1  <  0  A  List  >  ::=    <  0  A><  0  A  List  >  ,],1  I  3  <  0  A  List  >  ::=$    ,],1  <  0  A  List  >  ::=  <  0  A><  0  A  List  >    ,   0  A  7!  0  X  2  List,  0  X  3  7!  0  X  2  List],0  <  0  A  List  >  ::=  <  0  A>    <  0  A  List  >  ,   0  A  7!  0  X  4  List],1  <  S  >  ::=  <  0  A  List  >    s  0    0  A  7!  0  X  5  ,  0  X  5  7!  0  X  2  List,  0  X  3  7!  0  X  2  List],0  <  0  A  List  >  ::=  <  0  A>    <  0  A  List  >  ,   0  A  7!  0  X  6  List,  0  X  6  7!  0  X  2  List,  0  X  3  7!  0  X  2  List],0  <  0  A  List  >  ::=    $,],2  <  0  A  List  >  ::=    <  0  A><  0  A  List  >  ,],2  5 
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks
SAVE OUR EARTH

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!

x