Homework 3

Written problems due: Wednesday, July 23, 2025, 12:30pm (before class)

Coding problems due: Friday, July 25, 2025, 11:59pm PDT on Gradescope

Instructions

There are be 2 types of problems:

1. Written problems are marked with ✍️.

   • Must be done individually.
   • Please turn in a stapled, physical copy of your solutions before the lecture start time on the due date.
   • For each sub-problem, please provide a self-grade out of 2 points: 2 for a fully solved problem with a correct solution, 1 for a partially correct attempt with all work shown, and 0 for no attempt. If you're unsure whether your solution is correct, you can leave it as ?, and I will grade it for you.
   • On the first page of your solutions, please include your name (on Canvas/Gradescope), student ID, and a table containing the self-grades for each sub-problem, like this:

   Problem	Sub-problem	Self-grade (0/1/2/?)
   1	A	2
   1	B	2
   1	C	1
   1	D	?

   • If you handwrite your solutions, please write clearly and legibly.

2. Coding problems are marked with 🧑‍💻.

   • Can be done individually or in pairs.
   • Coding problems are autograded on Gradescope.
   • You can submit as many times as you want.
   • Note that you can use a maximum of 2 late days for each HW's coding problems, but not for the written problems.

Other important notes:

• Problems (written or coding) marked with ⭐️ are extra credit problems. You can do them for fun and for extra credit, but they are completely optional.

• You're encouraged to talk about the problems with the instructor, the TA, and your classmates, but you must write your own solutions.

• Note you won't be able to turn in corrections to homework problems, unlike quizzes.

• Use of generative AI tools and coding assistants is not allowed for this assignment.

• If you have any questions about the assignment, please post them in the #hw3 Discord channel, or come to the office hours.

Part 0 - Conceptual Problems

Problem 1 (✍️ written, 2 pts)

Finish the case of e1 == e2 in the proof of the type abstraction lemma.

Problem 2 (✍️ written, 2 pts)

Consider an alternative typing rule for if expressions:

Gamma |- e1 : Bool
Gamma |- e2 : t
---------------------------------- T-If*
Gamma |- if e1 then e2 else e3 : t

Redo the proof of the type abstraction lemma for if expressions using T-If* rule until the proof gets stuck. Then:

• Indicate the exact place where the proof fails
• Give some intuition why T-If* would not allow the proof to go through.
• Construct a counterexample that shows that a type system with this new rule is unsound.

Problem 3 (✍️ written, 2 pts)

Pick one typing rule (other than the original T-If rule) for the variable-free subset of Lamp. Modify it to make the type system unsound. Then:

• Do the proof of the type abstraction lemma for this modified rule until the proof gets stuck.
• Indicate the exact place where the proof fails.
• Give some intuition why this modified typing rule would not allow the proof to go through.

Problem 4 (✍️ written, 2 pts)

Construct a Lamp expression e such that

• e evaluates to a value
• e is ill-typed
• e does not use if-then-else. Essentially, this problem asks you to show that Lamp's type system is incomplete not only for if-then-else, but also for other constructs.

Problem 5 (✍️ written, 2 pts)

Construct a Lamp expression uncurry that takes a function accepting "2 arguments", and returns an equivalent function that accepts "1 argument" that is a pair.

For example, consider the function \x. \y. x + y. Then uncurry (\x. \y. x + y) should return a function equivalent to the following:

\p. let (x, y) = p in x + y

Problem 6 (✍️ written, 2 pts)

Construct a Lamp expression curry that takes a function accepting "1 argument" that is a pair, and returns an equivalent function that accepts "2 arguments".

For example, consider the function \p. let (x, y) = p in x + y. Then curry (\p. let (x, y) = p in x + y) should return a function equivalent to the following:

\x. \y. x + y

Problem 7 (✍️ written, 2 pts)

Show that for any type t1, t2, and t3, your curry function has the type ((t1, t2) -> t3) -> (t1 -> t2 -> t3) by drawing a type derivation tree for your curry function.

Problem 8 (✍️ written, 2 pts)

For the type ((t1, t2) -> t3) -> (t1 -> t2 -> t3), replace

• , with logical conjunction /\
• -> with logical implication ->. Write down the boolean proposition that you get. Then input this formula into an online truth table generator. What do you observe about the last column of the truth table?

Problem 9 (✍️ written, 2 pts)

