Homework # 8
due November 1

Reading

Please read Chapters 15 and 16 in your textbook. You may skip section 15.6.

Problems

Please do the following problems

• Exercise 15.2.1
• Exercise 15.2.3
• Exercise 16.1.2
• Exercise 16.1.3

Check your answers against the solutions in the book, but do not turn in anything unless you have questions.

Please do the following problems:

• Exercise 15.5.1
• Exercise 15.5.2
• Exercise 16.2.1
• Exercise 16.2.3

Turn in your answers to these problems.

Discussion

Assuming we have Top and Bot types, and `joins,' how can we type check lists (see section 11.12, pp.146-147). without requiring annotations on the terms (although we still require list types to include the element type)? Give (non-algorithmic) type rules. You may use the answer to Exercise 11.12.2 to help you.

Then write out algorithmic typechecking rules for the simply-typed lambda calculus with unannotated lists. You may assume algorithmic join and subtyping rules are already defined. You will need to add new rules for subtyping as well as rules for checking terms. Make sure your rules handle Top and Bot correctly.

About this document