Typechecking

MoreStlc: A Typechecker for STLC

(* $Date: 2013-07-17 16:19:11 -0400 (Wed, 17 Jul 2013) $ *)

Require Export 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, tell us how to check whether or not a term is well typed.

Fortunately, the rules defining has_type are syntax directed — they exactly follow the shape of the term. 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.

Module STLCChecker.
Import STLC.

Comparing Types

First, we need a function to compare two types for equality...

Fixpoint beq_ty (T₁ T₂:ty) : bool :=
  match T₁,T₂ with
  | TBool, TBool =>
      true
  | TArrow T₁₁ T₁₂, TArrow T21 T22 =>
      andb (beq_ty T₁₁ T21) (beq_ty T₁₂ T22)
  | _,_ =>
      false
  end.

... and we need to establish the usual two-way connection between the boolean result returned by beq_ty and the logical proposition that its inputs are equal.

Lemma beq_ty_refl : ∀T₁,
  beq_ty T₁ T₁ = true.
Proof.
  intros T₁. induction T₁; simpl.
    reflexivity.
    rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed.

Lemma beq_ty__eq : ∀T₁ T₂,
  beq_ty T₁ T₂ = true → T₁ = T₂.
Proof with auto.
  intros T₁. induction T₁; intros T₂ Hbeq; destruct T₂; inversion Hbeq.
  Case "T₁=TBool".
    reflexivity.
  Case "T₁=TArrow T1_1 T1_2".
    apply andb_true in H0. inversion H0 as [Hbeq1 Hbeq2].
    apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed.

The Typechecker

Now here's the typechecker. It 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 tapp 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 TArrow T₁₁ T₁₂ for some T₁ and T₂).

Fixpoint type_check (Γ:context) (t:tm) : option ty :=
  match t with
  | tvar x => Γ x
  | tabs x T₁₁ t₁₂ => match type_check (extend Γ x T₁₁) t₁₂ with
                          | Some T₁₂ => Some (TArrow T₁₁ T₁₂)
                          | _ => None
                        end
  | tapp t₁ t₂ => match type_check Γ t₁, type_check Γ t₂ with
                      | Some (TArrow T₁₁ T₁₂),Some T₂ =>
                        if beq_ty T₁₁ T₂ then Some T₁₂ else None
                      | _,_ => None
                    end
  | ttrue => Some TBool
  | tfalse => Some TBool
  | tif x t f => match type_check Γ x with
                     | Some TBool =>
                       match type_check Γ t, type_check Γ f with
                         | Some T₁, Some T₂ =>
                           if beq_ty T₁ T₂ then Some T₁ else None
                         | _,_ => None
                       end
                     | _ => None
                   end
  end.

Properties

To verify that this typechecking algorithm is the correct one, 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 : ∀Γ t T,
  type_check Γ t = Some T → has_type Γ t T.
Proof with eauto.
  intros Γ t. generalize dependent Γ.
  t_cases (induction t) Case; intros Γ T Htc; inversion Htc.
  Case "tvar"...
  Case "tapp".
    remember (type_check Γ t₁) as TO1.
    remember (type_check Γ t₂) as TO2.
    destruct TO1 as [T₁|]; try solve by inversion;
    destruct T₁ as [|T₁₁ T₁₂]; try solve by inversion.
    destruct TO2 as [T₂|]; try solve by inversion.
    destruct (beq_ty T₁₁ T₂) eqn: Heqb;
    try solve by inversion.
    apply beq_ty__eq in Heqb.
    inversion H0; subst...
  Case "tabs".
    rename i into y. rename t into T₁.
    remember (extend Γ y T₁) as G'.
    remember (type_check G' t0) as TO2.
    destruct TO2; try solve by inversion.
    inversion H0; subst...
  Case "ttrue"...
  Case "tfalse"...
  Case "tif".
    remember (type_check Γ t₁) as TOc.
    remember (type_check Γ t₂) as TO1.
    remember (type_check Γ t₃) as TO2.
    destruct TOc as [Tc|]; try solve by inversion.
    destruct Tc; try solve by inversion.
    destruct TO1 as [T₁|]; try solve by inversion.
    destruct TO2 as [T₂|]; try solve by inversion.
    destruct (beq_ty T₁ T₂) eqn:Heqb;
    try solve by inversion.
    apply beq_ty__eq in Heqb.
    inversion H0. subst. subst...
Qed.

Theorem type_checking_complete : ∀Γ t T,
  has_type Γ t T → type_check Γ t = Some T.
Proof with auto.
  intros Γ t T Hty.
  has_type_cases (induction Hty) Case; simpl.
  Case "T_Var"...
  Case "T_Abs". rewrite IHHty...
  Case "T_App".
    rewrite IHHty1. rewrite IHHty2.
    rewrite (beq_ty_refl T₁₁)...
  Case "T_True"...
  Case "T_False"...
  Case "T_If". rewrite IHHty1. rewrite IHHty2.
    rewrite IHHty3. rewrite (beq_ty_refl T)...
Qed.

End STLCChecker.