For any single question below you can alternatively write “Freebie” as your answer and you will get 25 points on it. If you use no “Freebie” you will have all questions graded and will have a +5 bonus added to your final exam score.
I pledge I used no resources other than my handwritten cheat sheet for this exam.
(25 points) We primarily focused on operational equivalence for Fb during the course, but the definition naturally generalizes to other languages we studied (and even to JavaScript, Python, etc). For example for FbR, the definition of ~= will read identically and the only difference is the contexts C will be FbR contexts not Fb contexts, and the ==> evaluation relation will also be FbR’s.
a. For the theory of FbR operational equivalence, are there any equations on pure Fb programs which would fail if they were applied to FbR and its operational equivalence? In other words are there an e1 and e2 in Fb such that e1 ~= e2, but viewing them as FbR programs (since FbR is a strict superset language) and using FbR ~=, that e1 ~= e2 would fail? Either give an example or a sentence arguing why not.
b. For the theory of FbR operational equivalence, propose one useful ~= law to add to the Fb laws we had such as beta, etc. Your law needs to deal with the new record syntax and should be a useful and general law, not something vacuous like {} ~= {}.
c. Use your new FbR law and the existing Fb laws to prove
Let r = { a = 5; b = (Fun x -> x) } In (r.b) 5 ~= (Fun x -> x) 5. Show your steps and name any laws used.
d. For languages with side effects such as FbS the same general notion of operational equivalence also can work, but the definition needs to be adapted slightly because FbS has a store, S, in its ==> relation. Write out what a reasonable definition of operational equivalence would be for FbS: “e1 ~= e2 in FbS if and only if …”
e. (This question is a repeat of a. but for FbS) For the theory of FbS operational equivalence, are there any equations on pure Fb programs which would fail if they were applied to FbS and its operational equivalence? In other words are there an e1 and e2 in Fb such that e1 ~= e2, but viewing them as FbS programs (since FbS is a strict superset language) and using FbS ~=, that e1 ~= e2 would fail? Either give an example or a sentence arguing why not.
(25 points) In lecture we covered how variants and records could be encoded in each other. For this question we are going to look at how variants can be encoded in records. In order to make things simpler, we will only encode a simple Some/None variant and not all variants.
a. First let us define a brand-new language FbSN which just has just these simple variants. The new grammar elements are Some(e), None, and Unwrap e Default e. The first two are just like in OCaml option type; the meaning of this unwrapper should be clear from a couple examples: Unwrap Some(1) Default 5 returns 1, whereas Unwrap None Default 5 has no Some to unwrap so returns 5, the default. Unwrap 33 Default 5 gets stuck, only Some/None can be unwrapped. And, Unwrap Some(0) Default (0 0) returns 0, the default case can be completely ignored here.
For this part, give the novel operational semantics rules for FbSN, in particular for the three new syntax elements.
b. Now we would like to encode the FbSN behavior in FbR. For this part, we will just hack it up aka use the design pattern of records. Concretely, for the following FbSN example show how the similar behavior could be encoded in records:
Let f = Fun sn -> (Unwrap sn Default 4) + 1 In f (Some(3)) + f None
(Hint: recall from the encoding of variants in records that each variant name corresponds to a record field name, and definitions and uses swap so a use of a variant is a definition of a record, and a definition of a variant is a use of a record.)
c. Now take the informal intuitions of the previous question and use it to define a general translation function FbSNtoFBR(e) which translates any FbSN program e to an equivalent-behaving FbR program. You can write your function either as math or as informal OCaml, as long as it is clear what you mean.
(25 points) This question concerns records, subtyping, and STFbR.
a. For a warm-up, give the TFbR rules for typing records and record projections.
b. Now, give the STFbR subtyping rule for records and the subsumption type rule.
c. With the rules above, show how records can have types with fewer fields in the type than is in the record: write a complete type derivation for |- {a = 5; b = False} : {b : Bool}
d. An informal intuition we gave about records with subtyping is the type (such as {b : Bool}) means any records in this type must have a boolean b field, but also may have any other fields of any type. On the other hand, in just TFbR records must have all of the declared fields, and no more. For this part, consider an opposite notion from STFbR, where a record type such as {a : Int; b : Bool} means only that it may have these fields, and if so at the indicated types, and that it can have no other fields. So for example |- {a = 5} : {a : Int; b : Bool} would hold – it doesn’t have to have a b field. |- {a = 5} : {a : Bool; b : Bool} would fail (a’s type conflicts) as would |- {a = 5; b = False} : {b : Bool} (record has more fields than is in the type). Call this new language OSTFbR, the O for “Opposite”. Keep all the STFbR rules except for the record subtyping rule, and suggest a new verion of that rule for which these examples would typecheck (or not) appropriately.
e. Discuss briefly the viability of OSTFbR as a programming language. Would it be sensible/sound/usable/etc?
(25 points) AFbV had a somewhat odd property that messages may not arrive in the order sent. so for example if one actor a executed code (b <- 5); (b <- 7) where b was some other actor’s address, b could receive the 7 message before the 5 message.
For this question, you are going to fix this oddity and make a modified operational AFbV semantics which preserves message ordering: messages will always arrive in the order sent.
Here are a few hints on how to do this. The local actor computation relation e =S=> v produces a set S of new messages and new actors; this clearly will not work as that would cause the two messages in the example above to be put in the set and their sequence order be lost. So the S must be changed. Additionally, in the global soup G it is currently also a set and it would instead need to also preserve message order. You don’t need to give every last rule, but do show the revised message send rule and the revised global stepping rule.