typed-lambda-calculus.v

Require Import String Arith List Bool Ascii.
Scheme Equality for string.

(*
 * The Simply-Typed Lambda Calculus
 *)

(*
 * Two base types:
 *  - Integers (natural numbers)
 *  - Functions (from type -> type)
 *)
Inductive type: Set :=
| IntTy  : type
| BoolTy : type
| FnTy   : type -> type -> type.

(*
 * Implementation of structural equality for types.
 *)
Fixpoint eq_type (t1: type) (t2: type): bool :=
  match t1, t2 with
  | IntTy, IntTy => true
  | BoolTy, BoolTy => true
  | FnTy arg ret, FnTy arg' ret' =>
    eq_type arg arg' && eq_type ret ret'
  | _, _ => false
  end.

(*
 * Prove that for all types `t`, eq_type t t holds
 *)
Theorem eq_type_correct t: eq_type t t = true.
Proof.
  induction t; simpl; trivial.
  rewrite IHt1.
  rewrite IHt2.
  tauto.
Qed.

(*
 * Expressions. Lambda calculus defines:
 *  - Var (a variable binding)
 *  - Lam (a lambda abstraction with a binder and an expression)
 *  - App (function application)
 * Extended to include:
 *  - Num (natural numbers)
 *  - Bool (boolean values)
 *)
Inductive exp : Set :=
| Bool : bool -> exp
| Num  : nat -> exp
| Var  : string -> exp
| Lam  : string -> type -> exp -> exp
| App  : exp -> exp -> exp
| If   : exp -> exp -> exp -> exp.

(*
 * Define a function to look up a type in an environment.
 * This is a simple O(n) look through a lit of pairs of
 * (string, type), representing the type of bound variables.
 *)
Definition find_in_env T (env: list (string * T)) (name: string) :=
  match (find (fun p => string_beq (fst p) name) env) with
  | None => None
  | Some (pair n v) => Some v
  end.

(*
 * Definition of monadic bind for option.
 *)
Definition option_bind A B (opt: option A) (f: A -> option B): option B :=
  match opt with
  | Some v => f v
  | None => None
  end.

(*
 * Actual type inferencing logic.
 * Always infer:
 *  - Num n -> Int
 *  - Bool b -> Bool
 *  - Var s -> whatever's in the environment for "s"
 *  - Lam binder arg_ty body -> function from arg_ty to type of body
 *  - App e1 e2 -> ensure e1 is a function that accepts e2 as
 *                 its argument, then the result is the return type
 *                 of e1.
 *)
Fixpoint infer (env: list (string * type)) (e: exp) :=
  match e with
  | Num n            => Some IntTy
  | Bool b           => Some BoolTy
  | Var s            => find_in_env type env s
  | Lam binder arg_ty body =>
    option_map
      (fun t' => FnTy arg_ty t')
      (infer ((binder, arg_ty)::env) body)
  | App e1 e2 =>
    match infer env e1 with
    | Some (FnTy e1t ret) =>
      match (infer env e2) with
      | Some e2t => if (eq_type e1t e2t) then Some ret else None
      | _ => None
      end
    | _ => None
    end
  | If b e1 e2 =>
    match infer env b with
    | Some BoolTy =>
      option_bind type type (infer env e1)
        (fun e1t =>
          option_bind type type (infer env e2)
            (fun e2t =>
              if eq_type e1t e2t then Some e1t else None))
    | _ => None
    end
  end.

(*
 * Proves that the inferencing engine can infer:
 *   env => (Num n) : IntTy
 * for all natural numbers n.
 *)
Theorem can_infer_num (n: nat) (env: list (string * type)):
  infer env (Num n) = Some IntTy.
Proof.
  tauto.
Qed.

(*
 * Proves that the inferencing engine can infer:
 *   env => (Bool b) : BoolTy
 * for `true` and `false.
 *)
Theorem can_infer_bool (b: bool) (env: list (string * type)):
  infer env (Bool b) = Some BoolTy.
Proof.
  tauto.
Qed.

Theorem can_infer_if (e1 e2 e3: exp) (t: type) (env: list (string * type)):
  (infer env e1) = Some BoolTy ->
  (infer env e2) = Some t ->
  (infer env e3) = Some t ->
  infer env (If e1 e2 e3) = Some t.
Proof.
  intros.
  simpl.
  rewrite H, H0, H1; simpl.
  rewrite eq_type_correct.
  trivial.
Qed.

(*
 * The following proofs are convenience theorems I needed
 * in order to eliminate string comparisons while proving
 * name-based lookup.
 *)

(*
 * Proves that a bool equals itself.
 *)
Theorem bool_identity b: bool_beq b b = true.
Proof.
  induction b; trivial.
Qed.

(*
 * Proves that an ascii character equals itself.
 *)
Theorem ascii_identity a: ascii_beq a a = true.
Proof.
  induction a.
  simpl.
  do 8 rewrite bool_identity.
  trivial.
Qed.

(*
 * Proves that a string equals itself.
 *)
Theorem string_identity s: string_beq s s = true.
Proof.
  induction s.
  trivial.
  simpl.
  rewrite IHs.
  rewrite ascii_identity.
  trivial.
Qed.

(*
 * Proves that the inferencing engine can infer:
 *  env => (\x: t . x): t -> t
 * which implies it can infer variables from the environment.
 *)
Theorem can_infer_var (s: string) (t: type) (env: list (string * type)):
  infer env (Lam s t (Var s)) = Some (FnTy t t).
Proof.
  simpl.
  unfold option_map.
  unfold find_in_env.
  simpl.
  rewrite string_identity.
  trivial.
Qed.

(*
 * Proves that the inferencing engine can infer:
 *  env => e1 : t1 -> t2
 *  env => e2 : t1
 *  --------------------
 *  env => (e1 e2) : t2
 * for all expressions e1 and e2.
 *)
Theorem can_infer_app (e1 e2: exp) (t1 t2: type) env:
  (infer env e1 = Some (FnTy t1 t2)) ->
  (infer env e2 = Some t1) ->
  infer env (App e1 e2) = Some t2.
Proof.
  intros.
  simpl.
  rewrite H.
  rewrite H0.
  rewrite eq_type_correct.
  reflexivity.
Qed.

(*
 * Proves that the inferencing engine can infer:
 *   env(s: t1) => e : t2
 *   ---------------------------
 *   (Lam s t1 e) : (FnTy t1 t2)
 *
 * for all expressions e.
 *)
Theorem can_infer_lam e t1 t2 s env:
  infer ((s, t1)::env) e = Some t2 ->
  infer env (Lam s t1 e) = Some (FnTy t1 t2).
Proof.
  intros.
  simpl.
  unfold option_map.
  rewrite H.
  trivial.
Qed.

(*
 * Proves that the inferencing engine cannot infer the type of:
 *   (Lam s1 t (Var s2))
 * if s1 != s2
 *)
Theorem cannot_infer_unsound_code t s1 s2:
  string_beq s1 s2 = false ->
  infer nil (Lam s1 t (Var s2)) = None.
Proof.
  intros.
  simpl.
  unfold option_map.
  unfold find_in_env.
  simpl.
  rewrite H.
  reflexivity.
Qed.