Library MoreTypes

Require Export Types.

Typechecking for STLC


The has_type relation defines what it means for a term to belong to a type (in some context). But it doesn't, in 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 (T1 T2:ty) {struct T1} : bool :=
  match T1,T2 with
  | ty_base i, ty_base i' =>
      beq_id i i'
  | ty_arrow T11 T12, ty_arrow T21 T22 =>
      andb (beq_ty T11 T21) (beq_ty T12 T22)
  | _,_ =>
      false
  end.

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

Lemma beq_ty_refl : forall T1,
  beq_ty T1 T1 = true.
Proof.
  intros T1. induction T1; simpl.
    apply sym_eq. apply beq_id_refl.
    rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed.

Lemma beq_ty__eq : forall T1 T2,
  beq_ty T1 T2 = true -> T1 = T2.
Proof with auto.
  intros T1. induction T1; intros T2 Hbeq; destruct T2; inversion Hbeq.
  Case "T1=ty_base i".
    apply sym_eq in H0. apply beq_id_eq in H0. subst...
  Case "T1=ty_arrow T1_1 T1_2".
    apply andb_true in H0. destruct 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 tm_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 ty_arrow T11 T12 for some T1 and T2).

Fixpoint type_check (Gamma:context) (t:tm) {struct t} : option ty :=
  match t with
  | tm_var i => Gamma i
  | tm_abs i T1 t1 => match type_check (extend Gamma i T1) t1 with
                        | Some T2 => Some (ty_arrow T1 T2)
                        | _ => None
                      end
  | tm_app t1 t2 => match type_check Gamma t1, type_check Gamma t2 with
                      | Some (ty_arrow T11 T12),Some T2 =>
                        if beq_ty T11 T2 then Some T12 else None
                      | _,_ => 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 : forall Gamma t T,
  type_check Gamma t = Some T -> has_type Gamma t T.
Proof with eauto.
  intros Gamma t. generalize dependent Gamma.
  (tm_cases (induction t) Case); intros Gamma T Htc; inversion Htc.
  Case "tm_var"...
  Case "tm_app".
    remember (type_check Gamma t1) as TO1.
    remember (type_check Gamma t2) as TO2.
    destruct TO1 as [T1|]; try solve by inversion;
    destruct T1 as [|T11 T12]; try solve by inversion.
    destruct TO2 as [T2|]; try solve by inversion.
    remember (beq_ty T11 T2) as b.
    destruct b; try solve by inversion.
    symmetry in Heqb. apply beq_ty__eq in Heqb.
    inversion H0; subst...
  Case "tm_abs".
    rename i into y. rename t into T1.
    remember (extend Gamma y T1) as G'.
    remember (type_check G' t0) as TO2.
    destruct TO2; try solve by inversion.
    inversion H0; subst...
Qed.

Theorem type_checking_complete : forall Gamma t T,
  has_type Gamma t T -> type_check Gamma t = Some T.
Proof with auto.
  intros Gamma t T Hty.
  (typing_cases (induction Hty) Case); simpl.
  Case "T_Var"...
  Case "T_Abs". rewrite IHHty...
  Case "T_App".
    rewrite IHHty1. rewrite IHHty2.
    rewrite (beq_ty_refl T1)...
Qed.

End STLCChecker.

Simple Extensions to STLC


let-bindings

When writing a complex expression, it is often useful---both for avoiding repetition and for increasing readability---to give names to some of its subexpressions. Most languages provide one or more ways of doing this. In OCaml, for example, we can write let x=t1 in t2 to mean ``evaluate the expression t1 and bind the name x to the resulting value while evaluating t2.''

Our let-binder follows ML's in choosing a call-by-value evaluation order, where the let-bound term must be fully evaluated before evaluation of the let-body can begin. The typing rule T_Let tells us that the type of a let can be calculated by calculating the type of the let-bound term, extending the context with a binding with this type, and in this enriched context calculating the type of the body, which is then the type of the whole let expression.

At this point in the course, it's probably just as easy to simply look at the rules defining this new feature as to wade through a lot of english text conveying the same information. Here they are:

Syntax: 
       t ::=                Terms:
           | x                 variable
           | \x:T. t           abstraction
           | t t               application
           | let x=t in t      let-binding
Reduction: 

                                 t1 ~~> t1'
                     ----------------------------------               (ST_Let1)
                     let x=t1 in t2 ~~> let x=t1' in t2

                        ----------------------------              (ST_LetValue)
                        let x=v1 in t2 ~~> [v1/x] t2
Typing: 
                Gamma |- t1 : T1      Gamma, x:T1 |- t2 : T2
                --------------------------------------------            (T_Let)
                        Gamma |- let x=t1 in t2 : T2

Pairs


Our functional programming examples have made frequent use of PAIRS of values. The type of such pairs is called a PRODUCT TYPE.

In Coq's functional language, the primitive way of extracting the components of a pair is PATTERN MATCHING. An alternative style is to take fst and snd -- the first- and second-projection operators -- as primitives. Just for fun (and for compatibility with the way we're going to do records just below), let's do our products this way.

Syntax: 
       t ::=                Terms:
           | ...
           | (t,t)             pair
           | t.fst             first projection
           | t.snd             second projection

       v ::=                Values:
           | \x:T.t
           | (v,v)             pair value

       T ::=                Types:
           | A                 base type
           | T -> T            arrow type
           | T * T             product type
