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.

Comparing types

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

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

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

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.

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

Syntax and operational semantics

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

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.

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

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

Some variables, for examples...

{ i1:A }

{ i1:A->B, i2:A }

Well-formedness

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

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

We'll structure our typing judgement so that no ill-formed types like weird_type are assigned to terms. To support this, we define record_ty and record_tm, which identify record types and terms, and well_formed_ty which rules out the ill-formed types.

First, a type is a record type if it is built with either ty_rnil or ty_rcons.

Similarly, a term is a record term if it is built with tm_rnil or tm_rcons

Note that record_ty and record_tm are not recursive -- they just checkw the outermost constructor. The well_formed_ty predicate, on the other hand, verifies that the whole type is well formed in the sense that the tail of every record (the second argument to ty_rcons) is a record.

Of course, we should also be concerned about ill-formed terms, but typechecking can rules those out without the help of an extra well_formed_tm definition because it already examines the structure of terms.

LATER : should they fill in part of this as an exercise? We didn't give rules for it above

Substitution

Reduction

Next we define the valuesof our language. A record is a value if all of its fields are.

Utility functions for extracting one field from record type or term

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

Typing

Next we define the typing rules. These are nearly direct transcriptions of the inference rules shown above. The only major difference is the use of well_formed_ty. In the informal presentation we used a grammar that only allowed well formed record types, so we didn't have to add a separate check.

We'd like to set things up so that that whenever has_type Gamma t T holds, we also have well_formed_ty T. That is, has_type never assigns ill-formed types to terms. In fact, we prove this theorem below.

However, we don't want to clutter the definition of has_type with unnecessary uses of well_formed_ty. Instead, we place well_formed_ty checks only where needed - where an inductive call to has_type won't already be checking the well-formedness of a type.

For example, we check well_formed_ty T in the T_Var case, because there is no inductive has_type call that would enforce this. Similarly, in the T_Abs case, we require a proof of well_formed_ty T11 because the inductive call to has_type only guarantees that T12 is well-formed.

In the rules you must write, the only necessary well_formed_ty check comes in the tm_nil case.

Examples

Exercise: 2 stars (examples)

Finish the proofs.

  fact := 
       fix
         (\f:nat->nat.
            \a:nat. 
               if a=0 then 1 else a * (f (pred a)))

Note that you may be able to type check fact but still have some rules wrong!

☐

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.

Before starting to prove this fact (or the one above!), make sure you understand what it is saying.

Properties of typing

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

Well-formedness

Field lookup

Here is an informal proof of the theorem below.

Lemma: If empty |- v : T and ty_lookup i T returns Some Ti, then tm_lookup i v returns Some ti for some term ti such that has_type empty ti Ti.

Proof: By induction on the typing derivation Htyp. Since ty_lookup i T = Some Ti, T must be a record type, this and the fact that v is a value eliminate most cases by inspection, leaving only the T_RCons case.

If the last step in the typing derivation is by T_RCons, then t = tm_rcons i0 t tr and T = ty_rcons i0 T Tr for some i0, t, tr, T and Tr.

This leaves two possiblities to consider - either i0 = i or not.

• If i = i0, then since ty_lookup i (ty_rcons i0 T Tr) = Some Ti we have T = Ti. It follows that t itself satisfies the theorem.
  
  
• On the other hand, suppose i <> i0. Then
  
          ty_lookup i T = ty_lookup i Tr
  
  and
  
          tm_lookup i t = tm_lookup i tr,
  
  so the result follows from the induction hypothesis. ☐

Progress

Context invariance

Preservation

☐