601.426/626, Princples of Programming Languages
Spring 2019
Final Examination

You can use one handwritten 8.5x11 notes sheet. Please put your name on your sheet, and we will be collecting them at the end of the exam. Good Luck!

1. [20 points] Consider the language Fb-- which is Fb with functions and application only. This language is also called the pure lambda calculus since all it has is functions.
   1. Write out all of the operational semantics rules for Fb--. Your cheat sheet could come in handy here :-)
   2. Write a complete OCaml interpreter for Fb--, in the form of a function eval : expr -> expr. Since this language is so tiny there are not many cases to consider and the interpreter won't take that long to write out. You can assume and use the following datatypes:

      type ident = Ident of string
      
      type expr = 
       Var of ident | Function of ident * expr | Appl of expr * expr 

   3. Modify the Fb-- operational semantics in your part a. answer to be call-by-name, making variant Fb--N: in call-by-name, function arguments are only evaluated when they are needed, not right when the function is called. An example in FbN is (Fun x -> x + x)(1 + 2) which would compute by computing (1 + 2) + (1 + 2), whereas in the Fb interpreter this would compute by computing 3 + 3, the argument (1 + 2) is first evaluated before the function is called. One test that you got your rule correct is diverging function arguments should pose no problem if they are never used: for example,

      (Fun x -> Fun y -> y)((Fun z -> z z)(Fun z -> z z)) ==> Fun y -> y

      in Fb--N, whereas in Fb-- it would not compute to any value.
   4. Consider a similar shrinking of TFb to TFb--. Since integers and booleans are removed the type grammar would be just

       τ ::= τ -> τ 

      but this completely fails in a really bad way; why?
   5. OK, let us fix this by making the type grammar include type variables like in the inferencer:

       τ ::= τ -> τ | 'a 

      An example typing would be program |- (Fun x : 'a -> x)(Fun y : 'b -> y) : 'a. Write out all of the type rules for TFb--.
   (Blank page on which to finish question 1 if you need room)

2. [8 points] The Abort control operator causes a program to immediately terminate and return a value. For this question we will add abort to the very simple language Fb-- in question 1, giving a new language Fb--Ab. It will include a new syntax form Abort(e) which when executed returns the value of e and quits. As an example,

   (Fun x -> (Fun z -> z))(Abort((Fun y -> y)) ==> Fun y -> y

   If we extended abort to full FbAb we would also have an example like 7 + Abort(1 + 3) ==> 4.

   For this question, write all of the operational semantics rules for Fb--Ab. Feel free to include rules from your answer to question 1 by referring to them.

3. [9 points] Sorry, there will be no pull out the points game this year, all the points in the points-bank got used up in the last few years. But as a consolation prize we will play a similar game, pull out the difference. Concretely, for each pair of Fb expressions below, prove they are not operationally equivalent using the definition of operational equivalence. Make sure to give the explicit context C which "pulls out the difference" as per the definition. (Note: remember the context C hole filling can never change the parsing order; one way to guarantee this is to put ( • ) instead of just •.)
   1. (Fun x -> y (x x)) and (Fun x -> y (x y))
   2. (Fun self -> Fun arg -> If arg = 0 Then 0 Else arg + self self (arg - 1)) and (Fun self -> Fun arg -> If arg = 0 Then 0 Else arg + self (arg - 1))
   3. x + 0 and x

4. [8 points] Several homeworks concerned languages with a record append operation, @. For this question assume we also have such an operation in a hypothetical language FbR@. An example use of it is

   Let r = {a = 5; c = 6} In Let rr = {b = 7; c = True } In Let rrr = r @ rr In rrr.c  ==> True

   Notice in particular from this example how if a field is in both records the appended record takes the field from the right record. This is also a functional operation, neither r nor rr was changed by the @ operation.

   For this question we are just going to explore some programming benefits of having such an append operation. With record append, it is much simpler to encode inheritance or even object extension. For this question, encode a simple Point object as a record with integer fields x, y and methods magnitude, isZero and then define an extension to it (its the same object but with more goodies added) called MorePoint which includes an additional method isNotZero which simply negates the result of calling isZero on the object. Concretely, the program

   Let Point = ... In Let MorePoint = ... (use @ and Point, don't repeat code here) ... In MorePoint.isNotZero MorePoint {}

   should appropriately execute. All you need to write for your answer is how Point and MorePoint are defined.

5. [20 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
   	      

   For this question you are to define a language with mutable records, FbmR. For simplicity, we will assume all fields in a record are mutable. Compared to FbR you only need to support the additional field mutation syntax e.l <- e for l a record label.
   1. Give the operational semantics for FbmR which should follow the analogous OCaml behavior as shown in the OCaml top loop example above. Since there is mutation you will need a store S as in FbS; you can make the format of the store be whatever you want. Also as with FbS you will need to redo all of the old Fb rules to thread the state. Since that would take a lot of writing, for your answer here just show the revised + rule. Do make sure to give rules for all of the record operations: record formation, projection (.) and field mutation (<-).
   2. We can extend FbmR to a typed version TFbmR. For this question give all type rules needed for any record operation. You don't need to repeat any type rules of TFb, but do give all the record-related typing rules.
   3. 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.
   4. Repeat the previous question, but for { c : { a : Int; b : Int }} and {c : { a : Int }}.
(extra page to continue to answer question 5.)
(Blank page, if you run out of room on any question say "see blank" and write here)