1. In English, explain the type `∀α, β . α → β.` You are ready for exercise 1. 2. Read Sections 7.3.2 and Section 7.4.1, starting on pages page 473 and page 474, respectively. We have seen the symbols ρ, τ, and σ before, but not with exactly this usage. (a) In this new context, what does ρ represent? How does it differ from the way we used ρ before? (b) In this new context, what does τ represent? How does it differ from the way we used τ in typed μScheme? (c) In this new context, what does σ represent? How does it differ from the way we used σ before? (d) Say briefly what, in nano-ML, is the difference between τ and σ. You are ready for exercise 2. And you are preparing for exercise 19. 3. Read the first two pages of Section 7.4.3, which explain "substitutions" and "instances." (a) Write a single substitution that replaces type variables α and β with types `sym` and `bool`, respectively. (b) Write a type τ that is an instance of the polymorphic type scheme `∀α . α list → int`. You have a foundation on which to get ready for exercises 18 and S. 4. 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. Define 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? Justify your answer. (c) What if new substitution `(α₂ ↦ int)` is applied to C? Does the resulting constraint have a solution? Justify your answer. You are getting ready for exercises 18 and S. 5. 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₂`? Justify your answer. (d) Explain why constraint `C₄` can't be solved: (e) Can constraint `C₃` be solved? Justify your answer. You are ready for excercises 18 and S. 6. Read the paragraphs that describe the typing rules for `lambda` and for "Milner's Let", which you will find on page 481. Don't overlook the small paragraph following the `lambda` rule. Now look at the `val` definition of `too-poly` in code chunk 481. The right-hand side of the `val` definition is a `lambda` expression with the name `empty-list` playing the role of `x₁`. (a) The rule for `lambda` says that we can pick any type `τ₁` for `empty-list`. After we've chosen `τ₁`, what is the *type scheme* to which `empty-list` (playing `x₁`) is bound in the extended environment which is used to check $e$? (b) Given that the rule for `lambda` says that we can pick any type `τ₁` for `empty-list`, why can't we pick a `τ₁` that makes the `lambda` expression type-check? Now look at the definition of `not-too-poly` in code chunk 482. The right-hand side is an example of Milner's `let` with `empty-list` playing the role of $x$, the literal `'()` playing the role of $e'$, and an application of `pair` playing the role of $e$. Suppose that Γ ⊢ `'()` : β list, where β is a type variable that does not appear anywhere in Γ. That is to say, the literal `'()` is given the type β list, which is playing the role of τ'. (c) What are the free type variables of τ'? (d) What set plays the role of `{ α₁, ..., αₙ }`? (e) What is the *type scheme* to which `empty-list` (playing x) is bound in the extended environment which is used to check $e$? Look at the VAR rule on page 480 and at the definition of the *instance* relation <: on page 476: (f) Given the type scheme of `empty-list` in `not-too-poly`, and given that `empty-list` is used in two different places, what type τ do you choose at each use of the VAR rule? (g) Explain informally why `not-too-poly` type checks. In exercises 19 and T, you are now ready to implement typing rules for syntactic forms that use `generalize`, including the VAL and LET forms.