1. Read Section 6.3, which describes how Typed Impcore is extended
    with arrays.  Examine code chunk 411, which shows the cases that
    have to be added to the type checker.  For each case, write down exactly
    one choice for a rule name (A-D) and exactly one choice for a
    prose description (1-4) below the case.  No rule names or prose
    descriptions should be repeated.

    Your choices for rule names are:
      A) MakeArray
      B) ArraySize
      C) ArrayPut
      D) ArrayAt

    Your choices for prose descriptions are:
      1) This rule first checks that expression `a` has type "array of tau," that
         expression `i` has type int, and that expression `e` has that same type tau.
         It then says that the type of the whole expression has type "tau."

      2) This rule first checks that expression `a` has type "array of some tau,"
         and then determines that the type of the whole epxression is int.

      3) This rule first checks that expression `len` has type int, and then
         determines that expression `init` has some type tau. It then determines
         that the whole expression has type "array of tau."

      4) This rule first checks the expression `a` has type "array of some tau"
         and that expression `i` has type int. It then says that the type of the
         whole expression is tau.



    For each of the following cases, indicate your selections immediatley
    below the text "The rule for case..."
      * The rule for case `| ty (AAT (a, i)) = ...` is:


      * The rule for case `| ty (APUT (a, i, e)) = ...` is:


      * The rule for case `| ty (AMAKE (len, init)) = ...` is:


      * The rule for case `| ty (ASIZE a) = ...` is:


    You are now ready for exercise 2 in the pair problems.

 2. Read Section 6.6.3 on quantified types in Typed μScheme.

    (a) Assume variable `syms` holds a list of symbols.  What expression do
        you write to compute its length? Pick exactly one of the options below.

        1. `(length syms)`
        2. `((o length sym) syms)`
        3. `((@ length sym) syms)`
        4. `((length sym) syms)`


    (b) You are given a function `larger?` of type `(int -> bool)`.
        Using the predefined function `o`, what code do you write to
        compose `larger?` with `not`?


    (c) In testing, we sometimes use a three-argument function `third`
        that ignores its first two arguments and returns its third
        argument.  Such a function has type

            (forall ('a 'b 'c) ('a 'b 'c -> 'c))

        There is only one sensible function that has this type.
        Using a `val` definition, define function `third` in Typed μScheme.

    You are ready for exercise TD.


 3. Read about type equivalence starting on page 438
    and page 439.

    You are given ML values `tau1` and `tau2`, which represent the
    respective Typed μScheme types `(forall ['a] 'a)` and `(forall ['b] 'b)`.
    Semantically, these types are equivalent. For each of the two ML
    expressions below, say whether the expression produces `true`
    or produces `false`. Write each answer immediately below the
    expression.

    (a) `tau1 = tau2`


    (b) `eqType tau1 tau2`


    You will soon be ready for Exercise 23, but
    you first need to complete the next comprehension question.



 4. Read Section 6.6.5 on typing rules for expressions in Typed μScheme.
    For each of the expressions below, say if it is well typed, and if
    so what its type is.  If the expression is not well typed, say
    what typing rule fails and why.

        ; (a)
        (if #t 1 #f)

        ; (b)         
        (let ([x 1]
              [y 2])
           (+ x y))

        ; (c)
        (lambda ([x : int]) x)

        ; (d)
        (lambda ([x : 'a]) x)

        ; (e)
        (type-lambda ['a] (lambda ([x : 'a]) x))
  
    You are now ready for Exercise 23.


 5. Exercise 24 on page 466 calls for you to add a
    primitive queue type to Typed μScheme. Read it.  Then read
    "Primitive type constructors of Typed uScheme" in Section 6.6.9.

    (a) Which existing primitive type most resembles a queue type?



    (b) When you add a primitive type constructor for queues, what
        chunk of the source code do you intend to add it to?
        (Give the page number, and if applicable, the letter. For example,
        page 448 has two chunks---448a and 448d---and the letter is the
        simplest way to distinguish the two.)


    Read "Primitives of Typed μScheme" in Section M.4, which starts on page 1224.

    (c) Which set of primitive functions most resembles the functions
        you will need to add for queues?


    (d) When you add primitives functions that operate on queues, what
        chunk of the source code do you intend to add it to?
        (Just like we asked above, give the page number, and if
        applicable, the letter.)


    You are ready for Exercise 24.