- [25 points] Consider the language FbP' which is
Fb with pairs but lacking the left/right projections. Instead, it supports pattern matching on pairs as an extension to Let. So for example you could write
Let (x,y) = (Fun z -> z)(True, 2+1) In If x Then y Else 0
These new patterns are shallow only, for example you cannot write Let (x,(z,y)) = ..., and the x and y need to be variables.
- Give the BNF grammar for FbP' based on the above informal description. Be sure to include the grammar of values as well. Note it is a strict extension of the Fb grammar.
- Give the operational semantics rules for FbP' which are not already in the Fb rule set.
- Prove that FbP (the pairs of Section 3.1 in the book) and FbP' above have equivalent expressiveness: make an FbP macro encoding the above new pattern match, and make FbP' macros for the left/right pair projections.
- Write an OCaml interpreter for FbP', in the
form of a function
eval : expr -> expr. You can leave out all the standard Fb evalaution clauses. Define a revised expr type as part of your answer. You are free to use "..." for the parts already in Fb. Note your code need not run, we will not run it, but you could run it if you chose to verify it is correct. You don't need to write out the code for the auxiliary functions like subst.
- [10 points]
This question concerns operational equivalence for FbP'. Its definition is completely analogous to Definition 2.16 in the book, applied to FbP' in place of Fb.
- Propose a new general FbP' operational equivalence principle for Let (x,y) = .... One principle could be "Let (x,y) = (Fun z -> z)(True, 2+1) In If x Then y Else 0 ~= 3", but that is non-general to the extreme. Come up with a general principle in the spirit of the other principles in Section 2.4.2. Be careful to make a true principle!
- Now use your new general principle to prove the non-general principle given above. You can also use the other principles of 2.4.2 as steps in your proof.
- [20 points]
Consider a typed version of FbP' from the previous question, TFbP', which extends TFb of Section 6.2.2 of the book. Along with pairs and the new Let pattern match syntax, TFbP' also includes regular typed-Let of the form Let x : tau = e in e (which was left out of TFb). Note that unlike OCaml there is no polymorphism on Let, this question concerns monomorphic Let only.
- Give the BNF grammar of TFbP'. Make sure to include a grammar for the types, and appropriate type declarations in the code to make writing a type checker feasible.
- Now, write out the new type rules. Include two rules for Let, one for the normal let and one for the new pairs pattern let.
- Write out a TFbP' typecheck function which includes the cases for the two new Let forms as well as for pairs. You don't need to repeat all the old TFb clauses, "..." is fine. Look at Section 6.3 of the book to recall the TFb type checker structure.
- Finally, consider STFbRP' -- adding pairs to STFbR. Generally this is just putting together the STFbR with the pair rules from TFbP' as per the previous question, but some new subtyping rules tau <: tau' may be needed. Either give the new subtyping rules or argue no new subtyping rules are needed.
- [15 points] This question concerns operational semantics for printing.
- Consider language FbPrint, Fb with printing. This printing is similar to what was in the AFbV binary, but can only print integers. Additional expression
Print(e) will print out the result of expression e assuming e evaluates to an integer. Printing is a side effect like state and actors; propose a side-effecting operational semantics ==> for FbPrint (adding any extra parameters or annotations to ==> as needed), and write the operational semantics rules for + and Print expressions (the other rules will be similar). Make sure that you record prints in the order they occurred.
- When we did the AFbV operational semantics we did not include Print as a side-effect, only the actor side-effects (messages and newly created actors were accumulated in a set). For this question, show how we could combine both actor and print side effects in the ==> relation for actors. Make sure you keep the print side effects in order as above.
- [15 points] Joey is a seriously spacey PL student. In his PL homework he coded
all his recursive functions incorrectly -- for example for the
summate function he wrote
combY (Function arg -> Function this ->
If arg = 0 Then 0 Else arg + this (arg - 1)) 5
reversing arg and this in the parameter list, which will not work!
- But, we can work around Joey's error. Give a modified definition of
Y, joeY, which would work for Joey's program above, i.e.
joeY (Function arg -> Function this ->
If arg = 0 Then 0 Else arg + this (arg - 1))) 5 ==> 15
- Now, write a combinator (i.e., Fb expression)
joeyFix which we can
put between Joey's bad code and the normal Y to fix his
argument out-of-order problem so the normal Y will again work:
combY ( joeyFix (Function arg -> Function this ->
If arg = 0 Then 0 Else arg + this (arg - 1))) 5 ==> 15
- On some of the other examples Joey got mixed up with the object encoding and forgot that he didn't need to pass
this to itself and he wrote a recursive
function like
combY (Function this -> Function arg ->
If arg = 0 Then 0 Else arg + this this (arg - 1)) 5
(notice the extra this not needed with Y). Write a joeYY
version of Y which would work around this bug so that
joeYY (Function this -> Function arg ->
If arg = 0 Then 0 Else arg + this this (arg - 1))) 5 ==> 15
now works. Your answers need to be general combinators for these types of errors, not just for summate.
- [12 points] Recall the mutable records of OCaml: some fields may be declared mutable which means they can be mutated just like refs. Here is an OCaml dialog as a refresher:
# type rt = {mutable a : int; mutable b : int};;
type rt = { mutable a : int; mutable b : int; }
# let r = { a = 5; b = 7};;
val r : rt = {a = 5; b = 7}
# r.b <- 4;;
- : unit = ()
# r;;
- : rt = {a = 5; b = 4}
# r.b;;
- : int = 4
This question concerns a typed language with mutable records, TFbmR. For simplicity, we will assume all fields are mutable in any record. Compared to FbR the only additional syntax is e.l <- e for l a record label. This is the same as the OCaml mutable fields in records, it is like having keyword mutable on every field.
- TFbmR is a typed language with these mutable records. For this question give all type rules needed for any record operation (including the new mutation operator). You don't need to repeat any type rules of TFb, but do give all the record-related typing rules.
- Now consider STFbmR in which we add subtyping like we did in STFbR, but now the fields are potentially mutable. You don't need to write out any rules, but think about what it should be.
Which direction is correct? { a : Int; b : Int } <: { a : Int }, or { a : Int } <: { a : Int; b : Int } Or, are both incorrect? Briefly justify your answer.
- Repeat the previous question, but for { c : { a : Int; b : Int }} and {c : { a : Int }}.
- [15 points] Last question, yay! Since it is the last question it is going to be a hard one which we don't expect many people will get.
The Leibnizian notion
of operational equivalence ~= we defined for Fb is a very general notion: "no observable difference in any context". But, as we saw in lecture there is subtlety in getting the proper definition of "observable" and "context". For this question we consider how to define operational equivalence for AFbV. Remember we are defining equivalence of code (i.e. expressions), not the actors themselves. One example of an equivalence we would like to have hold beyond the 1 + 1 ~= 2 sort of thing is
(Let d = Create((Fun me -> Fun data -> Fun msg -> 0),0) In 5) ~= 5
Here we create an actor and put it in d but since that variable is never used and its scope ends, it is a garbage actor we could never reach! So, we may as well have never Created it. So, even though it is in the global actor state its presence there is not observable by other code. Fortunately, Lebnitzian notions are extremely general and even work in this case.
- Define a general notion of ~= for AFbV expressions such that it is an equivalance relation and also supports the two examples given above (and, does not equate too much, so for example 1 ~= 2 must fail).
- Equivalence in the presence of side effects can make equivalent pure functional programs not equal. The question is if this is possible in AFbV: either find two concrete Fb programs e1 and e2 (they can have free variables but are otherwise fully defined) such that e1 ~= e2 in Fb, but e1 ~/= e2 (it fails) in AFbV. OR, argue informally why no such e1/e2 exist.