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.
This short chapter constructs such a function and proves it correct.

Comparing Types

First, we need a function to compare two types for equality...
... 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.

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

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:
Second, we define return and fail as synonyms for Some and None:
Now we can write the same type-checking function in a more imperative-looking style using these notations.

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.

Exercise: 4 stars, standard (type_check_defn)

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

Exercise: 2 stars, standard (ext_type_checking_sound)

Exercise: 2 stars, standard (ext_type_checking_complete)

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.

Exercise: 2 stars, standard, optional (valuef_defn)

(* We must first also redefine value as a function. *)
Fixpoint valuef (t : tm) : bool :=
  match t with
  | tm_var _ ⇒ false
  | <{ \_:_, _ }> ⇒ true
  | <{ _ _ }> ⇒ false
  | tm_const _ ⇒ true
  | <{ succ _ }> | <{ pred _ }> | <{ _ × _ }> | <{ if0 _ then _ else _ }> ⇒ false
  (* Complete the following cases *)
  (* sums *)
  (* FILL IN HERE *)
  | _ ⇒ false (* ... and delete this line when you complete the exercise. *)
  end.
(* Do not modify the following line: *)
Definition manual_grade_for_valuef_defn : option (nat×string) := None.
☐
(* A little helper to concisely check some boolean properties
   (in this case, that some term is a value, with valuef). *)
Definition assert (b : bool) (a : option tm) : option tm :=
  if b then a else None.

Exercise: 3 stars, standard, optional (stepf_defn)

(* Operational semantics as a Coq function. *)
Fixpoint stepf (t : tm) : option tm :=
  match t with
  (* pure STLC *)
  | tm_var x ⇒ None (* We only define step for closed terms *)
  | <{ \x1:T1, t2 }> ⇒ None (* Abstraction is a value *)
  | <{ t1 t2 }> ⇒
    match stepf t1, stepf t2, t1 with
    | Some t1', _, _ ⇒ Some <{ t1' t2 }>
    (* otherwise t1 is a normal form *)
    | None, Some t2', _ ⇒ assert (valuef t1) (Some <{ t1 t2' }>)
    (* otherwise t1, t2 are normal forms *)
    | None, None, <{ \x:T, t11 }> ⇒
      assert (valuef t2) (Some <{ [x:=t2]t11 }>)
    | _, _, _ ⇒ None
    end
  (* numbers *)
  | tm_const _ ⇒ None (* number value *)
  | <{ succ t1 }> ⇒
    match stepf t1, t1 with
    | Some t1', _ ⇒ Some <{ succ t1' }>
    (* otherwise t1 is a normal form *)
    | None, tm_const n ⇒ Some (tm_const (S n))
    | None, _ ⇒ None
    end
  | <{ pred t1 }> ⇒
    match stepf t1, t1 with
    | Some t1', _ ⇒ Some <{ pred t1' }>
    (* otherwise t1 is a normal form *)
    | 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 }>
    (* otherwise t1 is a normal form *)
    | 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 }>
    (* otherwise guard is a normal form *)
    | None, tm_const 0 ⇒ Some t
    | None, tm_const (S _) ⇒ Some f
    | _, _ ⇒ None
    end
  (* Complete the following cases. *)
  (* sums *)
  (* FILL IN HERE *)
  (* lists (the tm_lcase is given for free) *)
  (* FILL IN HERE *)
  | <{ case t0 of | nil ⇒ t1 | x21 :: x22 ⇒ t2 }> ⇒
    match stepf t0, t0 with
    | Some t0', _ ⇒ Some <{ case t0' of | nil ⇒ t1 | x21 :: x22 ⇒ t2 }>
    (* otherwise t0 is a normal form *)
    | None, <{ nil _ }> ⇒ Some t1
    | None, <{ vh :: vt }> ⇒
      assert (valuef vh) (assert (valuef vt)
        (Some <{ [x22:=vt]([x21:=vh]t2) }> ))
    | None, _ ⇒ None
    end
  (* unit *)
  (* FILL IN HERE *)
  (* pairs *)
  (* FILL IN HERE *)
  (* let *)
  (* FILL IN HERE *)
  (* fix *)
  (* FILL IN HERE *)
   | _ ⇒ None (* ... and delete this line when you complete the exercise. *)
  end.
(* Do not modify the following line: *)
Definition manual_grade_for_stepf_defn : option (nat×string) := None.
☐
(* To prove that stepf is equivalent to step, we start with
   a couple of intermediate lemmas. *)
(* We show that valuef is sound and complete with respect to value. *)

Exercise: 2 stars, standard, optional (sound_valuef)

(* valuef is sound with respect to value *)
Lemma sound_valuef : ∀ t,
    valuef t = true → value t.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, optional (complete_valuef)

(* valuef is complete with respect to value.
   This proof by induction is quite easily done by simplification. *)
Lemma complete_valuef : ∀ t,
    value t → valuef t = true.
Proof.
  (* FILL IN HERE *) Admitted.
☐
(* Soundness of stepf:

   Theorem sound_stepf : forall t t',
       stepf t = Some t'  ->  t --> t'.

   By induction on t. We automate the handling of each case with
   the following tactic auto_stepf. *)
Tactic Notation "auto_stepf" ident(H) :=
  (* Step 1: In every case, the left hand side of the hypothesis
     H : stepf t = Some t' simplifies to some combination of
     match u with ... end, assert u (...) (for some u).
     The tactic auto_stepf then destructs u as required.
     We repeat this step as long as it is possible. *)
  repeat
    match type of H with
    | (match ?u with _ ⇒ _ end = _) ⇒
      let e := fresh "e" in
      destruct u eqn:e
    | (assert ?u _ = _) ⇒
      (* In this case, u is always of the form valuef t0
         for some term t0. If valuef t0 = true, we immediately
         deduce value t0 via sound_valuef. If valuef t0 = false,
         then that equation simplifies to None = Some t', which is
         contradictory and can be eliminated with discriminate. *)
      let e := fresh "e" in
      destruct u eqn:e;
      simpl in H; (* assert true (...) must be simplified
                     explicitly. *)
      [apply sound_valuef in e | discriminate]
    end;
  (* Step 2: We are now left with either H : None = Some t' or
     Some (...) = Some t', and the rest of the proof is a
     straightforward combination of the induction hypotheses. *)
  (discriminate + (inversion H; subst; auto)).

Exercise: 2 stars, standard, optional (sound_stepf)

(* Soundness of stepf. *)
Theorem sound_stepf : ∀ t t',
    stepf t = Some t' → t --> t'.
Proof.
  intros t.
  induction t; simpl; intros t' H;
    auto_stepf H.
 (* The above proof script suffices for the reference solution. *)
 (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, optional (value_stepf_nf)

(* Now for completeness, another lemma will be useful:
   every value is a normal form for stepf. *)
Lemma value_stepf_nf : ∀ t,
    value t → stepf t = None.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard, optional (complete_stepf)

(* Completeness of stepf. *)
Theorem complete_stepf : ∀ t t',
    t --> t' → stepf t = Some t'.
Proof.
  (* FILL IN HERE *) 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.
(* FILL IN HERE *)
End StlcImpl.
☐
(* 2022-09-20 16:43 *)
+
Goals

Help
Messages