CSE 505 Homework 3: Lambda Calculus

Problems 1 and 2 due Thursday, February 17, at the start of class.
Problem 3 due Tuesday, February 22, at the start of class.

Problem 1: Typing derivations

Consider the following expression in the simply typed lambda calculus (with the unit base type *):

(λ x: * → * . (λ y:* . x y)) ((λ a:* → * . λ b:* → * . a) (λ c:* . c) (λ d:* . d))
Draw the full derivation tree by which you prove the type of this expression in the empty type environment. Label each "line" in the tree by the inference rule used.  Use the type system given in lecture.

Problem 2: Lambda calculus extensions

  1. Add a divide operator to the simply typed lambda calculus with ints and bools. Division by zero should yield a special exn value, and any computation examining an exn value should itself yield an exn value. Define extensions to the syntax of types, expressions, and/or values, give any new or revised typing rules, and give any new or revised big-step evaluation rules.
  2. Add record patterns to the simply typed lambda calculus with (at least) records. Define any extensions to the syntax of types, expressions, and/or values, give any new or revised typing rules, and give any new or revised big-step evaluation rules.
  3. The lecture notes extended the call-by-value simply typed lambda calculus with records. Add records to the call-by-name simply typed lambda calculus, defining any extensions to the syntax of types, expressions, and/or values, giving any new typing rules, and giving any new big-step evaluation rules. Give an example of a program that would "work" under the call-by-name semantics but not the call-by-value semantics.  Explain how this semantics relates to real data structures in Haskell.
  4. Recall that we added fix to the simply typed lambda calculus to allow programming recursive values, particularly functions.
    1. The evaluation rule given for fix only works under normal-order or call-by-name evaluation rules, but not applicative-order or call-by-value evaluation rules. Why?
    2. An alternative way to add recursion to the simply typed lambda calculus is to add letrec instead of fix. Give reasonable syntax, typing rule(s), and big-step call-by-value evaluation rule(s) for this extension.

Problem 3: Soundness proof

Extend the proof of soundness presented in class of the pure simply typed lambda calculus using call-by-name evaluation to also account for tagged unions, using the small-step semantics given in the textbook (called variants there). You should do this by first defining new cases for the definition of substitution [E2/X]E for when E is one of the two tagged union expression forms, then adding cases to the proofs of the canonical forms, progress, substitution, and preservation lemmas.

Turn-in instructions

Turn in a hardcopy of your answers, with your name at the top.

chambers@cs.washington.edu