Assignment 5 All Things Grow with Love

Assignment 5  Programming Languages and Paradigms

Q1.  [50 points] We revisit here our simple language for arithmetic expressions and booleans. Here we extend the language with pairs of expressions Backus-Naur Form (BNF): Operations op ::= + | − | ∗ |<|= Expressions e ::= n | e1 op e2 | true | false | if e then e1 else e2 | x | let x = e1 in e2 end
Values v ::= true | false | n Types t ::= bool | int
Values in our language are booleans, integers. This language is the language that we saw in class. To grow our language we want to add the idea of pairs. We want to add an expression to build pairs (e1,e2) and an expression to pattern match on them: let pair (x,y) = e1 in e2 end. Pairs of values are values, and their type is a called a product type of the types of each component. We extend the grammar by adding the following expressions, values, and types: Expressions e ::= ··· | (e1,e2) | let pair (x,y) = e1 in e2 end Values v ::= ··· | (v1,v2) Types t ::= t1 ×t2
1
Some examples of these new operations are: (1,true) : is a value of type int×bool let z = (3,2) in let pair (x,y) = z in x + y end end : is well-typed with type int and it evaluates to 5. let pair (x,y) = (false,7) in if x then 1 else y end : is well-typed with type int and it evaluates to 7. let pair (x,y) = 14 in if x then 1 else y end : is not well-typed because pattern matching lets require a pair to eliminate. Note that the last expression is syntactically allowed, but it is not well-typed. Pattern matching let expressions expect an expression of product type. Q1.1 (5 points) Extend on paper the definition for FV(e) which computes the free variables of the new expressions. Q1.2 (5 points) In the template file hw5.ml using the extended expression data-type, extend the definition of free variables from Q1.1 Q1.3 (5 points) Extend on paper the definition of substitution [e/x]e0 where we replace any free occurrence of the variable x in the expression e0 with the expression e. Q1.4 (7 points) Extend the definition of subst function as you did on paper in Q1.3 Q1.5 (5 points) Extend on paper the definition of well typed expressions to contemplate pattern matching lets. Q1.6 (9 points) Extend the definition of function infer so it is able to infer the types of pairs and their pattern matching using. We will use the typing judgment Γ ` e : T which states that expression e has type T in the context Γ where Γ is defined as follows: Typing Context Γ ::= · | Γ,x : int Recall that Γ records the type of variables. The rules for some of the expressions we have already seen in class; they are produced and slightly adapted below for your convenience. We define the rule for pairs, the pattern matching lets are up-to you.
Γ ` n : int Γ ` true : bool Γ ` false : bool Γ ` e : bool Γ ` e1 : T Γ ` e2 : T Γ ` if e then e1 else e2 : T Γ ` e1 : int Γ ` e2 : int Γ ` e1 + e2 : int Γ ` e1 : int Γ ` e2 : int Γ ` e1 ∗e2 : int Γ ` e1 : t1 Γ ` e2 : t2 Γ ` (e1,e2) : t1 ×t2 2
Q1.7 (5 points) Finally, we want to define the operational semantics for our language. Build on the big-step evaluation rules we have defined in the notes for part of our language and show the rules which must be added to cover the new constructs. In particular, think carefully how to define the operational semantics for evaluating let pair (x,y) = e1 in e2 end. Q1.8 (9 points) Extend the definition of the eval function to support pairs and their pattern matching.
Q2. TIMTOWTDI – There’s more than one way to do it [20 points] While pattern matching let expressions are very convenient, there is another option to take apart pairs, namely projections. Projections allow one to get the first or the second component of a pair. We add the following expressions to our language: Expressions e ::= ··· | fst e | snd e These two new operations are an alternative way of writing programs without using pattern matching lets. Some examples of these new operations are:
fst (1,true) : is a value of type int let z = (3,2) in fst z + snd z end : is well-typed with type int and it evaluates to 5. let z = (false,7) in if (fst z) then 1 else snd z end : is well-typed with type int and it evaluates to 7. let z = 14 in if x then 1 else snd y end : is not well-typed because projections require a pair to eliminate.
Q2.1 (10 points) Extend on paper the definition for FV(e) which computes the free variables of the new expressions and in the template file hw5.ml using the extended expression data-type, extend the definition of free variables. Q2.2 (10 points) Extend on paper the definition of substitution [e/x]e0 where we replace any free occurrence of the variable x in the expression e0 with the expression e and extend the definition of subst function.
Q3. Spring Cleaning During Fall [30 points] Realistic implementations of languages often try to optimize the execution time of the expressions as written by the user. These are transformations from code to code (in our case values of type Exp.exp to Exp.exp). We can define the type of modules that perform this optimizations as follows:
3
module type Optimization = sig val optimize : E.exp - E.exp end In this question we will explore a common compiler phase called: dead code elimination. That is, we will eliminate expressions that are assigned to a variable but the variable is never used. To illustrate the transformation, let’s consider some examples: let x = 7 in 9 end ⇒ 9 let x = 7 in x end ⇒ let x = 7 in x end let pair (x,y) = (3,false) in if y then x + 1 else 7 end ⇒ let pair (x,y) = (3,false) in if y then x + 1 else 7 end let pair (x,y) = (3,false) in x + 1 end ⇒let pair (x,y) = (3,false) in x + 1 end let pair (x,y) = (3,false) in if false then 1 else 2 end ⇒ if false then 1 else 2 let z = 3 in let x = 7 in let y = x in z end end end ⇒ let z = 3 in z end Q2.1 (15 points) Implement a module called DeadCode of type Optimization that implements this transformation. Notice that to correctly implement the last case you may need to perform more than one pass (depending on your implementation).
Another interesting transformation it is to eliminate all calls to pattern matching lets into regular lets and projections. The idea is to transform pattern matching lets into the regular lets and then take the pairs apart using projections. Let’s consider some examples: (1,true) ⇒ (1,true) let pair (x,y) = (3,2) in x + y end ⇒ let z = (3,2) in fst z + snd z end let pair (x,y) = (false,7) in if x then 1 else y end ⇒ let z = (false,7) in if (fst z) then 1 else snd z end Q2.2 (15 points) Implement a module called RemoveLetMatch of type Optimization that implements this transformation.
The goal of this homework is to better understand how to define simple languages, and extend them. This will allow us to use important concepts such as variable binding, free variables, substitution, operational semantics, and typing. This homework is both solved
4
on paper and in OCaml. Your on paper solution should be handed in as a pdf-file. Your code should use the template provided in hw5.ml.
Pleaseseethefile hw5.ml fortheencodingofexpressions.Intheimplementation, wemodel variables using strings.
Q6. Course Evaluations! (Honour Points) Done! Fantastic. Now,pleasetakeamomenttofilloutcourseevaluations! Hereareminder why this is important for everyone: • Course evaluation feedback improve courses. • You and other students can view course evaluation results in Minerva - but only if more than 30% fill out the course evaluations! • The more people fill out the course evaluations, the more representative the results. • It is a way to give back to other students, since the results are shared with them, if more than 30% of you fill them out. • Your professor enjoys reading about your experiences in the course, in class and in completing the homework. Even more, if you actually had fun! • It is a way to give back and say thanks, if you enjoyed the course. • It is a way to voice your concerns anonymously and provide suggestions. • Your responses matter to professor’s careers such as tenure and promotion and merit committees.
The conclusion is:
Fill Out Your Course Evaluations!
5