types.rkt

;; Using the type rules on the practice exam
;;
;; Write typing derivations of the following judgements.
;; If there is no possible typing derivation, explain
;; the issue.

{ x : num → (bool → bool), z : bool } ⊢ ((x 3) z) : bool

{ z : bool } ⊢ ((lambda (x : bool → num) (x z)) (lambda (y : bool) z)) : num

{ y : num + (bool → bool) } ⊢ (cons 5 (case y of (left x => x) (right y => 23))) : num * num

{ x : (num -> num) * (bool -> bool) } ⊢ (if ((cdr x) #f) ((car x) 5) ((car x) 8)) : num

;; For each of the following, find a term with the given type
;; 
;; If no the type has no inhabitants, explain why.

(num -> (num -> (num * num)))

(num -> num) -> ((bool -> num) -> num)

(num -> num) -> (bool -> (num -> num))

(num * bool) -> (bool * num)

(num + bool) -> (bool * num)