cs-4400-sp26

hw5: STLC with sums, products, and mu

Instructions:

• Due date: Friday, March 20 (11:59pm)
• Upload your solutions to GradeScope. You should upload a single file called code.rkt. Be sure to check that your uploaded solution is valid; you will receive 0 points if your solution does not run.
• Your programs will be evaluated on the fraction of tests that they pass. We will show you some tests, but not all tests. You should test your code thoroughly. After the submission deadline, we will reveal the hidden tests.
• Starter code: hw5-starter.rkt

1 Designing a typechecker and synthesizer for LExp [75 points]

(define-type LType
  [UnitT]
  [ProdT (t1 : LType) (t2 : LType)]
  [SumT (t1 : LType) (t2 : LType)]
  [FunT (arg : LType) (body : LType)]
  [MuT (var : Symbol) (body : LType)]
  [VarT (id : Symbol)])

(define-type LExp
  [foldE (e : LExp)]
  [unfoldE (e : LExp)]
  [fixE (x : Symbol) (e : LExp)]
  [varE (s : Symbol)]
  [unitE]
  [pairE (e1 : LExp) (e2 : LExp)]
  [pi1E (e : LExp)]
  [pi2E (e : LExp)]
  [tag1E (e : LExp)]
  [tag2E (e : LExp)]
  [caseE (s : LExp)
         (x : Symbol) (b1 : LExp)
         (y : Symbol) (b2 : LExp)]
  [lamE (id : Symbol) (body : LExp)]
  [appE (fun : LExp) (arg : LExp)]
  [annoE (e : LExp) (t : LType)])

We have provided you an interpreter for the LExp language (syntax given above) in the starter code; you should not change this interpreter. We have also provided a type checker and type synthesizer with some (but not all) cases already implemented.

An LType and LExp can be represented by the following CFG:

t ::= Unit | t x t | t + t | t -> t | mu a.t | a 

e ::= fold(e) | unfold(e) | fix(x.e) | x | () | (e1, e2)
      | pi1(e) | pi2(e) | tag1E(e) | tag2E(e)
      | case(e, x.e1, y.e2) | λx.e | e1 e2 | (e : t)

Your task is to implement the missing cases in type-check and type-synth.

• 1.1: Add a case for the annotation term in synthesis (annoE).
• 1.2: Add cases for sum types in both checking and synthesis (tag1E, tag2E, caseE).
• 1.3: Add cases for recursive types (foldE and unfoldE)
• 1.4: Add a case for fixed point expressions (fixE)

As usual, please include unit tests to make sure your implementation is working as expected for all the new cases.

2 Encodings with recursive types [25 points]

Given the following encoding of natural numbers:

(define-type Nat
  [Zero]
  [Succ (n : Nat)])

(encode-nat : (Nat -> LExp))
(define (encode-nat n)
  (type-case Nat n
    [(Zero) zeroE]
    [(Succ n) (foldE (tag2E (encode-nat n)))]))
	
;; Examples:
(define oneE (encode-nat (Succ (Zero))))
(define twoE (encode-nat (Succ (Succ (Zero)))))

Your task is to:

• 2.1 (15 points): Implement the addition function addE as a LExp (STLC+) expression.
• 2.2 (10 points): Write the expected type for addE as a LType.