Functional Programming COSC 3015
Popular in Course
Popular in ComputerScienence
This 29 page Class Notes was uploaded by Ashlynn Rau on Tuesday October 27, 2015. The Class Notes belongs to COSC 3015 at University of Wyoming taught by Staff in Fall. Since its upload, it has received 15 views. For similar materials see /class/230333/cosc-3015-university-of-wyoming in ComputerScienence at University of Wyoming.
Reviews for Functional Programming
Report this Material
What is Karma?
Karma is the currency of StudySoup.
Date Created: 10/27/15
Lecture 23 Lectured by Prof Caldwell and scribed by Sunil Kothari November 137 2008 1 Review We looked at uni cation7 substitutions and various substitution operators Remember two types are um39 able if there exists a substitution 0 such that atl atgi The terms are de ned as data Term V string I Abs String Term I Ap Term Term The types are de ned as Type TyVar String I Arrow Type Type The goal is a function infer Term A Type where infer it returns the Type of term t if there is one 2 Type Inference We can make it a MayBe type to handle cases when a term has no type data MayBe A Just A I Nothing We have a little proof system for the type inference But rst lets introduce the various concepts A sequent a state in the proof for the type inference F h z z t where7 1 F is called a context and is a list of string gtlt type pairs the context is what we know so far 2 E is a constraint set and is a list of type type ype i 3 t is a termi 4 a is a type The constraints get synthesized from the proof by propagating back down whereas we construct the proof tree bottom up The rule for a type variable is ma W where x T E F Var Here s an example of Axiom rule Sox0 gt0 aH0zTbzTl FxUx0 b Mz m where 0 and B are fresh Abs The notation means Fz Remove pairs from T where z is the rst element The rule for application is FE1FM0 gtT REngza F E1UE2F MN2739 So we can now do a proof where 0 is fresh App ltvargt Iialy8al IZ8 H afagtabzlzzf Abs Suppose we wanted to nd the type of the term yr lyz l TB70Ha gtTbzlzzogta lyi lvfa byza lyz l 7 70Ha gtTo bxlryia The constraint set generated by collecting the constraints from the above proof Abs Var App 0 A a 5 A 739 0 B The uni cation algorithm gives the substitution a 0 739 5 This substitution when applied to the type we assumed earlier 239e 0 gives 5 which is what we expected Now we can type this all in Haskell First we start with the axiom rule We have a function infer which takes as argument a context a term a type and list of fresh variables generated so far Again the function is de ned by case analysis on the term infertype context trm typ vars case trm of V x gt case lookup x context of Just t1 gt typt1xvars Nothing gt error quotinfer quot x quotnot in contextquot App m n gt Abs x m gt 1 Recall that lookup has the following type Typeinferencegt t lookup lookup Eq a gt a gt a b gt Maybe b We can test our code now even though the code for application and abstraction returns just an empty list Typeinferencegt infertype quotXquotArrow TyVar quot21quot TyVar quotaquot V quotxquot TyVar quot21quot aa gt a l Typeinferencegt infertype quotXquotArrow TyVar quot21quot TyVar quotaquot V quotxquot TyVar quotbquot ba gt a l We can now ll up the code for abstraction and application as follows Ap t1 t2 gt let a fresh quotaquot varsof context vars fv typ in let e1vars1 infertype context t1 Arrow TyVar a typ a2vars in let e2vars2 infertype context t2 TyVar a varsl vars in el e2 varsl vars2 Abs x t1 gt let varsl varsof context vars fv typ in let a fresh quotaquot varsl in let b fresh quotbquot avars1 in let vars2 abvars1 in let e1vars infertype x TyVar acontext t1 TyVar b vars2 in typ Arrow TyVar a TyVar be1 vars vars2 We will create a helper function infer to pass the arguments which remains more or less the same each time infer context trm let e infertype context trm fresh quotaquot fvars context 1 in subst unify e trm where fvars fvars xtxts fv t fvars xts NOW we can test our code Typeinferencegt t infer infer String Type gt Term gt Char TYPSH 21 infer quotyquot TyVar quotbquot Ap Abs quot2quot V quotxquot V quotyquot aaaa Typeinferencegt infertype quotyquot TyVar quotbquot Ap Abs quot2quot V quotxquot V quotyquot TyVar quot21quot baaaaaa gt aaaaa gt baab quotaaaaquotquotbquotquotaaquotquotyquotquotaaquotquotaquot Typeinferencegt let e infertype quotyquot TyVar quotbquot Ap Abs quot2quot V quotxquot V quotyquot TyVar quot21quot J in unify e a aaaaaa aaaab 2121an Typeinferencegt let e infertype quotyquot TyVar quotbquot TyVar quot21quot l in unify head 6 b aaaa Typeinferencegt let e infertype quotyquot TyVar quotbquot Ap Abs quot2quot V quotxquot V quotyquot TyVar quot21quot l in map2 subst unify head e tail e b aaaa Typeinferencegt infertype quotyquot TyVar quotbquot Ap Abs quot2quot V quotxquot V quotyquot TyVar quot21quot byaaaaaa gt aaaaa gt baabIlaaaallIlbllIlaallllyllllaallll u Ap Abs quot2quot v w v quotyquot Lecture 26 Lectured by Prof Caldwell and scribed by Sunil Kothari November 257 2008 1 Review We will start from the beginning The goal is to apply parsers to a string and that will generate tree in the en i The book de nes parsers as functions from String A Tree Then it is generalized to String A Tree7 Stringi Then the author says that since a string can parsed in multiple ways so let s account for those The resultant type of parsers is String A tree7 Stringi The one nice feature is that empty list will indicate failure Finally7 the type of parser is Parser a String A oz7 Stringi We hope to use sequencing operations from the Monadi These are 3 different ways of de ning a data type This is something newi newType Parser a MkPString A a7 String The only difference here is that there is another version type String Char Note that String is a synonym of Charli What happens in the data declaration data Parser a MkPString A a7 String Typically data is used for inductive data types so that you can do case and pattern matching typePaTsera String A a String Putting a constructor MkP here tells the system to recognize the type as a Parser Its more or less an ef ciency thing Note that there s no recursion in newType thing The newtype thing is not really there in the compiler Anyways we are adopting the newtype thing for Parser newtype Parser a MkP String gt aString apply is given as apply Parser a gt String gt aString apply MkP f i f i mphParser is given as applyParser Parser a gt String gt a applyParser p fstheadapply p Remember that gtgt the type of bind operator is Hugsgt t gtgt gtgt Monad a gt a b gt b gt a c gt a c Hugsgt Now we can de ne an instance of Monad for Parser as given in Birdls book instance Monad Parser gtgt Parser a gt a gt Parser b gt Parser b p gtgt q MkP f where f s ys xs lt apply p s ys lt apply q x s return a gt Parser a return v MkP i gt vi Note that list comprehension is like do notation for lists Interestingly Huttonls book de nes the bind operator as follows instance Monad where Hutton s thing p gtgt f MkP i gt case apply p i of l gt vout gt apply f v out out is the remaining part of the input string Next7 we look at item7 which parses a string Character by Character item22 Parser Char item MkP1 gt case i of J gt x2xs gt xxs Here s an example of a parser which reads rst two Characters and returns the remainder of the string Parsergt apply do x ltitem y lt item return yx quotxyzzyquot y x quotzzyquot 2 CharCharString Parsergt apply do x ltitem y lt item return yx quotxquot J 2 CharCharString Parsergt apply do x ltitem y lt item return yx quotxyzzzyquot y x quotzzzyquot 2 CharCharString Parsergt zero is a parser that always fails 7 returns an empty listl zero 2 Parser a zero MkPi gt 1 Parsergt apply zero quotxyzzyquot 2 aString Next7 we de ne a parser which reads the rst three Characters of a string and returns a pair of the rst and the third Character7 and also returns the remaining stringl p 2 Parser CharChar p do x lt item item y lt item return xy Parsergt apply p quotxyzzyquot x z quotzyquot 2 2 CharChar String This business of instantiating monads and guring out is a fascinating work of functional programming people The downside is that it is complicated But it gets easy when you use it As of now7 we have simple parsersi Now we make a parser which uses a predicate sat22Char gt Bool gt Parser Char sat p do x lt item if p x then return x else zero Here s some examples Parsergt apply sat x quotwxyzzyquot 2 2 CharString Parsergt apply sat x quotxyzzyquot x quotyzzyquot 2 2 CharString This is interesting 7 the type contains a function flip7 which is normally not the case 2t x flip x 2 Char gt Bool We can do more Parsergt apply sat gt c elem quotxyzzyquot quotwxyzzyquot 2 CharString Parsergt apply sat gt c elem quotxyzzyquot quotxyzzyquot x quotyzzyquot 2 CharString Parsergt apply sat gt c elem quotxyquot quotxyzzyquot x quotyzzyquot 2 CharString Then we have a parser which parses only digits and another which parses returns the character corresponding a particular digiti digit 2 Parser Char digit sat isDigit digit 2 Parser Int digit do d lt digit return ord d 0rd 0 Parsergt apply digit quot1234quot 1 quot234quot 2 CharString Parsergt apply digit quotabcdquot 2 CharString Parsergt apply digit quotabcdquot IntString Parsergt apply digit quot1234quot 1quot234quot IntString Parsergt More sophisticated parsers can now be de ned lower Parser Char lower sat isLower Parsergt apply lowers quotsUpperquot quotsquotquotUpperquot CharString Parsergt apply lowers quotssUpperquot quotssquotquotUpperquot Char String upper Parser Char upper sat isUpper char Char gt Parser Char Char K sat x sat i is a parser Which matches the rst character With L string 1 return 1 string xxs do Char K string xs return xxs If it s an actual string eat a character X and then recursively call string on xs Parsergt apply string quotxyquot quotxyzzyquot quotxyquotquot39zzyquot Char String Parsergt apply string quotwxyquot quotxyzzyquot CharString Parsergt The two parsers can also be combined using the choice operatori p plus q Mkp f where fx apply p s apply q s Hutton7s choice operator p q MkP i gt case apply p i of gt apply q i m gt m Hutton has simpli ed it so as to have deterministic parsersi Parsergt apply char x char y quotxyzzyquot x quotyzzyquot CharString Parsergt apply char x char y quotyxzzyquot y quotxzzyquot CharString Parsergt apply char x plus char y quotyxzzyquot y quotxzzyquot CharString Also7 consider lowers lowers Parser String lowers do c lt lower cs lt lowers return c cs return quotquot Here s some examples Parsergt apply lowers quotxyzzyquot quotxyzzyquotquotquot Char String Parsergt apply lowers quotxyzzyABCDquot quotxyzzyquotquotABCDquot Char String Parsergt apply lowers quotnyzzyABCDquot quotxquotquotXyzzyABCDquot CharString Let7s look futher downi Read is a type class Parsergt t read read Read a gt String gt a Parsergt read quot123quot Int 123 Int digit is de ned as digit Parser Char digit sat isDigit The nut is a parser that reads one or many digitsi nat Parser Int nat do xs lt many1 digit return read xs Parsergt apply nat quot123quot 123quotquot IntString Parsergt apply nat quot123abcquot 123quotabcquot IntString manyis a parser to read zero or more times t many lower many lower Parser Char A standard thing is to tokenize 239e eat as many space as possible space Parser space do many char return Here s an example Parsergt apply space quot xyzzyquot quotxyzzyquot String The following parser parses a list of natural numbers including any spaces natural Parser Int natural token nat symbol String gt Parser String symbol xs token string xs natlist Parser Int natlist do symbol quotquot n lt natural ns lt many do symbol quotquot natural symbol quot1quot return nns Parsergt apply natlist quot1 23 5 quot 1235 quotquot Int String Parsergt apply natlist quot lquot Int String Parsergt apply natlist quot1 23 5 zbcd quot 1235 quotzbcd quot1 Int String Parsergt Lecture 21 Lectured by Prof Caldwell and scribed by Sunil Kothari November 67 2008 1 Review We have a programming language which has constructors and destructors for functions and pairsi But we donlt have numbers and arithmetic expressions in our language but that is easy encode numbers as lambda terms We donlt need pairs even but it is convenient to have pairs The next goal is to have types and type inference for this language The next goal is to have a type inference algorithm for this language What are the types that we need to have 7 The constructs in the language are A12 1 l MN l AITM llt M7N gtl spreadMzyiN z Variables Type variables M N Application AITM Abstraction Arrow lt MN gt Pairs Product For the constructors we can say what the type is gonna be but for destructors we cannot say so So we have two languages one involving terms and the other involving typesi So let s do it in Haskell module Ttypes where data Types TyVar String I Arrow Types Types I Prod Types Types deriving Eq Show The type language is less complicated there is no binding here So7 lets de ne f1 fv TyVar x x v Arrow t1 t2 fv t1 fv 132 v Prod t1 t2 fv t1 fv t2 HaHa So where are we headed 7 We will look at type checking and follow it up with type inference What does the typing rules look like 7 There7s gonna be a notion of what type means under a context T We write T b I t where7 F is list of variable X type pairs M is a term an t is a type So how do we show ALM has type T so it must be the type T1 A T2 Typing rules specify this how aspect FxUxn F Mzro F b AxM 71 TO Abs The rule for application is 7391 a T F N 7391 W App The rule for a type variable is W where x T E F Axlom So how does this defers from type inference 7 What we are now doing is called type checking Here7s an example Aim A yZbe 3be pp X10111 App ybbzzyb ybbyb There is a little bit of manipulation going on Type inference takes care of that We need a couple of ideas substitutions which maps variables to types and we also need uni cation algorithm to solve the equations generated by these types 11 Substitutions Substitution are functions from substitutions to types If a is a substitution then a TyVar z 01 0 Arrow t1 t2 Arrow 0 t1 0 t2 0 Prod t1 t2 Prod 0 t1 0 t2 Given two types T1 and T2 we say a substitution uni es T1 and T2 iff 0T1 0T2i For example7 consider a A b and type c then 0 c I a A b is a uni er since 0a A b 0a A 01 agtb and 0cagtbi So 0 uni es agtb and cl Also0bbgtbcagtbalmthen0agtbagtbgtband 00 a babi So 0 is also auni eri De nition 1 Most general uni er A substitution 0 is a most general uni er of T1 and T2 for every 0 that uni es T1 and T2 there exists a substitution 0 such that 0 0 o 0 Example of types that are not uni able a and a A a Suppose there was a substitution that could unify these types7 then it would be aagtai But7 then 0a aaaand 0agtaagtagtagta So7 there is no substitution that uni es these two We will use these ideas and change the rules a little bit later generate con straints while deriving a derivation for a given type For examp e7 lf0 12 yy I 2 then 01 yr But consider 01 z I y and 02 I y I 2 then 02011 02y 2 But 01 y i One active area in programming languages is trying to reason about bindingsi We can now code what we discussed in Haskell as data Subst S String Types deriving EqShow apply Subst gt Types gt Types apply S 1 t 1 apply S xtxts TyVar y if x y then 1 else apply S xts TyVar y apply 5 Arrow t1 t2 Arrow apply 5 t1 apply 5 t2 apply 5 Prod t1 t2 Prod apply 5 t1 apply 5 t2 We can start the code for uni cation as unify TyVar x TyVar y if x y then S 1 else S xTyVar y unify TyVar x t S xt unify t TyVar x unify TyVar x t unify Arrow t1 t2 Arrow t3 t4 unify Prod t1 t2 Prod t3 t4 unify Arrow Prod error quotunifyquot unify Prod Arrow error quotunifyquot Notice we didn t do a check This is not complete yet but we Will continue next time Lecture 27 Lectured and scribed by Suml Kothari December 12 2008 1 Overview Our goal today is to have parsers which transform types in one language to another language Speci cally we want 77a A b A 577 to be converted into 77 Arrow TyVar a Arrow TyVar b TyVar a We plan to do the following 1 We will start with a simple type language which requires parens for unique parse treesi E0 We will look at an ef cient version of the above parseri 9 Next we look at how to parse without parensi 9 Finally we make the parens optional in our language 2 Review Recall that parser type is de ned as newType Parser a MkPString A a String In the previous lecture we looked at the different ways of de ning a type Look at the notes or in the book if you want more information For all the parsers that we de ne in this lecture most of them can be made from only two operatorsi return is de ned as return a gt Parser a return v MkP i gt vi Parser1gt apply return 1 quotabcquot 1quotabcquot IntegerString The other operator is gtgt called 77then77 in Hutton7s booki p gtgt f MkP i gt case apply p i of J gt vout gt apply f v out In general parsers are built in the following fashion pl gtgt Avl A 172 gtgt A UZ A pn gtgt Avn A return 111112 l 1m This notation is normally not used lnstead Haskell provides the do notation do v1 lt7 pl 1 lt7 p2 39pm return f 111112 1m Letls brie y reView some of the parsers that Prof Caldwell introduced last time item which parses a string character by character item Parser Char item MkP1 gt case i of J gt x2xs gt xxs Next we de ne a parser which reads the rst three characters of a string and returns a pair of the rst and the third character and also returns the remaining stringi p Parser CharChar p do x lt item item y lt item return xy Parsergt apply p quotxyzzyquot x z quotzyquot CharChar String The two parsers can also be combined using the choice operatori p plus q Mkp f where f x apply p s apply q s Huttonls choice operator p q MkP i gt case apply p i of J gt apply q i m gt m A standard thing is to tokenize 239e eat as many space as possible space Parser space do many char return token Parser a gt Parser a token p do space v lt p space return v 3 Parsing types This is What was covered in last lecture Today we Will build on that and convert types in one language to another language In compilers we often do that We Write programs in one language normally called the source language and convert it into another language often called the target language For example transforming C Programs to Java programs Each of these languages has a grammar Which dictates What terms programs are syntactically valid in a given language In our case the source grammar is given as type string 77 77 typewi gt 77 type 7777 77 77 77 X 77 7777 We need parenthesis in this language since some strings can be parsed into more than one parse trees For example the string 77a A b A c 77 can be parsed as agtbgtcorasagtbgtc The target language is given as type TyVar string l Arrow type type l Prod type type Letls Write a parser now typ Parser Type typ tyvar arrow prod The typ parser is a 77choice77 in the sense that we can either have a type variable or an arrow type or a product type The tyvar7 arrow7 and prod parsers are de ne tyvar Parser Type tyvar do n lt identifier return TyVar n arrowParser Type arrow do symbol quotquot a lt typ symbol quotquot symbol quotgtquot b lt typ symbol quotquot return Arrow a b prod Parser Type prod do symbol quotquot a lt ty symbol quotxquot b lt typ symbol quotquot return Prod a b We can load this and check typ quota gt b gt cquot Parser1gt apply quotbquot TyVar quotCquot TypeString Arrow TyVar quotaquot Arrow TyVar Parser1gt apply typ quota gt b gt c l TypeString Parser1gt apply typ quota gt b gt cquot l TypeString Parser1gt apply typ quota gt b gt cquot Arrow TyVar quotaquot TyVar quotbquotquotgt cquot TypeString Note that we the parser takes care of extra spaces as shown below Parser1gt apply typ quot a gt b gt c quot Arrow Arrow TyVar quotaquot TyVar quotbquot TyVar quotcquot 1 TypeString Parser1gt The parser so created is not an ef cient parseri The inef ciency comes from the following code typ Parser Type typ tyvar arrow prod To have an ef cient parser we change the code slightly The new parser is typ Parser Type typ tyvar comptype comptype Parser Type comptype do symbol quotquot a lt typ constructor lt op c lt typ symbol quotquot return constructor a c op Parser Type gt Type gt Type op arrow prod arrow Parser Type gt Type gt Type arrow do symbol quotgtquot return Arrow prodParser Type gt Type gt Type prod do symbol quotxquot return Prod This doesnlt change the nal output For example Parser2gt apply typ quota gt b gt cquot Arrow Arrow TyVar quotaquot TyVar quotbquot TyVar quotcquot TypeString Parser2gt Now we switch to a type language where the compound types always asso ciate to the right So we can do away with the parens in our source language The new grammar is given as type 2 string type 7 A 7 type l type 77 X 77 type The parser undergoes a slight modi cation typ Parser Type typ comptype comptype Parser Type comptype do a lt tyvar do constructor lt op c lt comptype return constructor a c return a op Parser Type gt Type gt Type op arrow prod We can load this in the interpreter and the results are as expected Parser3gt apply typ quota gt b gt cquot Arrow TyVar quota Arrow TyVar quotbquot TyVar quotcquot 1 TypeString Parser3gt apply typ quota gt b gt cgt d equot Arrow TyVar quotaquot Arrow TyVar quotbquot Arrow TyVar quotcquot Arrow TyVar quotdquot TyVar quotequot Parser3gt apply typ quota gt b x cquot Arrow TyVar quotaquot Prod TyVar quotbquot TyVar quotcquot Parser3gt gt II Type String Finally7 we make the parenthesis optional in the sense that if they are not speci ed then the compound types will associate to the right Again7 the mod i ed code is given below typ Parser Type typ comptype parencomptype parencomptype Parser Type parencomptype do symbol quotquot a lt ty symbol quotquot return a comptype Parser Type comptype do a lt tyvar parencomptype do constructor lt op c lt typ return constructor a c return a Again7 the results are as we expect Parser4gt apply typ quota gt b gt c gt d gt equot Arrow TyVar quotaquot Arrow Arrow TyVar quotbquot TyVar quotcquot Arrow TyVar quotdquot TyVar quotequot Parser4gt apply typ quota gt b gt c gt d gt equot Arrow TyVar quotaquot Arrow Arrow TyVar quotbquot Arrow TyVar quotcquot TyVar quotdquot TyVar quote Parser4gt COSC 3015 Lecture 16 Lectured and scribed by Sunil Kothari 21 October 2008 1 Review We looked at a couple of trees and their corresponding datatypes For instance the binary trees are given as data Btree a Leaf a I Fork Btree a Btree a and the binary search trees are given as data 0rd a gt Stree a Null I Fork Stree a a Stree a The induction principle for the Stree is PNull VI aVt1 t2 Stree a Pt1 Pt2 PFOTk t1 1 t2 Vt Stree a PO Note that we havenlt taken into account the constraint on the types But if we do consider the constraint the induction principle is V a Type Ord a IPNull VI aVt1t2 Stree a Pt1 Pt2 PFOTk t1 1 t2 Vt Stree a PO Today we will look at two different types of trees 0 Binary heap tree 0 Rose tree 11 Binary Heap Tree The binary search tree is given by data 0rd a gt Htree a Null I Fork a Htree a Htree a This looks familiar In fact it is very similar to the way a Stree is de ned The only difference is the position of the label in the Stree ln Htree the label on a nonnull node is given before the two subtrees The book says that the Htree has to satisfy the condition that the label on a given node cannot be greater than label on any subtree of the node Actually7 depending upon the order there are two kinds of binary heap trees min and max In the min binary heap trees7 the root node has the smallest labeli In this lecture7 we consider only min binary heap treesi When we try to atten a heap tree7 the order becomes important flatten0rd a gt Htree a gt a flatten Null flatten Fork x yt zt xmerge flatten yt flatten zt and the function merge is de ned as merge 0rd a gt a gt a gt a merge ys ys merge xs 1 xs merge xxs yys if x lt y then x merge xs y2ys else y merge xxs ys The thing to note is that merge will return a list that has labels in some order ascending order for min heap treesi Maingt merge a c b d quotabbccdquot Maingt There are two ways of creating a heap tree 1 Insert one node at a time and then pushup the inserted element so that the tree satis es the heap property slightly more than lineari In fact n log n7 where n is the size of the tree 2 Make a minimum height tree and then impose heap property Linear in the size of the tree The book de nes a function mkHeap which does the latter as mkIIeap heapify mkIItree Both heapify and mkHtree are linear in the size of the tree If Now we can come back to our question of the difference between a Stree and a Htreei Htree will satisfy the following predicate heapOrdered 0rd a gt Htree a gt Bool heapOrdered ordered flatten 12 Rose Trees With Rose trees described by Lambert Meertens we can represent trees of ar bitrary arity They are also known as General trees and we will see why its so In Haskell the trees are de ned as data Rosa a Node a Rose a Note that compared to other trees we have only one data constructor but still we can represent any kary tree as a Rose tree This is in contrast with the binary search tree and heap trees which are 2ary trees The induction principle for Rose trees is Vzts Rose alet E ItsPzt PNode 1 Its Vzt Rose aPzt Letls look at some examples 1 Node 0 is a single tree with no sub trees 2 Node 0 Nodel is a tree with one child In general we can de ne a rose with in nite children as NodeO Noden ln lt7 Finally note that any rose tree can expressed as a binary tree and any binary tree can be expressed as a rose tree The former is harder than the latter Lecture 19 Lectured by Prof Caldwell and scribed by Sunil Kothari October 307 2008 1 Review Use of the variables in the let con struct Q What is the use of variables seems like extra computation A consider the following example let I 2 x y 3 x y 4 x y in z z y The evaluation of a let construct is given as eval m Let 1 e1 e2 eval m e2 where m 2 ifz I then eval m e1 else m 2 Recall the datatype for the expression language data Exp N Int I V String I Add Exp Exp I Let String Exp Exp Suppose m 2 1007 then what is eval m Let 77x77 N 1 Add V 77x V 77x 7 ml m Let N 1 Add V 71 V w M eval m AddV z V z 77 77 wherem z N1 721 100 M eval m V 77177 eval m V 77y M 777 77177 m 77y77 M 1 100 M 101 Suppose we have a function f z a A 12 We can make a function which be haves like f but differs on one of the inputs The function update does this job update I a A b A a7b A a A 12 update f 17y w A ifw I then y else f 1 S07 if f z z then7 g update f 01 is a function that behaves just like the identity function except that on input 0 it returns 1 Lets do a computation With g 0 updatef010 Aw A ifw 0 then 1 else f w0 if0 0 then 1 else f 0 if true then 1else f 0 1 M M M M evalm AddV77 z Let77 1 N2 V77 I M1002 vl02 This is same as VI Int1Pz Where I in 131 is a binding of I which is quanti ed at the start of the expression 2 Capture avoiding substitutions Consider the lambda terrns given by the following datatype data Lam V String I Ap Lam Lam I Fun String Lam deriving Eq Show ApFun77I77 V77I77V77y77 M y How does this evaluation happens 7 I77 V77 177 77177 V77 y77 Where e1z I y replace all I by y in 61 M waw Maingt t subst subst Char Lam gt Lam gt Lam Maingt subst quotxquot V quotyquot V quotxquot V quotyquot Maingt subst quotxquot V quotyquot V quot2quot V quotZn Maingt subst quotxquot V quotwquot Fun quot2quot Ap V quot2quot V quotxquot Fun quot2quot Ap V quot2quot V quotwquot Maingt The following functions are equal A1 A z Ay A y Azazyzgtzy But A1 A z y not equal to Ay A y 2 nor Ay A y Maingt subst quotxquot V quotwquot Fun quotxquot V quotxquot Fun quotxquot V quotwquot Look what happened lll A1 A I w M A1 A w In the body of the lambda z is getting replaced by w even though I is bound In capture avoiding substitutions we want to substitute only free varaiblesi Here s an example A1 A z I z 2 M Am A z z 2 As mentioned earlier A1 A z Ay A y In general A1 A m A2 A mz I 2 and 2 E FVm So Azazy 7 Azazy Aw A w y So we will de ne this notion of free variables fV of a terrni fv V S Isl fvApmn fvmfvn f1 Fun 8 m filter 8 f1 m Once we have this we can use this to avoid capturing bound variables in the subst function and is de ned as subst xn V s if x s then 11 else V s xn Ap m k Ap subst xn m subst xn k subst xn Fun y m if x m c 0quot m d then Fun y m else if y elem iv 11 then Fun 2 subst xn subst y V z m else Fun y subst xn m where z fresh quot2quot vars where vars xyfv m fv n what we need is a total And a show function for the larnbda terms as instance Show Lam where show V x x show Ap m n show Fun x m quot x quot gtquot show m quotquot show In quotquot show n quotquot Another helper function is testsubst Which pretty prints the substitution testjubst xn t Now we can test our substitution function Maingt testsubst quotxquot V quotwquot Fun quot2quot quotzgtzx gt zgtz wquot Maingt testsubst quotxquot V quotwquot Fun quotwquot quotwgtw x gt zgtz wquot Maingt testsubst quotxquot V quotwquot Fun quotwquot quotwgtw Z gt zzgtzz 2quot Maingt show 1 quot gt quot show subst xn t Ap V quot2quot V quotxquot Ap V quotwquot V quotxquot Ap V quotwquot V quotzquot