| |
Due on Friday November 30.
A Simple Type System for EFL
- Do Exercise 15.1. You don't have to show the proof of each judgment --
just be sure to get it right. Also, if one of the expressions has more
than one typing, provide just one of them, but say whether or not more exist.
- Suppose we were to change the tuple semantics so that indexing is dynamic,
as we did in Problem Set 7. Give sound inference rules for this modified
tuple, both for tuple introduction and elimination. Does your solution
completely avoid run-time errors? Explain.
- In a style similar to that given for lists, what is an appropriate
recursive type for trees, where internal nodes have integer values, and leaves
are like NIL for lists. For comparison, in Haskell we might write such a
datatype as:
data Tree = Leaf | Node Int
Tree Tree
- Show that, with the introduction of recursive types, there exist infinite
type derivations. Explain why this might be a problem for automatic type
inference.
|