Assignment 5, Due November 22nd, 1:00 p.m.

1. Figure 9.5 on Page 159 gives subtyping rules for types in the typed-lambda calculus.  (i) Explain the logic behind the subtype rules for Sum and Record; (ii) Why is it that a subtype record type has more fields than its supertype, while a subtype sum type has fewer variants than its supertype?
2. Give a code fragment in lambda calculus that illustrates BdExist (again in Figure 9.5).  Your example should create values of both the supertype and subtype existential types with S and T being different types.
3. Exercise 9.3.1 on Page 151
4. Explain what these functions do and give the type that SML would infer for the following functions.  Also, explain how you arrived at your type (the SML/NJ compiler said so is not a valid answer ;-))
   1. fun aggr f null = 0
         |  aggr f (h::t) = f(h) + aggr f t;
   2. fun nodup x y = if x = y then x::nil else x::(y::nil);
   3. fun foldl f (e, []) = e
          | foldl f (e, h::t) = foldl f (f(e,h), t);
5. The C# reference describes a new language proposed by Microsoft as an alternative to Java.  (i) Describe what Boxing and Unboxing mean in the context of C#.  Given an example that illustrates the usefulness of boxing and unboxing.  (ii) Describe Delegates in the context of C#.  Give an example that illustrates the usefulness of delegates.  (iii) C++ uses the same syntax for overriding inherited virtual methods and for declaring new virtual methods.  C# uses a keyword "override" to distinguish between the two.  Which do you prefer and why?