Library PLF.Typechecking

Typechecking: A 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.

This short chapter constructs such a function and proves it correct.

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
Set Warnings "-non-recursive".
From Stdlib Require Import Bool.
From PLF Require Import Maps.
From PLF Require Import Smallstep.
From PLF Require Import Stlc.
From PLF Require MoreStlc.

Module STLCTypes.
Export STLC.

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.
  -
    reflexivity.
  -
    rewrite andb_true_iff in H0. inversion H0 as [Hbeq1 Hbeq2 ].
    apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed.
End STLCTypes.

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).

Module FirstTry.
Import STLCTypes.

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.

End FirstTry.

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.

Module STLCChecker.
Import STLCTypes.

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.

Exercises

In this exercise we'll extend the typechecker to deal with the extended features discussed in chapter MoreStlc. Your job is to fill in the omitted cases in the following.

Module TypecheckerExtensions.
Import MoreStlc.
Import STLCExtended.

Fixpoint eqb_ty (T1 T2 : ty ) : bool :=
  match T1 ,T2 with
  | <{{Nat }}>, <{{Nat }}> ⇒
      true
  | <{{Unit }}>, <{{Unit }}> ⇒
      true
  | <{{T11 → T12 }}>, <{{T21 → T22 }}> ⇒
      andb (eqb_ty T11 T21 ) (eqb_ty T12 T22 )
  | <{{T11 × T12 }}>, <{{T21 × T22 }}> ⇒
      andb (eqb_ty T11 T21 ) (eqb_ty T12 T22 )
  | <{{T11 + T12 }}>, <{{T21 + T22 }}> ⇒
      andb (eqb_ty T11 T21 ) (eqb_ty T12 T22 )
  | <{{List T11 }}>, <{{List T21 }}> ⇒
      eqb_ty T11 T21
  | _,_ ⇒
      false
  end.

Lemma eqb_ty_refl : ∀ T ,
  eqb_ty T T = true.
Proof.
  intros T.
  induction T ; simpl ; auto ;
    rewrite IHT1 ; rewrite IHT2 ; reflexivity. Qed.

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

☐

Just for fun, we'll do the soundness proof with just a bit more automation than above, using these "mega-tactics":

Ltac invert_typecheck Gamma t T :=
  remember (type_check Gamma t ) as TO ;
  destruct TO as [T |];
  try solve_by_invert ; try (inversion H0 ; eauto ); try (subst ; eauto ).

Ltac analyze T T1 T2 :=
  destruct T as [T1 T2 | |T1 T2 |T1 | |T1 T2 ]; try solve_by_invert.

Ltac fully_invert_typecheck Gamma t T T1 T2 :=
  let TX := fresh T in
  remember (type_check Gamma t ) as TO ;
  destruct TO as [TX |]; try solve_by_invert ;
  destruct TX as [T1 T2 | |T1 T2 |T1 | |T1 T2 ];
  try solve_by_invert ; try (inversion H0 ; eauto ); try (subst ; eauto ).

Ltac case_equality S T :=
  destruct (eqb_ty S T ) eqn : Heqb ;
  inversion H0 ; apply eqb_ty__eq in Heqb ; subst ; subst ; eauto.

Exercise: 2 stars, standard (ext_type_checking_sound)

☐

End TypecheckerExtensions.

Above, we showed how to write a typechecking function and prove it sound and complete for the typing relation. Do the same for the operational semantics -- i.e., write a function stepf of type tm → option tm and prove that it is sound and complete with respect to step from chapter MoreStlc.

Module StepFunction.
Import MoreStlc.
Import STLCExtended.

☐

Definition assert (b : bool ) (a : option tm ) : option tm :=
if b then a else None.

Exercise: 3 stars, standard, optional (stepf_defn)

