Tute (Week 10)

1. Overloading
2. Subtyping
- 2.1. Coercions and Subtyping
- 2.2. Constructor variance
3. LCR Conditions
4. Session Types

1. Overloading

Consider the following file in Haskell:

class Compare a where
  cmp :: a -> a -> Bool

instance Compare Int where
  cmp x y = x <= y

instance (Compare a) => Compare [a] where
  cmp xs ys = and (zipWith cmp xs ys)

group  :: (Compare a) => [a] -> [[a]]
group []     = []
group (x:xs) = let (ys, zs) = span (cmp x) xs
                in (x:ys) : group zs

How would the type checker translate this code to remove the type classes?

2. Subtyping

2.1. Coercions and Subtyping

You are given the type Rectangle, parameterised by its height and width, and the type Square parameterised by the length of one of its sides. Neither type is mutable.

a. Which type is the subtype, which type is the supertype?

b. Give a subtype/supertype ordering of the following set of function types: Rectangle -> Rectangle, Rectangle -> Square, Square -> Rectangle, Square -> Square.

c. Define a data type Square and a data type Rectangle in Haskell. Then define a coercion function from elements of the subclass to elements of the superclass.

d. Show that the ordering you have given in the previous question is correct by defining coercion functions for each pair of types in a subtyping relationship in part (b).

2.2. Constructor variance

List some examples of a covariant, contravariant and invariant type constructor.

3. LCR Conditions

Consider the following two processes, each manipulating a shared variable \(x\), which starts out at \(0\).

Thread 1: \(x := x + 1; x:= x - 1;\)

Thread 2: \(x := x \times 2\)

a) What are the possible final values of \(x\) assuming each statement is executed atomically?

b) Rewrite the above program into one where each statement obeys the limited critical reference restriction. What are the possible final values now?

c) How could locks be used in your answer to (b) to ensure that only the final results from part (a) are possible?

4. Session Types

Using the session-typed process calculus introduced in the lecture, specify the process and type for a server that first takes the name of a product for sale, then provides a choice between two services:

Quote: output a price of type Price, then do nothing.
Sell: input payment details of type CardNo, output a receipt of type Receipt, then do nothing.

a) Define the types (i) Quote and (ii) Sell in terms of Price, CardNo, Receipt.

b) Assume we have processes give_price |- Γ,y:Price that transmits a Price along channel y and complete_sale |- Γ,y:CardNo,z:Receipt that accepts a CardNo on channel y then sends a Receipt on channel z. (You can leave their typing derivations unexpanded.)

Specify processes (i) quote of type Quote and (ii) sell of type Sell and show their typing derivations.

c) Suppose the names of products for sale have type Name. Now specify the process and derive the type of the entire server. (You can leave quote, sell and their typing derivations unexpanded.)

d) (i) Specify a process and type of a client seeking a quote from this server. You can specify the types as duals of the types above.

(ii) Show the typing derivation for the part that chooses to get the quote. You can leave get_price and its typing derivation unexpanded.

e) Show the reduction of the process formed by parallel composition of the above client process with the server process.