CS 5535: Homework 2

1. A rule known as the contravariant rule (also known as the arrow rule) may be used to determine subtyping between procedure types.  It states that:

   PROCEDURE P1 (Params1): Result1 <: PROCEDURE P2 (Params2): Result2
if
(a) Result1 <: Result2, and
(b) Params2 <: Params1, i.e., each parameter in Params2 is a subtype of the corresponding parameter in Params1.
For example,
   PROCEDURE f (i: fT1, j: fT2): fT3 <: PROCEDURE g (i: gT1, j: gT2): gT3
if
(a) fT3 <: gT3, and
(b) gT1 <: fT1 and gT2 <: fT2.
Answer the following questions about this rule (5 points per question, total 15):
 (a) Does this rule follow from the definition of subtypes?  Explain.
 (b) Give an example of using this rule (you may use the syntax of your favorite language)
 (c) The Modula-3 type system paper presents an argument against using this rule in Modula-3. Illustrate the thrust of the Modula-3 argument with an example.
2. Give an example of inclusion polymorphism involving objects in your favorite object-oriented language.  Your example should make use of method invocations and overriding.  Now show how this example could be expressed in Cardelli and Wegner's terminology involving sets, quantifiers, and bounded quantifiers. (15 points)
3. In typed lambda calculus, give two functions (10 points each), curry and uncurry, such that

  (a) curry takes a function that takes two arguments and curries it.  For example it takes function with signature
          fun (x: Integer, y: Integer) (returns Integer)
       and returns a function with signature
          fun (x: Integer) (returns Integer->Integer) fun (y: Integer) (returns Integer)
  (b) uncurry goes the oppsite direction as curry (i.e., takes a curried function and returns a function that takes a pair)