If we think of a type as a set containing all values of that type, then we can compute the size of a type as the number of values in that set. For example, the size of Nat is infinite, since there are infinitely many natural numbers. The size of Bool is 2, since there are exactly two boolean values: True and False.

Define a Python function size(t: Type) -> Optional[int] that computes the size of a type t. If the type is infinite, the function should return None.

def size(t: Type) -> Optional[int]:
    match t:
        case TNat():
            return None
        case TBool():
            return 2
        case TProd(ts):
            pass
            # your code here
        case TFun(t1, t2):
            pass
            # your code here
        case _:
            raise ValueError(f"Unknown type: {t}")

You do not need to account for recursive types in this problem. For function types, only count the number of behaviorially distinct functions, i.e., \x. x + 1 and \x. x + 2 are considered different functions, but \x. x + 1 and \y. 1 + y + 0 are considered the same function, since they behave the same way for all inputs.

Part 1 - Programming in Lamp

Carefully read the updated Lamp Reference Manual. Again, a reference implementation of Lamp is available on CSIL as ~junrui/lamp (for evaluation) and ~junrui/lamp-ty (for typing). Please use them to test your Lamp programs.

Before you jump into coding, let us explain some new shiny concrete syntax added to Lamp:

• Every abbreviation needs to be annotated with a type. So the Fib function should be defined as:

  def Fib: Nat -> Nat = \n. ...
  

• All other type annotations are optional. But you can manually provide additional type annotations (as a form of machine-checked documentation) to any expression using the syntax e: t.

• We generalize pairs to n-tuples, where n can be any natural number (including 0). For example, (1, 2, 3) is a 3-tuple, and () is a 0-tuple (aka a unit). The elimination form is extended analogously to n-tuples, so you can write:

  let (x1, x2, ..., xn) = e1 in e2
  

  There is no concrete syntax for 1-tuples, so (1) is treated as 1 (but your code doesn't need to have a special case for this).

For all problems in Part 1 (this part) of the HW, please use the reference implementation to check if the Lamp programs you wrote are correct or not!!! You'll need to use them as test cases for Part 2 (implementing the Lamp language).

Problem 1 (✍️ written, 2 pts per sub-problem)

Let us use (Bool, Nat, Nat) to represent rational numbers. The first element is a boolean that indicates whether the number is positve, and the second and third elements are the numerator and denominator, respectively. For example, (True, 1, 2) represents 1/2, and (False, 1, 3) represents -1/3.

1. Define a function IsCanonical: (Bool, Nat, Nat) -> Bool that checks whether a rational number is in its canonical form. A rational number is in its canonical form if the denominator is not zero and the numerator and denominator are coprime (i.e., their greatest common divisor is 1).
2. Define a function Canonicalize: (Bool, Nat, Nat) -> (Bool, Nat, Nat) that takes a rational number and returns its canonical form (e.g., (False, 1, 2) remains the same, while (True, 2, 4) becomes (True, 1, 2)).
3. Define a function Add: (Bool, Nat, Nat) -> (Bool, Nat, Nat) -> (Bool, Nat, Nat) that takes two rational numbers and returns their sum. The result should be in canonical form.
4. Define a function Sub: (Bool, Nat, Nat) -> (Bool, Nat, Nat) -> (Bool, Nat, Nat) that takes two rational numbers and returns their difference. The result should be in canonical form.
5. Define a function Div: (Bool, Nat, Nat) -> (Bool, Nat, Nat) -> (Bool, Nat, Nat) that takes two rational numbers and returns their division. The result should be in canonical form.

Part 2 - Implementing the Lamp Language

Download the starter code from here.

Problem 1 (🧑‍💻 coding, 10 pts)

The operational semantics of Lamp is already implemented in the eval function. You're highly encouraged to read the code and understand how it works. Your task is to implement the subst function.

For subst, we're generalizing the subst function from HW2 to perform simultaneous substitution of multiple variables. The sigma dictionary maps variables to their replacements, and the function should traverse the AST and apply the substitutions accordingly.

Finally, to run your interpreter, you can do python -m backend.eval < [path to a Lamp file].

Problem 2 (🧑‍💻 coding, 20 pts)

Implement the bidirectional type system for Lamp. The system is specified using inference rules in the Lamp Reference Manual. Your task is to finish the implementation of

• the synth function, which implements the type synthesis judgment
• the check function, which implements the type checking judgment.

To run your type checker, you can do python -m backend.typing < [path to a Lamp file].