# CS231 Types and Programming Languages Homework 3

## Problem 4
### a.

Given: function x: T1 -> if x then 0 else 1
Let T1 = Bool and T2 = Int

Typing Derivation:

----------------T-Var   --------------T-TRUE     -------------T-FALSE
G, x: Bool |- x: Bool   G, x: Bool |- 0: Int     G, x: Bool |- 1: Int   
--------------------------------------------T-IF
G, x: Bool |- if x then 0 else 1: Int
--------------------------------------------T-FUN
G |- function x: Bool -> if x then 0 else 1 : Int

### b.

Given: function f: T1 -> if (f 0) then 0 else 1
Let T1 = function and T2 = Int

Typing Derivation:

-------------------T-Var   
G, x: function |- 0: Int
--------------------------------------------T-App
G, x: function |- if 0 then 0 else 1
-----------------------------------------------T-FUN
G |- function f: function -> if (f 0) then 0 else 1

### c.

Given: function f: T1 -> function x: T2 -> if (f x) then (x 0) else 1
Let T1 = function and T2 = function

Typing Derivation:
??
-------------------------------------------T-App
G, f: function |- if (f x) then (x 0) else 1
----------------------------------------------T-App
G, f: function |- function x: function -> if (f x) then (x 0) else 1
-----------------------------------------------T-FUN
G |- function f: function -> function x: function -> if (f x) then (x 0) else 1

## 5

(* Problem 5 *)

(* T ::= Bool | T -> T *)
type typ = Bool | Arrow of typ * typ

(* t ::=  x | function x:T -> t | t1 t2 *)
type t = True | Var of string | Function of string * typ * t 
       | FunCall of t * t


(* env is a **type alias** for a list of (string,typ) pairs 
   env is not a new type, like t above, 
   but rather just a name for an existing type. 
   a list of pairs is sometimes called an *association* list.
   OCaml already has some useful operations for manipulating such lists.
   In particular, the function List.assoc (in the List standard library)
   looks up the value associated with a given key in a given association
   list.  e.g., List.assoc "y" [("x", Bool); ("y", Arrow(Bool,Bool))]
   returns Arrow(Bool,Bool).  List.assoc raises a Not_found exception
   if the given key is not in the list.
*)
type env = (string * typ) list

exception TypeError

(* typecheck takes a term (of type t) and a type environment (of type env) 
   and it returns the type of the term, or raises TypeError if the term
   cannot be given a type.  this function should have the same behavior
   as the typechecking rules on the cheat sheet. *)
let rec typecheck (t:t) (env:env) : typ = raise TypeError

## Problem 6
### Part a.
**Theorem:** If null |- t: T, then either t is a value or there exists some term t' such that t -> t'.

We will prove by induction on typing derivation.