1. Read Sections 7.3.2 and Section 7.4.1,
    starting on pages 480 and 481, respectively.  
    We have seen the symbols ρ, τ, and σ before, but not with exactly this usage.

    For parts a, b, and c of this question, please answer each part by
    choosing exactly one of the following descriptions. Write the
    number of your choice directly below the part that it answers. For
    example, you could write 3 below part a, 4 below part b, and 1
    below part c.

    1. ρ represents a mapping from variables to locations
    2. σ represents a type quantified over a list of type variables,
       where each type variable is distinct (otherwise known as a type
       scheme)
    3. τ represents a non-function type
    4. ρ represents a mapping from variables to values
    5. σ represents a list of location-value pairs, where each
       location is distinct (otherwise known as a store)
    6. τ represents a quantifier-free type (otherwise known as a type)

    For part d, write exactly one of True or False as your answer.


    (a) In this new context, what does ρ represent?


    (b) In this new context, what does τ represent?


    (c) In this new context, what does σ represent?


    (d) The symbol τ represents monomorphic types and σ represents polymorphic
        types.



    You are preparing for exercise 19.



 2. Read the first two pages of Section 7.4.3, which explain
    "substitutions" and "instances."


    (a) Yes or no: does the substitution `(α → sym, β → bool, α₂ → int)`
        replace type variables `α` and `β` with types `sym` and `bool`,
        respectively?



    (b) Which of the following are instances of the polymorphic type
        `∀α . α list → int`?  For each one, please indicate whether it
        is an instance of the type (True) or whether it is not an
        instance of the type (False).
        
        `int list`   True or False

        `int list list`  True or False

        `int * int list → list`  True or False



    You have a foundation on which to get ready for exercises
    18 and S.



 3. Read the first page of Section 7.5.2, which shows the form of
    a constraint.   Then skip to the first page of Section 7.5.3,
    which explains how to apply a substitution to a constraint.



    Given substitution `θ = (α₁ ↦ int)` and constraint 
    
    > `C = α₁ ~ α₂ /\ α₂ ~ α₃ list /\ α₄ ~ α₃ list list`.

    Now define C' as the result of applying θ to C.
    
    (a) Write C':


    
    (b) Do you think C' has a solution?  Please answer yes or no.

    Now define D as the result of appliying substitution `(α₂ ↦ int)` to C.

    (c) Write D:

    (d) Do you think D has a solution?  Please answer yes or no.



    You are getting ready for exercises 18 and S.



 4. Now read all of Section 7.5.3, which explains
    how to solve constraints.  

    To demonstrate your understanding, reason about solving these four
    constraints:

    > `C₁ = α ~ int`
    >
    > `C₂ = α ~ bool`
    >
    > `C₃ = C₁ /\ C₂`
    >
    > `C₄ = α₁ ~ α₂ /\ α₂ list ~ α₁`

    (a) Write a substitution `θ₁` that solves constraint `C₁`:
       



    (b) Write a substitution `θ₂` that solves constraint `C₂`:




    (c) Does the composition `θ₂ ∘ θ₁` solve constraint `C₃ = C₁ /\ C₂`?
        Please answer yes or no.




    (d) Can constraint `C₃` be solved? Please answer yes or no.




    (e) Can constraint `C₄` be solved? Please answer yes or no.




    You are ready for excercises 18 and S.