Homework # 11
due Tuesday, November 22

Reading

Please read Chapter 22 in your textbook.

Problems

Please do the following problems (with some variation, as noted): The programming questions should be done in the context of the reconbase type checker, changing only the core.ml file. Please attach a printout of your core.ml file to your physical homework; leave the full implementation in the Homework #11 directory.

• Exercise 22.2.3
• Exercise 22.3.3
• Exercise 22.3.9
  Instead of using the approach given here, please have the $F$ and $F'$ being passed around be integers, where you assume the existence of an infinite (coutable) set of variables You may use the solution to the assignment if you get stuck, but remember that the solution deals with lists, not integers.

  For the proof, omit all but the VAR, APP and ABS rules. The proof is very short if you define equivalence correctly.

• Exercise 22.3.10
  Your function that generates constraints should start:

  
  let rec recon ctx nextnum t =
    match t with
  

  To append lists, use List.concat. Lists may be created using [$p_0$;$p_1$;...;$p_n$].

  You should handle Bool and Nat in addition to the pure lambda calculus terms in the previous problem.

• Exercises 22.4.3, 22.4.6
  Check your answers against the solution in the book; do not turn them in.
• Exercise 22.5.2
• Exercise 22.5.5
  Your program should not be interactive. Just do what all our checkers have done: read things from a file. (In other words, simply get the program to compile and run correctly. You do not need to change any files other than core.ml.)
• Implement the rule in 22.6 whenever the type variable is called ``_''

About this document