Due: By the beginning of lecture on Wednesday, April 22.
You are required to typeset your answers. Not only will this make your
answers easier to read, but it will make your work easier if you can use an editor to cut/paste/modify
parts of different problems. We strongly recommend using LaTeX since it
is superior for layout of mathematical material. If you choose to use
some other word processing application, please be sure that it produces
equally high quality output.
Consider the expressions e, e′, [e/f]e′ and [f←e]e′ as defined on page 111
in Harper's book (or slide 25 from Functions-PDF).
Assuming y: τ, f: τ → τ′ and τ≠σ (as Harper does at the bottom of page 111):
Derive a type for e or show that it is not well-typed.
Derive a type for e′ or show that it is not well-typed.
Derive a type for [e/f]e′ or show that it is not well-typed.
Derive a type for [f←e]e′ or show that it is not well-typed.
Consider the expressions e, e′, [e/f]e′ and [f←e]e′ as defined on page 111
in Harper's book (or slide 25 from Functions-PDF)
and the expression e′′ as defined on page 112 in Harper's book
(or slide 28 from Functions-PDF).
Assuming y: τ, f: τ → τ′ and τ=σ and taking s to be a value of type τ:
Derive a type for [e/f]e′ or show that it is not well-typed.
Derive a type for [f←e]e′ or show that it is not well-typed.
Derive a type for [f←e]e′′ or show that it is not well-typed.
Use the dynamic semantics to derive an evaluation of [e/f]e′(s).
Use the dynamic semantics to derive an evaluation of [f←e]e′(s).
Use the dynamic semantics to derive an evaluation of [f←e]e′′(s).
Consider the definition of recursive functions using ordinary (non-recursive) functions and
general recursion, as given on page 128 in Harper's book
(or slide 27 from RecursiveFunctions-PDF).
Show that the static and dynamic semantics of recursive functions are derivable from this definition.
Show that the definition of natural numbers as a recursive type, given in section 20.2 (p. 172)
in Harper's book
(or slides 28-31 from RecursiveTypes-PDF)
correctly simulates the dynamic semantics for natural numbers given in Chapter 15 of Harper's book.
Refer to the slides from RecursiveTypes-PDF.
In the same way that the natlist type is encoded as a recursive type on slides 32-35 (or p. 172-173
in Harper's book), give an encoding of the type of binary trees of nats as a recursive type.
Consider the L{dyn} expression in the middle of page 193 in Harper's book.
Give the abstract syntax for using the expression to compute the sum 1+1.
Show (the interesting steps in) an evaluation of your expression for computing the
sum of 1+1 (your answer to (a) above) using the dynamic semantics of L{dyn}.
Show (the interesting steps in) an evaluation of an expression for computing
the sum of 1+(the identity function) using the dynamic semantics of L{dyn}.
Consider the hybrid typing example (fun ... ) near the top of page 196 in Harper's book.
Translate the example from concrete syntax to the corresponding abstract syntax.
Type and type check the example.
Show (the interesting steps in) using the example function to compute the sum 1+1.
Consider the hybrid typing example (fun ... ) near the bottom of page 196 in Harper's book.
Translate the example from concrete syntax to the corresponding abstract syntax.
Type and type check the example.
Show (the interesting steps in) using the example function to compute the sum 1+1.
Consider the hybrid typing example (fun ... ) on page 197 in Harper's book.
Translate the example from concrete syntax to the corresponding abstract syntax.
Type and type check the example.
Show (the interesting steps in) using the example function to compute the sum 1+1.
Consider the definition of natural numbers in System F given on page 209 in Harpers book.
Show that the static and dynamic semantics given in Chapter 14 are derivable in System F
under this definition.
Show a detailed attempt to type the expression on slide 18.
Give an example of an expression like the one on slide 18, but with a suitable
replacement for the "in n" part of the expression, that could be successfully typed using the
static semantics for existential types.
Show the typing derivation for your answer to (b) above.
Consider the encoding of existential types using System F given on page 222 of Harper's book
(or slide 25 in Exist-PDF). Show that this
encoding correctly reflects the static and dynamic semantics of existential types.
