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.