Programming Languages Assignment 5

Due: Wednesday April 20th

  1. (25 points)

    For this problem, we will discuss for-loops in F♭S. We use the syntax For x In e To e Do e Done to describe a for-loop.

    For example, consider the following code: 

    Let c = Ref 0 In
Let junk =
    For x In 1 To 10 Do
        c := !c + x
    Done
In !c

    This expression should evaluate to 55. Observe the following points:

    • The actual value of the For... expression is unspecified, but its effects on state are important.
    • We assume that the first two expression arguments should evaluate to integers. If they are not, the loop may diverge.
    • We assume that the loop always increments by one. If the first argument is greater than the second, your loop may diverge.
    • The loop variable should, of course, be bound in its body on each iteration.

    With that in mind, complete the following:

    1. (10 points)

      First, show that the above syntax can be encoded in F♭S. (You may use Let...In and Let Rec syntax to make your life easier.)

    2. (15 points)

      Now, write the operational semantics rule (or rules) implementing for-loops in F♭SF. Remember that operational semantics rules are not encodings; this rule won't look like your answer to (a) above.

  2. (10 points)

    Show a proof of evaluation of the following F♭X expression: 

                (Function x ->
                Try
                    If x = 0 Then Raise #Go 7 Else Raise #Stop 5
                With #Go n -> n
            ) 0
  3. (40 points + 10 bonus points)
    1. (15 points)

      Recall the language F♭r from Homework 4: F♭ with rings. We will now add an additional piece of syntax to F♭r: RingSize e (which produces an F♭ integer describing how big the ring is).

      We will now define the language TrF♭r; F♭ with rings, type annotations, and Let Rec. This language has the type grammar:

      τ ::= Int | Bool | τ -> τ | Ring τ

      Give the type rules for this language. These rules should cover all of the ring syntax from Homework 4 -- Left, Right, RingAdd, RingDrop, RingGet, and Ring -- as well as the new RingSize syntax. You may assume that TrF♭r includes all of the TF♭ rules in the book (including Let Rec rule).

    2. (5 points)

      Write a function in TrF♭r which takes a ring of integers and calculates their sum. (You will need Let Rec somewhere because you can't type the Y-combinator.) Why would it not be possible to write this function in TrF♭r without the RingSize operator?

    3. (15 points)

      We now consider the TrF♭H: F♭ with type annotations, Let Rec, and heterogeneous rings! This language will permit rings to have contents of different types (like the original F♭r did) but will statically assure that no ring is used in a type-incorrect fashion. The type grammar for this language is:

      τ ::= Int | Bool | τ -> τ | Ring τ @ ... @ τ

      Note that the type of rings has gotten considerably more complicated to accommodate this new requirement. For instance, we would say that the expression Ring 1 @ 2 @ True has the type Ring Int @ Int @ Bool. Write the type rules for this language. (These type rules are considerably more complex than those for TrF♭r.)

    4. (5 points)

      To our dismay, we discover that it is no longer possible to write a function which sums a ring of integers! Explain why this is the case.

    5. (up to 10 bonus points)

      Devise a strategy by which you could enhance TrF♭H so that writing a function which sums over a ring of integers is again possible. There are many such strategies available to you. Your bonus will be determined by the clarity, correctness, and elegance of your solution.

  4. (10 points)

    Write a subtype of the following type: 

    ( { x:Int; y:{z:Bool} } -> { x: Int; y: {z: Int -> Int } } ) ->
{} ->
{ a: { x:Int; y:{z:Bool} }; b: { x: Int; y: {z: Int -> Int } } }

    Your answer must not contain the types { x:Int; y:{z:Bool} } or { x: Int; y: {z: Int -> Int } }.

  5. (15 points)

    Write an EF♭ type derivation of the following code: 

         (Function f -> Function x -> f x) (Function z -> z + z)

    Then, show that this expression has type Int -> Int by computing the closure of the constraint set and solving the constraints as described in the book.

    Be very careful to calculate the right resulting type and constraint set. As a hint, your constraint set should have three pairings in it by the time you are done and, obviously, you should be able to complete the closure algorithm to discern that this expression has the type Int -> Int.