1. Read Section 6.3, which describes how Typed Impcore is extended
    with arrays.  Examine code chunk 403, which shows the cases that
    have to be added to the type checker.  For each case, name the
    corresponding type rule, and explain the rule in informal English:

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

        Your explanation of the rule:



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

        Your explanation of the rule:



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

        Your explanation of the rule:



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

        Your explanation of the rule:




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

 2. Exercise 8 asks you to design new syntax and type rules for lists.
    In μScheme, we operate on lists by calling polymorphic functions.
    But in a monomorphic language, you must design *new syntax* for
    each list operation.

    (a) In the initial basis of μScheme, what four functions on lists
        would be sufficient to implement all the others?





    Exercise 8 asks you to label each of your rules as
    a formation rule, an introduction rule, or an elimination rule.
    Read the sidebar on "Formation, introduction, and elimination" on
    page 404.

    (b) Suppose that for each of the functions in part (a), you design
        a new syntactic form of expression.  For each function, give
        its name, and say whether you expect the corresponding
        syntactic form to be an introduction form or an elimination
        form.  (An introduction form creates new data, and an
        elimination form interrogates or "takes apart" old data.)

        i.


        ii.


        iii.


        iv. 



    (c) How many formation rules will you need, and why?




    (d) You will need at least one rule for each of the syntactic
        forms in part (b), and you will need whatever formation rules
        you have listed in part (c).  Do you expect to need any other
        rules? If so, why?



    
    You are now ready for Exercise 8.





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

    (a) Variable `syms` holds a list of symbols.  What expression do
        you write to compute its length?




    (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.


 4. Read about type equivalence on pages 430 and 431.

    You are given ML values `tau1` and `tau2`, which represent the
    respective Typed μScheme types `(forall ['a] 'a)` and `(forall ['b] 'b)`.
    These types are equivalent, but if you code `tau1 = tau2`, you'll
    get `false`.  In your type checker, what code do you write to
    determine if `tau1` and `tau2` are equivalent?




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



 5. 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.


 6. Exercise 24 on page 458 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, and why?



    (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.)


    Read "Primitives of Typed μScheme" in section M.4 of Appendix M on
    page 1294.

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


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


    You are ready for Exercise 24.