►C311/  H311/  A596 Spring 2025 – Programming Languages
▼Assignments
•13 Assignment 13:   Types
    contents  ← prev  up  next → 

13 Assignment 13: Types

Preliminaries

From 04-16_proof.rkt in the lecture notes, recall the grammar for types, type environments, judgments, and proofs:
  Type = num
  | bool
  | (Type * Type)
  | (Type -> Type)
  | (Type + Type)
     
  TEnv = ()
  | Symbol
  | ((Symbol Type) . TEnv)
     
  Judgment = (TEnv /- Expr : Type)
     
  Proof = (Judgment because . ListOfProofs)
     
  ListOfProofs = ()
  | (Proof . ListOfProofs)
The initial type environment just contains the following entries:
((+     (num -> (num -> num)))
 (-     (num -> (num -> num)))
 (zero? (num -> bool        )))
As allowed by the inference-ok? function, below are the inference rules:

   

      

   

   

   

Assignment
Types classify programs

Feel free to define functions that automate repetitive aspects of the following exercises.

  1. Define q1 to be a type derivation for (zero? ((- 3) 2)) in the initial type environment. In other words, complete the following proof:
    (define q1
      '((Gamma0 /- (zero? ((- 3) 2)) : ...)
        because
        ...))
    To visualize and check your work, use the draw-proof and unproven-judgments functions in 04-16_proof.rkt in the lecture notes.
    > (unproven-judgments q1)
    '()

  2. Define q2 to be a type derivation for (λ x (zero? ((- 3) x))) in the initial type environment.

  3. Define q3 to be a type derivation for (λ x (λ y (pair ((+ x) y) ((- x) y)))) in the initial type environment.

  4. Define q4 to be a type derivation for (λ p ((+ (fst p)) (snd p))) in the initial type environment.

  5. Define q5 to be a type derivation for (λ p (pair (snd p) (fst p))) in the initial type environment.

  6. Define q6 to be a type derivation for (λ p (if (fst p) (fst p) (snd p))) in the initial type environment.

  7. Define q7 to be a type derivation for (λ b (λ p (if b (pair #t (snd p)) (pair (fst p) 3)))) in the initial type environment.

  8. Define q8 to be a type derivation for (λ f (λ x (f (f x)))) in the initial type environment.

  9. Define q9 to be a type derivation for (λ f (λ g (λ x (f (g x))))) in the initial type environment.

  10. Define q10 to be a type derivation for (λ x (case x y (right y) z (left z))) in the initial type environment.

Types reject programs

In comments, explain briefly in English to someone who knows how our programs run but is unfamiliar with our type system:

  1. Why doesn’t the program evaluated below have any type? It seems to work fine.
    > (value-of '(((λ b (if b zero? (+ 1))) #t) 3)
                init-env)

  2. Why doesn’t the program evaluated below have any type? It seems to work fine.
    > (value-of '(((λ b (λ x (if b (pair 3 x) x))) #t) 4)
                init-env)

  3. Why doesn’t the program evaluated below have any type? It seems to work fine.
    > (value-of '((λ x (x x)) (λ x (x x)))
                init-env)

Extending the type system

Let’s extend our type system to handle let expressions. Here’s their grammar:
  Expr = (let Symbol Expr Expr)

  1. Define and test a function inference-ok-let? that takes a Proof and determines whether its root is a valid inference for the type of a let expression. The two premises for the inference should be type judgments for the two subexpressions. Check just the root inference, not how the two premises are themselves proven.
    > (inference-ok-let?
       '((Gamma0 /- (let + ((+ 3) 2) (zero? +)) : bool)
         because
         ((Gamma0 /- ((+ 3) 2) : num) because I said so)
         ((((+ num) . Gamma0) /- (zero? +) : bool) because it is trivial)))
    #t

Brainteasers: Programs inhabit types

Knowing that a program has a type can tell us a lot about what the program does. For instance, every program that has both the type num and the type bool has to be an infinite loop:
> (value-of '((rec f x (f x)) 3)
            init-env)

  1. Define bb to be a list of as many programs as you can think of, each of which has the type (bool -> bool) in the initial type environment. The programs must each behave differently.

  2. Define bbnn to be a list of as many programs as you can think of, each of which has both the type (bool -> bool) and the type (num -> num) in the initial type environment. The programs must each behave differently.

  3. Define bbbnnn to be a list of as many programs as you can think of, each of which has both the type ((bool * bool) -> bool) and the type ((num * num) -> num) in the initial type environment. The programs must each behave differently.

Just Dessert

Let’s extend our type system to handle lists:
  Expr = (null)
  | (cons Expr Expr)
  | (lcase Expr Expr Symbol Symbol Expr)
     
  Type = (Type list)
For instance, here’s the definition of map:
(rec map f
  (λ lst
    (lcase lst
      (null)
      x xs (cons (f x) ((map f) xs)))))
It ought to have the type ((num -> bool) -> ((num list) -> (bool list))).

  1. Define and test a function inference-ok-lists? that takes a Proof and determines whether its root is a valid inference for the type of a null, cons, or lcase expression. Check just the root inference, not how the premises are themselves proven.

    contents  ← prev  up  next →