TypecheckingA Typechecker for STLC

The has_type relation of the STLC defines what it means for a term to belong to a type (in some context). But it doesn't, by itself, give us an algorithm for checking whether or not a term is well typed.
Fortunately, the rules defining has_type are syntax directed -- that is, for every syntactic form of the language, there is just one rule that can be used to give a type to terms of that form. This makes it straightforward to translate the typing rules into clauses of a typechecking function that takes a term and a context and either returns the term's type or else signals that the term is not typable.

Comparing Types

First, we need a function to compare two types for equality...
Fixpoint eqb_ty (T1 T2:ty) : bool :=
  match T1,T2 with
  | <{ Bool }> , <{ Bool }> ⇒
      true
  | <{ T11→T12 }>, <{ T21→T22 }> ⇒
      andb (eqb_ty T11 T21) (eqb_ty T12 T22)
  | _,_ ⇒
      false
  end.
... and we need to establish the usual two-way connection between the boolean result returned by eqb_ty and the logical proposition that its inputs are equal.
Lemma eqb_ty_refl : ∀ T,
  eqb_ty T T = true.
Proof.
  intros T. induction T; simpl.
    reflexivity.
    rewrite IHT1. rewrite IHT2. reflexivity. Qed.

Lemma eqb_ty__eq : ∀ T1 T2,
  eqb_ty T1 T2 = true → T1 = T2.
Proof with auto.
  intros T1. induction T1; intros T2 Hbeq; destruct T2; inversion Hbeq.
  - (* T1=Bool *)
    reflexivity.
  - (* T1 = T1_1->T1_2 *)
    rewrite andb_true_iff in H0. inversion H0 as [Hbeq1 Hbeq2].
    apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed.

The Typechecker

The typechecker works by walking over the structure of the given term, returning either Some T or None. Each time we make a recursive call to find out the types of the subterms, we need to pattern-match on the results to make sure that they are not None. Also, in the app case, we use pattern matching to extract the left- and right-hand sides of the function's arrow type (and fail if the type of the function is not T11→T12 for some T11 and T12).
Fixpoint type_check (Gamma : context) (t : tm) : option ty :=
  match t with
  | tm_var x ⇒
      Gamma x
  | <{\x:T2, t1}> ⇒
      match type_check (x ⊢> T2 ; Gamma) t1 with
      | Some T1 ⇒ Some <{T2→T1}>
      | _ ⇒ None
      end
  | <{t1 t2}> ⇒
      match type_check Gamma t1, type_check Gamma t2 with
      | Some <{T11→T12}>, Some T2 ⇒
          if eqb_ty T11 T2 then Some T12 else None
      | _,_ ⇒ None
      end
  | <{true}> ⇒
      Some <{Bool}>
  | <{false}> ⇒
      Some <{Bool}>
  | <{if guard then t else f}> ⇒
      match type_check Gamma guard with
      | Some <{Bool}> ⇒
          match type_check Gamma t, type_check Gamma f with
          | Some T1, Some T2 ⇒
              if eqb_ty T1 T2 then Some T1 else None
          | _,_ ⇒ None
          end
      | _ ⇒ None
      end
  end.

Digression: Improving the Notation

Before we consider the properties of this algorithm, let's write it out again in a cleaner way, using "monadic" notations in the style of Haskell to streamline the plumbing of options. First, we define a notation for composing two potentially failing (i.e., option-returning) computations:
Notation " x <- e1 ;; e2" := (match e1 with
                              | Some x ⇒ e2
                              | None ⇒ None
                              end)
         (right associativity, at level 60).

Second, we define return and fail as synonyms for Some and None:
Notation " 'return' e "
  := (Some e) (at level 60).
Notation " 'fail' "
  := None.

Now we can write the same type-checking function in a more imperative-looking style using these notations.
Fixpoint type_check (Gamma : context) (t : tm) : option ty :=
  match t with
  | tm_var x ⇒
      match Gamma x with
      | Some T ⇒ return T
      | None ⇒ fail
      end
  | <{\x:T2, t1}> ⇒
      T1 <- type_check (x ⊢> T2 ; Gamma) t1 ;;
      return <{T2→T1}>
  | <{t1 t2}> ⇒
      T1 <- type_check Gamma t1 ;;
      T2 <- type_check Gamma t2 ;;
      match T1 with
      | <{T11→T12}> ⇒
          if eqb_ty T11 T2 then return T12 else fail
      | _ ⇒ fail
      end
  | <{true}> ⇒
      return <{ Bool }>
  | <{false}> ⇒
      return <{ Bool }>
  | <{if guard then t1 else t2}> ⇒
      Tguard <- type_check Gamma guard ;;
      T1 <- type_check Gamma t1 ;;
      T2 <- type_check Gamma t2 ;;
      match Tguard with
      | <{ Bool }> ⇒
          if eqb_ty T1 T2 then return T1 else fail
      | _ ⇒ fail
      end
  end.

Properties

To verify that the typechecking algorithm is correct, we show that it is sound and complete for the original has_type relation -- that is, type_check and has_type define the same partial function.
Theorem type_checking_sound : ∀ Gamma t T,
  type_check Gamma t = Some T → has_type Gamma t T.
Proof with eauto.
  intros Gamma t. generalize dependent Gamma.
  induction t; intros Gamma T Htc; inversion Htc.
  - (* var *) rename s into x. destruct (Gamma x) eqn:H.
    rename t into T'. inversion H0. subst. eauto. solve_by_invert.
  - (* app *)
    remember (type_check Gamma t1) as TO1.
    destruct TO1 as [T1|]; try solve_by_invert;
    destruct T1 as [|T11 T12]; try solve_by_invert;
    remember (type_check Gamma t2) as TO2;
    destruct TO2 as [T2|]; try solve_by_invert.
    destruct (eqb_ty T11 T2) eqn: Heqb.
    apply eqb_ty__eq in Heqb.
    inversion H0; subst...
    inversion H0.
  - (* abs *)
    rename s into x, t into T1.
    remember (x ⊢> T1 ; Gamma) as G'.
    remember (type_check G' t0) as TO2.
    destruct TO2; try solve_by_invert.
    inversion H0; subst...
  - (* tru *) eauto.
  - (* fls *) eauto.
  - (* test *)
    remember (type_check Gamma t1) as TOc.
    remember (type_check Gamma t2) as TO1.
    remember (type_check Gamma t3) as TO2.
    destruct TOc as [Tc|]; try solve_by_invert.
    destruct Tc; try solve_by_invert;
    destruct TO1 as [T1|]; try solve_by_invert;
    destruct TO2 as [T2|]; try solve_by_invert.
    destruct (eqb_ty T1 T2) eqn:Heqb;
    try solve_by_invert.
    apply eqb_ty__eq in Heqb.
    inversion H0. subst. subst...
Qed.

Theorem type_checking_complete : ∀ Gamma t T,
  has_type Gamma t T → type_check Gamma t = Some T.
Proof with auto.
  intros Gamma t T Hty.
  induction Hty; simpl.
  - (* T_Var *) destruct (Gamma _) eqn:H0; assumption.
  - (* T_Abs *) rewrite IHHty...
  - (* T_App *)
    rewrite IHHty1. rewrite IHHty2.
    rewrite (eqb_ty_refl T2)...
  - (* T_True *) eauto.
  - (* T_False *) eauto.
  - (* T_If *) rewrite IHHty1. rewrite IHHty2.
    rewrite IHHty3. rewrite (eqb_ty_refl T1)...
Qed.