601.426/626, Princples of Programming Languages
Spring 2018
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. [16 points] Consider an extension to FbS which adds const references: FbcS. The only new concrete syntax needed is @e, which expects e to be a cell reference and returns a const version. Const cells can be dereferenced but not assigned to. e.g.

   Let x = Ref 3 In Let cx = @x In !cx

   evals to 3, while

   Let x = Ref 3 In Let cx = @x In cx := 3

   does not compute to any value (it gets stuck). Note that

   Let x = Ref 3 In Let cx = @x In x:= 4; !cx

   will not get stuck, creating a const reference only makes that reference immutable, but the underlying cell is still mutable; this expression returns 4. Note that dereference ! in these examples is overloaded to work on either normal references or const references. The type for a const reference to a value with type tau is tau ConstRef.
   1. Give the operational semantics for FbcS as an extension to FbS (you only need to give new or changed values, rules etc).
   2. We can extend FbcS to a typed version TFbcS. As with the previous question start from the TFbS type rules and add or modify the rules.
   3. Now consider STFbcS in which we add a subtyping relation between constant references and normal references. Which direction is correct? tau Ref <: tau ConstRef, or tau ConstRef <: tau Ref? Or, are both incorrect? Briefly justify your answer.
   4. Picking an incorrect subtyping rule from the previous question give a program which will typecheck using that subtype rule but will have run-time type error (it will get stuck).
(extra page to answer question 1.)
2. [9+1 points] Let's play every PL student's favorite game, pull out the points! Put each of the expressions below in an Fb context C such that the result of C[the-question-expression] returns the number of points you get for the question (the limit is 3, any number over 3 is 3 points). Of course, your context C cannot include any integer constants or integer operators. (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 3))
   2. g (Fun self -> Fun arg -> If arg = 0 Then 0 Else arg + self self (arg - 1)) 2
   3. g (Fun self -> Fun arg -> If arg = 0 Then 0 Else arg + self (arg - 1)) 2
   4. (hard one for one point extra credit)
      w (Fun f -> ((Fun b -> Fun f -> f 1 f) ((f 1) (f 1)) (f f))) (Fun x -> x + 1)

3. [10 points] One thing both Leandro and Shriram pointed out in their lectures is how JavaScript programs "hardly ever get stuck", nearly any operator applied to any values will return something even if its somewhat non-sensical.
   1. For this question you need to JavaScript-ize Fb: define the operational semantics of FbJS which has the identical syntax and values of Fb, but includes extra rules such that nothing ever gets stuck. You can't change the existing Fb rules because they define the correct behavior when the program is well-formed, but you can add as many new rules as you want (do make sure your new rules don't make the language non-deterministic, however!). Note that you are free to return whatever values you wish for these newly-allowed cases, for example True and 0 can return True, 0, or any other value really.
   2. Adding these rules can change the notion of operational equivalence on programs. For this part, give two Fb programs which are operationally equivalent as Fb programs, but are not operationally equivalent as FbJS programs, or argue that no such two programs exist.
   3. For this question it's just the reverse of the previous: give two Fb programs which are operationally equivalent as FbJS programs, but are not operationally equivalent as Fb programs, or argue that no such two programs exist.

4. [10 points] This question concerns actor programing. In AFbV, assume there is a program with the following initialization code skeleton:

   Let techie = ... In
   Let disarmer = ... In
   Let techie1 = Create(techie, 2) In
   Let techie2 = Create(techie, 2) In
   Let a_disarmer = Create(disarmer, (techie1, techie2)) In
     a_disarmer <- 'ready 0;;
   		

   1. Write behaviors for the techie and disarmer such that the following constraints hold:
      • Each techie must send two `bomb(_) messages to the disarmer in total, no more, no less.
      • You can never have two `bomb(_) messages in the global soup at once, it will blow up if so.
      Note that you can send any other messages of your own design and generally do anything as long as it meets the above two conditions.
   2. Argue in words how your program enforces the constraint that no two `bomb(_) messages can be in the soup at any point.

5. [8 points] Trace EFb's type inference algorithm specification (the book version, not your OCaml code) for the following programs. (1) Show the EFb type derivation tree and (2) the subsequent constraint closure, then (3) check for inconsistencies and, if there are none, (4) simplify the type.
   1. (Fun x -> x + 1)(True)
   2. (Fun f -> f 1)(Fun x -> x - 1)
   In both cases be sure to specify if type inference succeeded or failed.
   (Blank page one, if you run out of room on any question say "see blank one" and write here)
   (Blank page two, if you run out of room on any question say "see blank two" and write here)