Fixpoint stepf (t : tm ) : option tm :=
  match t with

  | tm_var x ⇒ None
  | <{ \x1 :T1 , t2 }> ⇒ None
  | <{ t1 t2 }> ⇒
    match stepf t1 , stepf t2 , t1 with
    | Some t1', _, _ ⇒ Some <{ t1' t2 }>

    | None , Some t2', _ ⇒ assert (valuef t1 ) (Some <{ t1 t2' }>)

    | None , None , <{ \x :T , t11 }> ⇒
      assert (valuef t2 ) (Some <{ [x :=t2 ]t11 }>)
    | _, _, _ ⇒ None
    end

  | tm_const _ ⇒ None
  | <{ succ t1 }> ⇒
    match stepf t1 , t1 with
    | Some t1', _ ⇒ Some <{ succ t1' }>

    | None , tm_const n ⇒ Some (tm_const (S n ))
    | None , _ ⇒ None
    end
  | <{ pred t1 }> ⇒
    match stepf t1 , t1 with
    | Some t1', _ ⇒ Some <{ pred t1' }>

    | None , tm_const n ⇒ Some (tm_const (n - 1))
    | _, _ ⇒ None
    end
  | <{ t1 × t2 }> ⇒
    match stepf t1 , stepf t2 , t1 , t2 with
    | Some t1', _, _, _ ⇒ Some <{ t1' × t2 }>

    | None , Some t2', _, _ ⇒
      assert (valuef t1 ) (Some <{ t1 × t2' }>)
    | None , None , tm_const n1 , tm_const n2 ⇒ Some (tm_const (mult n1 n2 ))
    | _, _, _, _ ⇒ None
    end
  | <{ if0 guard then t else f }> ⇒
    match stepf guard , guard with
    | Some guard', _ ⇒ Some <{ if0 guard' then t else f }>

    | None , tm_const 0 ⇒ Some t
    | None , tm_const (S _) ⇒ Some f
    | _, _ ⇒ None
    end





  | <{ case t0 of | nil ⇒ t1 | x21 :: x22 ⇒ t2 }> ⇒
    match stepf t0 , t0 with
    | Some t0', _ ⇒ Some <{ case t0' of | nil ⇒ t1 | x21 :: x22 ⇒ t2 }>

    | None , <{ nil T }> ⇒ Some t1
    | None , <{ vh :: vt }> ⇒
      assert (valuef vh ) (assert (valuef vt )
        (Some <{ [x22 :=vt ]([x21 :=vh]t2) }> ))
    | None, _ ⇒ None
    end








   | _ ⇒ None
  end.
Definition manual_grade_for_stepf_defn : option (nat ×string) := None.

☐

Exercise: 2 stars, standard, optional (sound_valuef)

Lemma sound_valuef : ∀ t,
valuef t = true → value t.
Proof.
Admitted.

☐

Exercise: 2 stars, standard, optional (complete_valuef)

Lemma complete_valuef : ∀ t,
value t → valuef t = true.
Proof.
Admitted.

☐

Tactic Notation "auto_stepf" ident(H) :=

  repeat
    match type of H with
    | (match ?u with _ ⇒ _ end = _) ⇒
      let e := fresh "e" in
      destruct u eqn:e
    | (assert ?u _ = _) ⇒

      let e := fresh "e" in
      destruct u eqn:e;
      simpl in H;
      [apply sound_valuef in e | discriminate]
    end;

  (discriminate + (inversion H; subst; auto)).

Exercise: 2 stars, standard, optional (sound_stepf)

Theorem sound_stepf : ∀ t t',
    stepf t = Some t' → t --> t'.
Proof.
  intros t.
  induction t; simpl; intros t' H;
    auto_stepf H.
Admitted.

☐

Exercise: 2 stars, standard, optional (value_stepf_nf)

Lemma value_stepf_nf : ∀ t,
value t → stepf t = None.
Proof.
Admitted.

☐

Exercise: 2 stars, standard, optional (complete_stepf)

Theorem complete_stepf : ∀ t t',
t --> t' → stepf t = Some t'.
Proof.
Admitted.

☐

End StepFunction.

Exercise: 5 stars, standard, optional (stlc_impl)

Using the Imp parser described in the ImpParser chapter of Logical Foundations as a guide, build a parser for extended STLC programs. Combine it with the typechecking and stepping functions from the above exercises to yield a complete typechecker and interpreter for this language.

Module StlcImpl.
Import StepFunction.

End StlcImpl.

☐