1. Read section 6.3.3, which describes how Typed Impcore is extended
with arrays. Examine code chunk 417, which shows the cases that
have to be added to the type checker.
For each case, name the type-system rule that applies. Each
answer should be a rule name like Apply or GlobalAssign.
* 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:
Now pick one of the rules and explain, in informal English, what
the rule is supposed to do.
_You are ready for exercise 2 in the pair problems._
2. Read section 6.6.3 on quantified types in Typed μScheme.
In addition to the prose, read the transcripts in the first couple
pages of that section: each value that has a quantified type is
instantiated later in the transcript, giving you more examples to
relate back to the prose.
(a) Assume variable `syms` holds a list of symbols (it has type
`(list sym)`). 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 `positive?` of type `(int -> bool)`.
Using the predefined function `o`, which has type
`(forall ('a 'b 'c) (('b -> 'c) ('a -> 'b) -> ('a -> 'c)))`,
what code do you write to compose `positive?` 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 will need to use both `type-lambda` and `lambda`.
_You are ready for exercise TD._
3. Read about type equivalence starting on page 445
and page 446.
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 two comprehension questions._
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 almost ready for exercise 23._
5. Read the [handout on "Program Design with Typing
Rules"](../handouts/typroofs.pdf). In particular, read the
explanation of how the [If]{.smallcaps} rule is rewritten to add
type-equality judgments τ ≡ τ3 and τ1 ≡ bool. Now look at the
list of typing rules for expressions in Figure 6.9 on page 471.
Identify one other rule that needs to be rewritten in the same
fashion as [If]{.smallcaps}, for the same reason.
The rule you found is named →
_You are now ready for exercise 23._
6. Exercise A below calls for you to add a primitive array type to
Typed μScheme. Read it. Then read "Primitive type constructors of
Typed uScheme" in section 6.6.9, which starts on page 455.
(a) When you add a primitive type constructor for arrays, 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 451 has chunks 451a and
451b, and the letter is the simplest way to
distinguish the two.)
In section M.4, which starts on page 1263, read "Primitives of
Typed μScheme."
(b) Which set of primitive functions most resembles the functions
you will need to add for arrays?
(c) When you add primitives functions that operate on arrays, 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 A._