Reduction: 
                                 t1 ~~> t1'
                            --------------------                     (ST_Pair1)
                            (t1,t2) ~~> (t1',t2)

                                 t2 ~~> t2'
                            --------------------                     (ST_Pair2)
                            (v1,t2) ~~> (v1,t2')

                                 t1 ~~> t1'
                             ------------------                       (ST_Fst1)
                             t1.fst ~~> t1'.fst

                             ------------------                    (ST_FstPair)
                             (v1,v2).fst ~~> v1

                                 t1 ~~> t1'
                             ------------------                       (ST_Snd1)
                             t1.snd ~~> t1'.snd

                             ------------------                    (ST_SndPair)
                             (v1,v2).snd ~~> v2
(Note the implicit convention that metavariables like v1 always denote values.)

Typing: 
                  Gamma |- t1 : T1       Gamma |- t2 : T2
                  ---------------------------------------              (T_Pair)
                          Gamma |- (t1,t2) : T1*T2

                            Gamma |- t1 : T1*T2
                            --------------------                        (T_Fst)
                            Gamma |- t1.fst : T1

                            Gamma |- t1 : T1*T2
                            --------------------                        (T_Snd)
                            Gamma |- t1.snd : T2

Records


Next, let's look at the generalization of products to RECORDS -- n-ary products with labeled fields.

Syntax: 
       t ::=                          Terms:
           | ...
           | {i1=t1, ..., in=tn}         record 
           | t.i                         projection

       v ::=                          Values:
           | ...
           | {i1=v1, ..., in=vn}         record value

       T ::=                          Types:
           | ...
           | {i1:T1, ..., in:Tn}         record type
Intuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "..." in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions. It is possible to devise informal notations that are more precise, but these tend to be quite heavy and to obscure the main points of the definitions. So we'll leave these a bit loose (they are informal anyway, after all) and do the work of tightening things up when the times comes to translate it all into Coq.

Reduction: 
                                 ti ~~> ti'                            (ST_Rcd)
    --------------------------------------------------------------------  
    {i1=v1, ..., im=vm, in=tn, ...} ~~> {i1=v1, ..., im=vm, in=tn', ...}

                                 t1 ~~> t1'
                               --------------                        (ST_Proj1)
                               t1.i ~~> t1'.i

                          -------------------------                (ST_ProjRcd)
                          {..., i=vi, ...}.i ~~> vi
Again, these rules are a bit informal. For example, the first rule is intended to be read "if ti is the leftmost field that is not a value and if ti steps to ti', then the whole record steps..." In the last rule, the intention is that there should only be one field called i, and that all the other fields must contain values.

Typing: 
               Gamma |- t1 : T1     ...     Gamma |- tn : Tn
             --------------------------------------------------         (T_Rcd)
             Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn}

                       Gamma |- t : {..., i:Ti, ...}
                       -----------------------------                   (T_Proj)
                             Gamma |- t.i : Ti

Lists


The typing features we have seen can be classified into BASE TYPES like Bool and Unit, and TYPE CONSTRUCTORS like -> and * that build new types from old ones. Another useful type constructor is list. For every type T, the type list T describes finite-length lists whose elements are drawn from T.

Below we give the syntax, semantics, and typing rules for lists. Except for the fact that explicit type annotations are mandatory on nil and cannot appear on cons, these lists are essentially identical to those we defined in Coq. We use case (a very simplified form of match) to destruct lists, to avoid dealing with questions like "what is the head of the empty list?"

While we say that cons v1 v2 is a value, we only mean that when v2 is also a list -- we'll have to enforce this in the formal definition of value.

Syntax: 
       t ::=                Terms:
           | nil T
           | cons t t
           | case t of 
                 nil -> t
               | x::x -> t

       v ::=                Values:
           | ...
           | nil T             nil value
           | cons v v          cons value

       T ::=                Types:
           | list T
           | ...
Reduction: 
                                 t1 ~~> t1'
                       --------------------------                    (ST_Cons1)
                       cons t1 t2 ~~> cons t1' t2

                                 t2 ~~> t2'
                       --------------------------                    (ST_Cons2)
                       cons v1 t2 ~~> cons v1 t2'

                                  t1 ~~> t1'                         (ST_Case1)
  ---------------------------------------------------------------------------- 
  (case t1 of nil -> t2 | h::t -> t3) ~~> (case t1' of nil -> t2 | h::t -> t3)

               ---------------------------------------------       (ST_CaseNil)
               (case nil T of nil -> t2 | h::t -> t3) ~~> t2

                                                                  (ST_CaseCons)
      ---------------------------------------------------------------  
      (case (cons vh vt) of nil -> t2 | h::t -> t3) ~~> [vh/h,vt/t]t3
Typing: 
                          -----------------------                       (T_Nil)
                          Gamma |- nil T : list T

                Gamma |- t1 : T      Gamma |- t2 : list T
                -----------------------------------------              (T_Cons)
                       Gamma |- cons t1 t2: list T

                Gamma |- t1 : list T1        Gamma |- t2 : T
                      Gamma, h:T1, t:list T1 |- t3 : T
              ------------------------------------------------         (T_Case)
              Gamma |- (case t1 of nil -> t2 | h::t -> t3) : T

General recursion


Another facility found in most programming languages (including Coq) is the ability to define recursive functions. For example, we might like to be able to define the factorial function like this: 
   fact = \x:nat. 
             if x=0 then 1 else x * (fact (pred x)))
But this would be require quite a bit of work to formalize: we'd have to introduce a notion of "function definitions" and carry around an "environment" of such definitions in the definition of the step relation.

Here is another way that is straightforward to formalize: instead of writing recursive definitions where the right-hand side can contain the identifier being defined, we can define a FIXED-POINT OPERATOR that performs the "unfolding" of the recursive definition in the right-hand side lazily during reduction. 
   fact = 
       fix
         (\f:nat->nat.
            \x:nat. 
               if x=0 then 1 else x * (f (pred x)))
The intuition is that the higher-order function f passed to fix is a GENERATOR for the fact function: if f is applied to a function that approximates the desired behavior of fact up to some number n (that is, a function that returns correct results on inputs less than or equal to n), then it returns a better approximation to fact---a function that returns correct results for inputs up to n+1. Applying fix to this generator returns its fixed point---a function that gives the desired behavior for all inputs n.

Syntax: 
       t ::=                Terms:
           | ...
           | fix t             fixed-point operator
Reduction: 
                                 t1 ~~> t1'
                             ------------------                       (ST_Fix1)
                             fix t1 ~~> fix t1'

                -------------------------------------------         (ST_FixAbs)
                fix (\x:T1.t2) ~~> [(fix(\x:T1.t2)) / x] t2
Typing: 
                            Gamma |- t1 : T1->T1
                            --------------------                        (T_Fix)
                            Gamma |- fix t1 : T1

Exercise: 1 star (halve_fix)

Translate this recursive definition into one using fix: 
   halve = 
     \x:nat. 
        if x=0 then 0 
        else if (pred x)=0 then 0
        else 1 + (halve (pred (pred x))))
FILL IN HERE...

Exercise: 1 star (fact_steps)

Write down the sequence of steps that the term fact 1 goes through to reduce to a normal form (assuming the usual reduction rules for arithmetic operations).

FILL IN HERE...

Formalizing the extensions


Exercise: 5 stars (STLC_extensions)

The rest of the file formalizes just the most interesting extension, records. Formalizing the others is left to you. We've provided the necessary extensions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly. (A good strategy is to work on the extensions one at a time, in multiple passes, rather than trying to work through the file from start to finish in a single pass.)

Module STLCExtended.

Syntax and operational semantics


The most obvious way to formalize the syntax of record types would be this:

Module FirstTry.

Definition alist (X : Set) := list (id * X).

Inductive ty : Set :=
  | ty_base : id -> ty
  | ty_arrow : ty -> ty -> ty
  | ty_rcd : (alist ty) -> ty.

Unfortunately, we encounter here a limitation in Coq: this type does not automatically give us the induction principle we expect -- the induction hypothesis in the ty_rcd case doesn't give us any information about the ty elements of the list, making it useless for the proofs we want to do.

(* Check ty_ind. *)
(* Yields:
    ty_ind : 
      forall P : ty -> Prop,
        (forall i : id, P (ty_base i)) ->
        (forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) ->
        (forall a : alist ty, P (ty_rcd a)) -> forall t : ty, P t   *)

End FirstTry.

It is possible to get a better induction principle out of Coq, but the details of how this is done are not very pretty, and it is not as intuitive to use as the ones Coq generates automatically for simple Inductive definitions.

Fortunately, there is a different way of formalizing records that is, in some ways, even simpler and more natural: instead of using the existing list type, we can essentially include its constructors ("nil" and "cons") in the syntax of types.

(Since this is the final definition that we'll use for the rest of the chapter, we also include constructors for and pairs lists and a base type of numbers.)

Inductive ty : Set :=
  (* proper types *)
  | ty_base : id -> ty
  | ty_arrow : ty -> ty -> ty
  | ty_rcd : ty -> ty
  | ty_pair : ty -> ty -> ty
  | ty_list : ty -> ty
  | ty_nat : ty
  (* rows of types *)
  | tyr_nil : ty
  | tyr_cons : id -> ty -> ty -> ty.

Although the two are given in the same definition, we will make a clean intuitive distinction between "proper types" and "rows of types" whenever we use them. (For the sake of streamlining the development in this chapter, we won't actually bother to add enough side conditions here to exclude programs that confuse the distinction. In the next chapter we'll be more careful about this.)

Tactic Notation "ty_cases" tactic(first) tactic(c) :=
  first;
  [ c "ty_base" | c "ty_arrow" | c "ty_rcd" |
    c "ty_pair" | c "ty_list" | c "ty_nat" |
    c "tyr_nil" | c "tyr_cons" ].

Similarly, at the level of terms, we have constructors tmr_nil -- the empty record -- and tmr_cons, which adds a single field to the front of a list of fields.

Inductive tm : Set :=
  (* Proper terms *)
  | tm_var : id -> tm
  | tm_app : tm -> tm -> tm
  | tm_abs : id -> ty -> tm -> tm
  | tm_proj : tm -> id -> tm
    (* records *)
  | tm_rcd : tm -> tm
    (* pairs *)
  | tm_pair : tm -> tm -> tm
  | tm_fst : tm -> tm
  | tm_snd : tm -> tm
    (* lists *)
  | tm_nil : ty -> tm
  | tm_cons : tm -> tm -> tm
  | tm_case : tm -> tm -> id -> id -> tm -> tm
          (* i.e., case t1 of | nil -> t2 | x::y -> t3 *)
    (* numbers *)
  | tm_nat : nat -> tm
  | tm_succ : tm -> tm
  | tm_pred : tm -> tm
  | tm_mult : tm -> tm -> tm
  | tm_if0 : tm -> tm -> tm -> tm
    (* let *)
  | tm_let : id -> tm -> tm -> tm
          (* i.e., let x = t1 in t2 *)
    (* fix *)
  | tm_fix : tm -> tm

  (* rows of terms *)
  | tmr_nil : tm
  | tmr_cons : id -> tm -> tm -> tm.

Tactic Notation "tm_cases" tactic(first) tactic(c) :=
  first;
  [ c "tm_var" | c "tm_app" | c "tm_abs" |
    c "tm_proj" | c "tm_rcd" |
    c "tm_pair" | c "tm_fst" | c "tm_snd" |
    c "tm_nil" | c "tm_cons" | c "tm_case" |
    c "tm_nat" | c "tm_succ" | c "tm_pred" | c "tm_mult" | c "tm_if0" |
    c "tm_let" |
    c "tm_fix" |
    c "tmr_nil" | c "tmr_cons" ].

(* Some variables, for examples... *)
Notation x := (Loc 0).
Notation f := (Loc 1).
Notation g := (Loc 2).
Notation l := (Loc 3).
Notation A := (Loc 4).
Notation B := (Loc 5).
Notation k := (Loc 6).
Notation i1 := (Loc 7).
Notation i2 := (Loc 8).

(* { i1:A } *)
Check ty_rcd (tyr_cons i1 (ty_base A) tyr_nil).

(* { i1:A->B, i2:A } *)
Check ty_rcd (tyr_cons i1 (ty_arrow (ty_base A) (ty_base B))
             (tyr_cons i2 (ty_base A)
              tyr_nil)).

Substitution


Fixpoint subst (x:id) (s:tm) (t:tm) {struct t} : tm :=
  match t with
  | tm_var y => if beq_id x y then s else t
  | tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1))
  | tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)
  | tm_proj t1 i => tm_proj (subst x s t1) i
  | tm_rcd tr => tm_rcd (subst x s tr)
  | tmr_nil => tmr_nil
  | tmr_cons i t1 tr1 => tmr_cons i (subst x s t1) (subst x s tr1)
  (* FILL IN HERE *)
  | _ => t (* ... and delete this line *)
  end.

Reduction


A record is a value if all of its fields are:

Inductive value : tm -> Prop :=
  | v_abs : forall x T11 t12,
      value (tm_abs x T11 t12)
  | v_rcd : forall vr,
      value vr ->
      value (tm_rcd vr)
  (* FILL IN HERE *)
  | v_nil : value tmr_nil
  | v_cons : forall i v1 vr,
      value v1 ->
      value vr ->
      value (tmr_cons i v1 vr).

Hint Constructors value.

Utility functions for extracting one field from a row of types or terms:

Fixpoint tyr_lookup (i:id) (Tr:ty) {struct Tr} : option ty :=
  match Tr with
  | tyr_cons i' Ti Tr' => if beq_id i i' then Some Ti else tyr_lookup i Tr'
  | _ => None
  end.

Fixpoint tmr_lookup (i:id) (tr:tm) {struct tr} : option tm :=
  match tr with
  | tmr_cons i' ti tr' => if beq_id i i' then Some ti else tmr_lookup i tr'
  | _ => None
  end.

The step function uses the term-level lookup function (for the projection rule), while the type-level lookup is needed for has_type.

Reserved Notation "t1 '~~>' t2" (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T11 t12 v2,
         value v2
      -> (tm_app (tm_abs x T11 t12) v2) ~~> (subst x v2 t12)
  | ST_App1 : forall t1 t1' t2,
         t1 ~~> t1'
      -> (tm_app t1 t2) ~~> (tm_app t1' t2)
  | ST_App2 : forall v1 t2 t2',
         value v1
      -> t2 ~~> t2'
      -> (tm_app v1 t2) ~~> (tm_app v1 t2')
  | ST_Proj1 : forall t1 t1' i,
        t1 ~~> t1'
     -> (tm_proj t1 i) ~~> (tm_proj t1' i)
  | ST_ProjRcd : forall tr1 i vi,
        value (tm_rcd tr1)
     -> tmr_lookup i tr1 = Some vi
     -> (tm_proj (tm_rcd tr1) i) ~~> vi
  | ST_Rcd : forall tr tr',
         tr ~~> tr'
      -> (tm_rcd tr) ~~> (tm_rcd tr')
  (* FILL IN HERE *)
  | ST_Rcd_Head : forall i t1 t1' tr2,
        t1 ~~> t1'
     -> (tmr_cons i t1 tr2) ~~> (tmr_cons i t1' tr2)
  | ST_Rcd_Tail : forall i v1 tr2 tr2',
        value v1
     -> tr2 ~~> tr2'
     -> (tmr_cons i v1 tr2) ~~> (tmr_cons i v1 tr2')

where "t1 '~~>' t2" := (step t1 t2).

Note: From now on, the rules of the step relation will be called ST_Foo rather than S_Foo (reserving S_ as the prefix for subtyping rules in the next chapter).

Tactic Notation "step_cases" tactic(first) tactic(c) :=
  first;
  [ c "ST_AppAbs" | c "ST_App1" | c "ST_App2" |
    c "ST_Proj1" | c "ST_ProjRcd" | c "ST_Rcd" |
    (* FILL IN HERE *)
    c "ST_Rcd_Head" | c "ST_Rcd_Tail" ].

Notation stepmany := (refl_step_closure step).
Notation "t1 '~~>*' t2" := (stepmany t1 t2) (at level 40).

Hint Constructors step.

Typing


(* Standard definitions for contexts *)
Definition context := id -> (option ty).
Definition empty : context := (fun _ => None).
Definition extend (Gamma : context) (x:id) (T : ty) :=
  fun x' => if beq_id x x' then Some T else Gamma x'.

Generalizing our abstract syntax from records (from lists to the nil/cons presentation) introduces the possibility of writing strange terms like this...

Definition weird_term := tm_rcd (tm_nat 5).

where the "tail" of a record value is not actually a record value!

As we remarked above, we are not actually going to spend much energy excluding such "monster terms." We will exclude this one, but there will be others -- like tm_rcd (tmr_cons x tmr_nil tmr_nil) -- that will be allowed by the typing rules. However, the presence of such terms in the language is more a curiosity than a real problem: in particular, we will still be able to prove the standard progress and preservation properties.

Inductive is_tmr : tm -> Prop :=
  | is_tmr_nil :
      is_tmr tmr_nil
  | is_tmr_cons : forall i t1 tr2,
      is_tmr tr2 ->
      is_tmr (tmr_cons i t1 tr2).

Hint Constructors is_tmr.

Inductive has_type : context -> tm -> ty -> Prop :=
  (* Typing rules for proper terms *)
  | T_Var : forall Gamma x T1,
      Gamma x = Some T1 ->
      has_type Gamma (tm_var x) T1
  | T_Abs : forall Gamma x T11 T12 t12,
      has_type (extend Gamma x T11) t12 T12 ->
      has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12)
  | T_App : forall T1 T2 Gamma t1 t2,
      has_type Gamma t1 (ty_arrow T1 T2) ->
      has_type Gamma t2 T1 ->
      has_type Gamma (tm_app t1 t2) T2
  | T_Proj : forall Gamma i t1 Ti Tr,
      has_type Gamma t1 (ty_rcd Tr) ->
      tyr_lookup i Tr = Some Ti ->
      has_type Gamma (tm_proj t1 i) Ti
  | T_Rcd : forall Gamma tr1 Tr1,
      is_tmr tr1 ->
      has_type Gamma tr1 Tr1 ->
      has_type Gamma (tm_rcd tr1) (ty_rcd Tr1)
  (* FILL IN HERE *)
  (* Typing rules for rows of terms *)
  | TR_Nil : forall Gamma,
      has_type Gamma tmr_nil tyr_nil
  | TR_Cons : forall Gamma i ti Ti tr1 Tr1,
      has_type Gamma ti Ti ->
      has_type Gamma tr1 Tr1 ->
      has_type Gamma (tmr_cons i ti tr1) (tyr_cons i Ti Tr1).

Hint Constructors has_type.

Tactic Notation "has_type_cases" tactic(first) tactic(c) :=
  first;
  [ c "T_Var" | c "T_Abs" | c "T_App" | c "T_Proj" | c "T_Rcd" |
    (* FILL IN HERE *)
    c "TR_Nil" | c "TR_Cons"
].

Examples


Exercise: 2 stars (examples)


(* fact := 
       fix
         (\f:nat->nat.
            \x:nat. 
               if x=0 then 1 else x * (f (pred x)))    *) 
Definition fact :=
  tm_fix
    (tm_abs f (ty_arrow ty_nat ty_nat)
      (tm_abs x ty_nat
        (tm_if0 
           (tm_var x) 
           (tm_nat 1) 
           (tm_mult 
              (tm_var x) 
              (tm_app (tm_var f) (tm_pred (tm_var x))))))).

(* Note that you may be able to type check fact but still have some
   rules wrong! *)
Example fact_typechecks :
  has_type empty fact (ty_arrow ty_nat ty_nat).
Proof with auto.
(* FILL IN HERE *)

Example fact_example: 
  (tm_app fact (tm_nat 1)) ~~>* (tm_nat 1).
Proof.
  (* Remove the enclosing comments and finish the proof *)
  (* FILL IN HERE *)


(* map :=
     \g:nat->nat.
       fix
         (\f:[nat]->[nat].
            \l:[nat]. 
               case l of
               | [] -> []
               | x::l -> (g x)::(f l)) *) 
Definition map :=
  tm_abs g (ty_arrow ty_nat ty_nat)
    (tm_fix
      (tm_abs f (ty_arrow (ty_list ty_nat) (ty_list ty_nat))
        (tm_abs l (ty_list ty_nat)
          (tm_case (tm_var l)
            (tm_nil ty_nat) 
            x l (tm_cons (tm_app (tm_var g) (tm_var x)) 
                         (tm_app (tm_var f) (tm_var l))))))).

Example map_typechecks :
  has_type empty map 
    (ty_arrow (ty_arrow ty_nat ty_nat)
      (ty_arrow (ty_list ty_nat) 
        (ty_list ty_nat))).
Proof with auto.
  (* Remove the enclosing comments and finish the proof *)
  (* FILL IN HERE *)

Example map_example :
  tm_app (tm_app map (tm_abs x ty_nat (tm_succ (tm_var x))))
         (tm_cons (tm_nat 1) (tm_cons (tm_nat 2) (tm_nil ty_nat)))
  ~~>* (tm_cons (tm_nat 2) (tm_cons (tm_nat 3) (tm_nil ty_nat))).
Proof with auto.
  (* Remove the enclosing comments and finish the proof *)
  (* FILL IN HERE *)
Example typing_example : forall y,
  has_type (extend empty y (ty_base A))
         (tm_app (tm_abs x (ty_rcd (tyr_cons k (ty_base A) tyr_nil))
                           (tm_proj (tm_var x) k))
                 (tm_rcd (tmr_cons k (tm_var y) tmr_nil)))
         (ty_base A).
Proof.
  intros y.
  apply T_App with (T1:=ty_rcd (tyr_cons k (ty_base A) tyr_nil)).
    apply T_Abs. apply T_Proj with (tyr_cons k (ty_base A) tyr_nil).
      apply T_Var. reflexivity.
      reflexivity.
    apply T_Rcd; try auto.
      apply TR_Cons.
        apply T_Var. unfold extend. rewrite <- beq_id_refl. reflexivity.
        apply TR_Nil. Qed.

Lemma typing_example_2 :
  has_type empty
    (tm_app (tm_abs x (ty_rcd (tyr_cons i1 (ty_arrow (ty_base A) (ty_base A))
                              (tyr_cons i2 (ty_arrow (ty_base B) (ty_base B))
                               tyr_nil)))
              (tm_proj (tm_var x) i2))
            (tm_rcd (tmr_cons i1 (tm_abs x (ty_base A) (tm_var x))
                    (tmr_cons i2 (tm_abs x (ty_base B) (tm_var x))
                     tmr_nil))))
    (ty_arrow (ty_base B) (ty_base B)).
Proof.
  (* Feel free to use Coq's automation features in this proof.
     However, if you are not confident about how the type system
     works, you may want to carry out the proof first using the basic
     features (apply instead of eapply, in particular) and then
     perhaps compress it using automation. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Example typing_nonexample :
  ~ exists T,
      has_type (extend empty x (ty_rcd (tyr_cons i2 (ty_arrow (ty_base A) (ty_base A))
                                        tyr_nil)))
               (tm_rcd (tmr_cons i1 (tm_abs x (ty_base B) (tm_var x)) (tm_var x)))
               T.
Proof.
  (* Before starting to prove this fact (or the one above!), make sure
     you understand what it is saying. *)
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Example typing_nonexample_2 : forall y,
  ~ exists T,
    has_type (extend empty y (ty_base A))
           (tm_app (tm_abs x (ty_rcd (tyr_cons i1 (ty_base A) tyr_nil))
                     (tm_proj (tm_var x) i1))
                   (tm_rcd (tmr_cons i1 (tm_var y) (tmr_cons i2 (tm_var y) tmr_nil))))
           T.
Proof.
  (* FILL IN HERE (and delete "Admitted") *) Admitted.

Progress and Preservation


The proofs of progress and preservation for this system are essentially the same (though of course somewhat longer!) as for the pure simply typed lambda-calculus. The main change is the addition of some technical lemmas involving rows.

Lemma rcd_fields_match : forall Gamma tr Tr i Ti,
  has_type Gamma (tm_rcd tr) (ty_rcd Tr) ->
  tyr_lookup i Tr = Some Ti ->
  exists ti, tmr_lookup i tr = Some ti.
(* Lemma: If Gamma |- {tr} : {Tr} and tyr_lookup i Tr returns
   Some Ti, then tmr_lookup i tr returns Some ti for some term ti. *)
Proof with eauto.
  (* Proof: By induction on the structure of the type row Tr.  The
     case where Tr = tyr_nil is immediate (since then the assumption
     that tyr_lookup i Tr = Some Ti is contradictory). *)
  intros Gamma tr Tr i Ti Htyp Hget.
  generalize dependent tr.
  (ty_cases (induction Tr) Case); try (solve by inversion)...
  Case "tyr_cons".
    (* If Tr = tyr_cons i0 Tr1 Tr2, then the last two steps in the
       typing derivation must be T_Rcd preceeded by TR_Cons, which
       means that tr = tmr_cons i0 ti1 tr1 for some ti1 and tr1 *)
    intros tr Htyp. inversion Htyp; subst. clear Htyp.
    inversion H3; subst; try (solve by inversion). clear H3.
    (* This leaves two possiblities to consider - either i0 = i or not *)
    simpl in Hget. remember (beq_id i i0) as beq. destruct beq.
    SCase "get head".
      (* If i = i0, then tyr_lookup i Tr = Some T1.  But then
         tmr_lookup i tr = Some t1, and we are done. *)
      apply beq_id_eq in Heqbeq. subst. inversion Hget. subst. clear Hget.
      exists ti. simpl. rewrite <- beq_id_refl...
    SCase "get tail".
      (* On the other hand, suppose i <> i0.  Then 
         tyr_lookup i Tr = tyr_lookup i Tr2 and 
         tmr_lookup i tr = tmr_lookup i tr1,
         and the result follows from the induction hypothesis. *)
      apply IHTr2 with (tr := tr1) in Hget...
      destruct Hget as [ti' Hget]. exists ti'. simpl.
      rewrite <- Heqbeq...
      apply T_Rcd... inversion H2... Qed.

Theorem progress : forall t T,
     has_type empty t T
  -> value t \/ exists t', t ~~> t'.
Proof with eauto.
  (* THEOREM: Suppose empty |- t : T.  Then either
       1. t is a value, or
       2. t ~~> t' for some t'.
     Proof: By induction on the given typing derivation. *)
  intros t T Ht.
  remember empty as Gamma.
  generalize dependent HeqGamma.
  (has_type_cases (induction Ht) Case); intros HeqGamma; subst.
  Case "T_Var".
    (* The final rule in the given typing derivation cannot be T_Var,
       since it can never be the case that empty |- x : T (since the
       context is empty). *)
    inversion H.
  Case "T_Abs".
    (* If the T_Abs rule was the last used, then t = tm_abs x T11 t12,
       which is a value. *)
    left...
  Case "T_App".
    (* If the last rule applied was T_App, then t = t1 t2, and we know 
       from the form of the rule that
         empty |- t1 : T1 -> T2
         empty |- t2 : T1
       By the induction hypothesis, each of t1 and t2 either is a value 
       or can take a step. *)
    right.
    destruct IHHt1; subst...
    SCase "t1 is a value".
      destruct IHHt2; subst...
      SSCase "t2 is a value".
      (* If both t1 and t2 are values, then we know that 
         t1 = tm_abs x T11 t12, since abstractions are the only values
         that can have an arrow type.  But 
         (tm_abs x T11 t12) t2 ~~> subst x t2 t12 by ST_AppAbs. *)
        inversion H; subst; try (solve by inversion).
        exists (subst x t2 t12)...
      SSCase "t2 steps".
        (* If t1 is a value and t2 ~~> t2', then t1 t2 ~~> t1 t2' 
           by ST_App2. *)
        destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')...
    SCase "t1 steps".
      (* Finally, If t1 ~~> t1', then t1 t2 ~~> t1' t2 by ST_App1. *)
      destruct H as [t1' Hstp]. exists (tm_app t1' t2)...
  Case "T_Proj".
    (* If the last rule in the given derivation is T_Proj, then 
       t = tm_proj t i and
           empty |- t : (ty_rcd Tr)
       By the IH, t either is a value or takes a step. *)
    right. destruct IHHt...
    SCase "rcd is value".
      (* If t is a value, then from the typing rules we can see that
         it must have the form of a record, and that 
         tyr_lookup i Tr = Some T.  By Lemma rcd_fields_match, this 
         means that tmr_lookup i t = ti for some term ti.  
         ST_ProjRcd gives us tm_proj (tm_rcd t) i ~~> ti. *)
      inversion H0; subst; try (solve by inversion).
      inversion Ht; subst.
      destruct (rcd_fields_match _ _ _ _ _ Ht H) as [ti Hget].
      exists ti...
    SCase "rcd_steps".
      (* On the other hand, if t ~~> t', then tm_proj t i ~~> tm_proj t' i
         by ST_Proj1. *)
      destruct H0 as [t' Hstp]. exists (tm_proj t' i)...
  Case "T_Rcd".
    (* If the last rule in the given derivation is T_Rcd, then 
       t = tm_rcd tr1, where tr1 is a valid record body, and
          empty |- tr1 : Tr1
       for some Tr1.  By the IH, we know that tr either is a value
       or takes a step. *)
    destruct IHHt; try reflexivity.
    SCase "tr is a value".
      (* If tr1 is a value, then so is tm_rcd tr1. *)
      left...
    SCase "tr steps".
      (* If tr1 ~~> tr1', then tm_rcd tr1 ~~> tm_rcd tr1' by ST_Rcd. *)
      right. destruct H0 as [tr1' Hstp]. exists (tm_rcd tr1')...
  (* FILL IN HERE *)
  Case "TR_Nil".
    (* If the last rule in the given derivation is TR_Nil, then 
       t = tmr_nil, which is a value. *)
    left...
  Case "TR_Cons".
    (* If the last rule is TR_Cons, then t = tmr_cons i ti tr1 and
         empty |- ti : Ti
         empty |- tr1 : Tr1
       By the IH, each of ti and tr1 either is a value or can take
       a step. *)
    destruct IHHt1...
    SCase "head is a value".
      destruct IHHt2; try reflexivity.
      SSCase "tail is a value".
      (* If ti and tr1 are both values, then tmr_cons i ti tr1
         is a value as well. *)
        left...
      SSCase "tail steps".
        (* If ti is a value and tr1 ~~> tr1', then 
           tmr_cons i ti tr1 ~~> tmr_cons i ti tr1' by 
           ST_Rcd_Tail. *)
        right. destruct H0 as [tr1' Hstp].
        exists (tmr_cons i ti tr1')...
    SCase "head steps".
      (* If ti ~~> ti', then 
         tmr_cons i ti tr1 ~~> tmr_cons i ti' tr1 
         by ST_Rcd_Head. *)
      right. destruct H as [ti' Hstp].
      exists (tmr_cons i ti' tr1)... Qed.

Inductive appears_free_in : id -> tm -> Prop :=
  | afi_var : forall x,
      appears_free_in x (tm_var x)
  | afi_app1 : forall x t1 t2,
      appears_free_in x t1 -> appears_free_in x (tm_app t1 t2)
  | afi_app2 : forall x t1 t2,
      appears_free_in x t2 -> appears_free_in x (tm_app t1 t2)
  | afi_abs : forall x y T11 t12,
        y <> x
     -> appears_free_in x t12
     -> appears_free_in x (tm_abs y T11 t12)
  | afi_proj : forall x t1 i,
     appears_free_in x t1 ->
     appears_free_in x (tm_proj t1 i)
  | afi_rcd : forall x tr1,
     appears_free_in x tr1 ->
     appears_free_in x (tm_rcd tr1)
  (* FILL IN HERE *)
  (* rows *)
  | afir_head : forall x i ti tr1,
      appears_free_in x ti ->
      appears_free_in x (tmr_cons i ti tr1)
  | afir_tail : forall x i ti tr1,
      appears_free_in x tr1 ->
      appears_free_in x (tmr_cons i ti tr1).

Hint Constructors appears_free_in.
Lemma context_invariance : forall Gamma Gamma' t S,
     has_type Gamma t S
  -> (forall x, appears_free_in x t -> Gamma x = Gamma' x)
  -> has_type Gamma' t S.
Proof with eauto.
  intros. generalize dependent Gamma'.
  (has_type_cases (induction H) Case);
    intros Gamma' Heqv...
  Case "T_Var".
    apply T_Var. rewrite <- Heqv...
  Case "T_Abs".
    apply T_Abs. apply IHhas_type. intros y Hafi.
    unfold extend. remember (beq_id x y) as e.
    destruct e...
  Case "T_App".
    apply T_App with T1...
  (* FILL IN HERE *)
  Case "TR_Cons".
    apply TR_Cons... Qed.

Lemma free_in_context : forall x t T Gamma,
   appears_free_in x t ->
   has_type Gamma t T ->
   exists T', Gamma x = Some T'.
Proof with eauto.
  intros x t T Gamma Hafi Htyp.
  (has_type_cases (induction Htyp) Case); inversion Hafi; subst...

  Case "T_Var".
    exists T1...
  Case "T_Abs".
    destruct IHHtyp as [T' Hctx]... exists T'.
    unfold extend in Hctx.
    apply not_eq_false_beqid in H2. rewrite <- H2 in Hctx...
  (* FILL IN HERE *)
Qed.

Lemma substitution_preserves_tmr : forall x v tr,
     is_tmr tr
  -> is_tmr (subst x v tr).
Proof.
  intros x v tr H. induction H.
  Case "is_tmr_nil".
    apply is_tmr_nil.
  Case "is_tmr_cons".
    simpl. apply is_tmr_cons. assumption. Qed.

Lemma step_preserves_tmr : forall tr tr',
     is_tmr tr
  -> tr ~~> tr'
  -> is_tmr tr'.
Proof.
  intros tr tr' Hirb Hs.
  (step_cases (induction Hs) Case); try (solve by inversion).
  Case "ST_Rcd_Head".
    inversion Hirb. subst.
    apply is_tmr_cons. assumption.
  Case "ST_Rcd_Tail".
    inversion Hirb. subst.
    apply is_tmr_cons. apply IHHs. assumption. Qed.

Lemma substitution_preserves_typing : forall Gamma x U v t S,
     has_type (extend Gamma x U) t S
  -> has_type empty v U
  -> has_type Gamma (subst x v t) S.
Proof with eauto.
  (* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then 
     Gamma |- (subst x v t) S. *)
  intros Gamma x U v t S Ht Hv.
  generalize dependent Gamma. generalize dependent S.
  (* Proof: By induction on the term t.  Most cases follow directly
     from the IH, with the exception of tm_var, tm_abs, and tm_rcd.
     The former aren't automatic because we must reason about how the
     variables interact.  tm_rcd isn't automatic because we must
     appeal to a separate lemma (proven above) about records. *)
  (tm_cases (induction t) Case);
    intros S Gamma Htyp; simpl; inversion Htyp; subst...
  Case "tm_var".
    simpl. rename i into y.
    (* If t = y, we know that
         empty |- v : U and
         Gamma,x:U |- y : S
       and, by inversion, extend Gamma x U y = Some S.  We want to
       show that Gamma |- subst x v y : S.

       There are two cases to consider: either x=y or x<>y. *)
    remember (beq_id x y) as e. destruct e.
    SCase "x=y".
    (* If x = y, then we know that U = S, and that subst x v y = v.
       So what we really must show is that if empty |- v : U then
       Gamma |- v : U.  We have already proven a more general version
       of this theorem, called context invariance. *)
      apply beq_id_eq in Heqe. subst.
      unfold extend in H1. rewrite <- beq_id_refl in H1.
      inversion H1; subst. clear H1.
      eapply context_invariance...
      intros x Hcontra.
      destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
      inversion HT'.
    SCase "x<>y".
    (* If x <> y, then Gamma y = Some S and the substitution has no
       effect.  We can show that Gamma |- y : S by T_Var. *)
      apply T_Var. unfold extend in H1. rewrite <- Heqe in H1...
  Case "tm_abs".
    rename i into y. rename t into T11.
    (* If t = tm_abs y T11 t0, then we know that
         Gamma,x:U |- tm_abs y T11 t0 : T11->T12
         Gamma,x:U,y:T11 |- t0 : T12
         empty |- v : U
       As our IH, we know that forall S Gamma, 
         Gamma,x:U |- t0 : S -> Gamma |- subst x v t0 S.
    
       We can calculate that 
         subst x v t = tm_abs y T11 (if beq_id x y
                                      then t0 
                                      else subst x v t0)
       And we must show that Gamma |- subst x v t : T11->T12.  We know
       we will do so using T_Abs, so it remains to be shown that:
         Gamma,y:T11 |- if beq_id x y then t0 else subst x v t0 : T12
       We consider two cases: x = y and x <> y.
    *)
    apply T_Abs.
    remember (beq_id x y) as e. destruct e.
    SCase "x=y".
    (* If x = y, then the substitution has no effect.  Context
       invariance shows that Gamma,y:U,y:T11 and Gamma,y:T11 are
       equivalent.  Since the former context shows that t0 : T12, so
       does the latter. *)
      eapply context_invariance...
      apply beq_id_eq in Heqe. subst.
      intros x Hafi. unfold extend.
      destruct (beq_id y x)...
    SCase "x<>y".
    (* If x <> y, then the IH and context invariance allow us to show that
         Gamma,x:U,y:T11 |- t0 : T12       =>
         Gamma,y:T11,x:U |- t0 : T12       =>
         Gamma,y:T11 |- subst x v t0 : T12 *)
      apply IHt. eapply context_invariance...
      intros z Hafi. unfold extend.
      remember (beq_id y z) as e0. destruct e0...
      apply beq_id_eq in Heqe0. subst.
      rewrite <- Heqe...
  Case "tm_rcd".
    (* If t is a record, the result follows by the IH and
       Lemma substitution_preserves_tmr. *)
    apply T_Rcd.
    apply substitution_preserves_tmr...
    apply IHt...
  (* FILL IN HERE *)
Qed.

Lemma rcd_types_match : forall Gamma tr Tr i ti Ti,
  has_type Gamma (tm_rcd tr) (ty_rcd Tr) ->
  tyr_lookup i Tr = Some Ti ->
  tmr_lookup i tr = Some ti ->
  has_type Gamma ti Ti.
Proof with eauto.
  intros Gamma tr Tr i ti Ti Htyp.
  generalize dependent tr.
  (ty_cases (induction Tr) Case);
    intros tr Htyp Htyget Htmget;
    try (solve by inversion)...
  Case "tyr_cons".
    inversion Htyp; subst. clear Htyp.
    inversion H3; subst; try (solve by inversion). clear H3.
    simpl in Htyget. remember (beq_id i i0) as beq. destruct beq.
    SCase "get head".
      apply beq_id_eq in Heqbeq. subst.
      inversion Htyget. subst.
      inversion Htmget. rewrite <- beq_id_refl in H0.
      inversion H0. subst...
    SCase "get tail".
      simpl in Htmget.
      rewrite <- Heqbeq in Htmget.
      apply (IHTr2 tr1)...
      apply T_Rcd...
      inversion H2... Qed.

Theorem preservation : forall t t' T,
     has_type empty t T
  -> t ~~> t'
  -> has_type empty t' T.
Proof with eauto.
  intros t t' T HT.
  (* Theorem: If empty |- t : T and t ~~> t', then empty |- t' : T. *)
  remember empty as Gamma. generalize dependent HeqGamma.
  generalize dependent t'.
  (* Proof: By induction on the given typing derivation.  Many cases are
     contradictory (T_Var, T_Abs) or follow directly from the IH
     (TR_Cons).  We show just the interesting ones. *)
  (has_type_cases (induction HT) Case);
    intros t' HeqGamma HE; subst; inversion HE; subst...
  Case "T_App".
    (* If the last rule used was T_App, then t = t1 t2, and three rules
       could have been used to show t ~~> t': T_App1, T_App2, and 
       T_AppAbs. In the first two cases, the result follows directly from 
       the IH. *)
    inversion HE; subst...
    SCase "ST_AppAbs".
      (* For the third case, suppose 
           t1 = tm_abs x T11 t12
         and
           t2 = v2.  We must show that empty |- subst x v2 t12 : T2. 
         We know by assumption that
             empty |- tm_abs x T11 t12 : T1->T2
         and by inversion
             x:T1 |- t12 : T2
         We have already proven that substitution_preserves_typing and 
             empty |- v2 : T1
         by assumption, so we are done. *)
      apply substitution_preserves_typing with T1...
      inversion HT1...
  Case "T_Proj".
  (* If the last rule was T_Proj, then t = tm_proj t1 i.  Two rules
     could have caused t ~~> t': T_Proj1 and T_ProjRcd.  The typing
     of t' follows from the IH in the former case, so we only
     consider T_ProjRcd.

     Here we have tr is a record value, i.e.,
       t1 = tm_rcd tr
     and
       empty |- tm_rcd tr : ty_rcd Tr
     and we can look up the field i using tmr_lookup and tyr_lookup to
     find
        tyr_lookup i Tr = Some Ti
     and
        tmr_lookup i tr = Some ti'.
     We also know that empty |- tm_proj (tm_rcd r) i : Ti.  By 
     Lemma rcd_types_match, we know that empty |- ti' : Ti, and we
     are done. *)
    apply (rcd_types_match empty tr1 Tr i)...
  Case "T_Rcd".
    (* The case where the last rule is T_Rcd follows by
       step_preserves_tmr and T_Rcd. *)
    apply T_Rcd...
    eapply step_preserves_tmr...
  (* FILL IN HERE *)
Qed.

End STLCExtended.