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

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

The simply typed lambda-calculus has enough structure to make its theoretical properties interesting, but it is not yet much of a programming language. In this chapter, we begin to close the gap with more familiar languages by introducing a number of familiar features that have straightforward treatments at the level of typing.

Numbers and Booleans

Adding types, constants, and primitive operations for numbers and booleans is easy -- just a matter of combining the two halves of the Stlc.v chapter.

The Unit Type

Another useful base type, found especially in languages in the ML family, is the singleton type Unit. In contrast to the uninterpreted base types of the simply typed lambda-calculus, this type is interpreted, in the simplest possible way: we explicitly introduce a single element---the term constant unit (with a small u)---and a typing rule making unit an element of Unit. We also add unit to the set of possible result values of computations---indeed, unit is the only possible result of evaluating an expression of type Unit.

       t ::=                Terms:
           | ...               (other terms same as before)
           | unit              unit value

       v ::=                Values:
           | ...     
           | unit              unit

       T ::=                Types:
           | ...
           | Unit              Unit type

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:
           | ...               
           | 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. The formalization of pairs is almost too simple to be worth discussing---by this point in the book, it should be about as easy to read a set of inference rules (or a formal Inductive definition) as to wade through a description in English conveying the same information. However, let's look briefly at the various parts of the definition to emphasize the common pattern. In Coq, 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, let's do our products this way. For example, here's how we'd write a function that takes a pair of numbers and returns the pair of their sum and product:

       \x:nat*nat. 
          let sum = x.fst + x.snd in
          let prod = x.fst * x.snd in
          (sum,prod)

Adding pairs to the simply typed lambda-calculus, then, involves adding two new forms of term---pairing, written (t1,t2), and projection, written t.fst for the first projection from t and t.snd for the second projection---plus one new type constructor, T1*T2, called the product of T1 and T2. Syntax:

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

       v ::=                Values:
           | ...
           | (v,v)             pair value

       T ::=                Types:
           | ...
           | T * T             product type

For evaluation, we need several new rules specifying how pairs and projection behave.

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

Rules ST_FstPair and ST_SndPair specify that, when a fully evaluated pair meets a first or second projection, the result is the appropriate component. The congruence rules ST_Fst1 and ST_Snd1 allow reduction to proceed under projections, when the term being projected from has not yet been fully evaluated. ST_Pair1 and ST_Pair2 evaluate the parts of pairs: first the left part, and then---when a value appears on the left---the right part. The ordering arising from the use of the metavariables v and t in these rules enforces a left-to-right evaluation strategy for pairs. (Note the implicit convention that metavariables like v and v1 can only denote values.) We've also added a clause to the definition of values, above, specifying that (v1,v2) is a value. The fact that the components of a pair value must themselves be values ensures that a pair passed as an argument to a function will be fully evaluated before the function body starts executing. The typing rules for pairs and projections are straightforward. The rule, T_Pair, says that (t1,t2) has type T1*T2 if t1 has type T1 and t2 has type T2. Conversely, the rules T_Fst and T_Snd tell us that, if t1 has a product type T11*T12 (i.e., if it will evaluate to a pair), then the types of the projections from this pair are T11 and T12.

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

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

Gamma |- t1 : T11*T12	(T_Snd)
Gamma |- t1.snd : T12

Records

Another familiar structure from everyday programming languages is records. Intuitively, records can be obtained from pairs by two kinds of generalization: they are n-ary products (rather than just binary) and their fields are accessed by label (rather than position). 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 here (they are informal anyway, after all) and do the work of tightening things up elsewhere (in Records.v). Reduction:

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

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

Encoding Records

There are several ways to make the above definitions precise.

• We can directly formalize the syntactic forms and inference rules, staying as close as possible to the form we've given them above. This is conceptually straightforward, and it's probably what we'd want to do if we were building a real compiler -- in particular, it will allow is to print error messages in the form that programmers will find easy to understand. But the formal versions of the rules will not be pretty at all!
• We could look for a smoother way of presenting records -- for example, a binary presentation with one constructor for the empty record and another constructor for adding a single field to an existing record, instead of a single monolithic constructor that builds a whole record at once. This is the right way to go if we are primarily interested in studying the metatheory of the calculi with records, since it leads to clean and elegant definitions and proofs. The file Records.v shows how this can be done.
• Alternatively, if we like, we can avoid formalizing records altogether, by stipulating that record notations are just informal shorthands for more complex expressions involving pairs and product types. We sketch this approach here.

First, observe that we can encode arbitrary-size tuples using nested pairs and the unit value. To avoid overloading the pair notation (t1,t2), we'll use curly braces without labels to write down tuples, so {} is the empty tuple, {5} is a singleton tuple, {5,6} is a 2-tuple (morally the same as a pair), {5,6,7} is a triple, etc.

    {}                 ---->  unit
    {t1, t2, ..., tn}  ---->  (t1, trest)
                              where {t2, ..., tn} ----> trest

Similarly, we can encode tuple types using nested product types:

    {}                 ---->  Unit
    {T1, T2, ..., Tn}  ---->  T1 * TRest
                              where {T2, ..., Tn} ----> TRest

The operation of projecting a field from a tuple can be encoded using a sequence of second projections followed by a first projection:

    t.0        ---->  t.fst
    t.(n+1)    ---->  (t.snd).n

Next, suppose that there is some total ordering on record labels, so that we can associate each label with a unique natural number. This number is called the position of the label. For example, we might assign positions like this:

      LABEL   POSITION
      a       0
      b       1
      c       2
      ...     ...
      foo     1004
      ...     ...
      bar     10562
      ...     ...

We use these positions to encode record values as tuples (i.e., as nested pairs) by sorting the fields according to their positions. For example:

      {a=5, b=6}      ---->   {5,6}
      {a=5, c=7}      ---->   {5,unit,7}
      {c=7, a=5}      ---->   {5,unit,7}
      {c=5, b=3}      ---->   {unit,3,5}
      {f=8,c=5,a=7}   ---->   {7,unit,5,unit,unit,8}
      {f=8,c=5}       ---->   {unit,unit,5,unit,unit,8}

Note that each field appears in the position associated with its label, that the size of the tuple is determined by the label with the highest position, and that we fill in unused positions with unit. We do exactly the same thing with record types:

      {a:Nat, b:Nat}      ---->   {Nat,Nat}
      {c:Nat, a:Nat}      ---->   {Nat,Unit,Nat}
      {f:Nat,c:Nat}       ---->   {Unit,Unit,Nat,Unit,Unit,Nat}

Finally, record projection is encoded as a tuple projection from the appropriate position:

      t.l  ---->  t.(position of l)

It is not hard to check that all the typing rules for the original "direct" presentation of records are validated by this encoding. (The reduction rules are "almost validated" -- not quite, because the encoding reorders fields.) Of course, this encoding will not be very efficient if we happen to use a record with label bar! But things are not actually as bad as they might seem: for example, if we assume that our compiler can see the whole program at the same time, we can choose the numbering of labels so that we assign small positions to the most frequently used labels. Indeed, there are industrial compilers that essentially do this!

Sums

Many programs need to deal with values that can take two distinct forms. For example, we might identify employees in an accounting application using using either their name or their id number. A search function might return either a matching value or an error code. These are specific examples of a binary sum type, which describes a set of values drawn from exactly two given types, e.g. Value = Nat + Bool We create elements of these types by tagging elements of the component types. For example, if n is a Nat then inl v is an Value; similarly, if b is a Bool then inr b is an Value. The names of the tags inl and inr arise from thinking of them as functions

   inl : Nat -> Nat + Bool
   inr : Bool -> Nat + Bool

that "inject" elements of Nat or Bool into the left and right components of the sum type Value. But note that we don't actually treat them as functions. In general, the elements of a type T1 + T2 consist of the elements of T1 tagged with the token inl, plus the elements of T2 tagged with inr. To use elements of sum types, we introduce a case construct (a very simplified form of Coq's match) to destruct them. For example, the following procedure converts an Value into a Nat:

    getNat : \x:Value.
       case x of
         inl n => n
         inl b => if b then 1 else 0

More formally... Syntax:

       t ::=                Terms:
           | ...               
           | inl t             tagging (left)
           | inr t             tagging (right)
           | case t of         case
               inl x => t
             | inr x => t 

       v ::=                Values:
           | ...
           | inl v             tagged value (left)
           | inr v             tagged value (right)

       T ::=                Types:
           | ...
           | T + T             sum type

Evaluation:

t1 --> t1'	(ST_Inl)
inl t1 --> inl t1'

t1 --> t1'	(ST_Inr)
inr t1 --> inr t1'

t0 --> t0'	(ST_Case)
case t0 of inl x1 => t1 | inl x2 => t2 -->
case t0' of inl x1 => t1 | inl x2 => t2

	(ST_CaseInl)
case (inl v0) of inl x1 => t1 | inl x2 => t2 --> [v0/x1] t1

	(ST_CaseInr)
case (inr v0) of inl x1 => t1 | inl x2 => t2 --> [v0/x2] t2

Typing:

Gamma |- t1 : T1	(T_Inl)
Gamma |- inl t1 : T1 + T2

Gamma |- t1 : T2	(T_Inr)
Gamma |- inr t1 : T1 + T2

Gamma |- t0 : T1+T2    Gamma,x1:T1 |- t1 : T
Gamma, x2:T2 |- t2 : T	(T_Case)
Gamma |- case t0 of inl x1 => t1 | inr x2 => t2 : T

Note that one important feature of our other STLC type extensions fails for this one, namely uniqueness of types. The problem arises from the rules for inl and inr. For example, the T_Inl rule says that once we have shown that t1 is an element of type T1, we can derive that inl t1 is an element of T1 + T2 for any type T2. For example, we can derive both inl 5 : Nat + Nat and inl 5 : Nat + Bool (and infinitely many other types). The failure of uniqueness of types means that we cannot build a typechecking algorithm simply by "reading the rules from bottom to top" as we could for all the other features seen so far. This problem could be remedied in various ways. The most direct is to require that the programmer annotate each use of inl and inr with the full sum type T1 + T2 that is intended. But this is rather heavyweight, so we'll just ignore the problem in the remainder of this chapter, since we don't need to build a typechecker.

Variants

Just as products can be generalized to records, sums can be generalized to n-ary labeled types called variants. Instead of T1+T2, we can write something like <l1:T1,l2:T2,...ln:Tn> where l1,l2,... are field labels which are used both to construct instances and as case arm labels.

Lists

The typing features we have seen can be classified into base types like Bool, 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. In principle, we could develop lists given facilities for defining variants and for defining recursive types. But we've skipped the details of the former, and giving semantics to the latter is quite non-trivial. Instead, we'll just discuss the special case of lists directly. 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 built in Coq. We use lcase to destruct lists, to avoid dealing with questions like "what is the head of the empty list?" So, for example, here is a function that calculates the sum of the first two elements of a list of numbers:

    \x:list nat.  
    lcase x of nil -> 0 
       | a::x' -> lcase x' of nil -> a
                     | b::x'' -> a+b 

While we say that cons v1 v2 is a value, we really mean that v2 should also be a list -- we'll have to enforce this in the formal definition of value. Syntax:

       t ::=                Terms:
           | ...
           | nil T
           | cons t t
           | lcase t of nil -> t | x::x -> t

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

       T ::=                Types:
           | ...
           | list T            list of Ts

Reduction:

t1 --> t1'	(ST_Cons1)
cons t1 t2 --> cons t1' t2

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

t1 --> t1'	(ST_Lcase1)
(lcase t1 of nil -> t2 | h::t -> t3) -->
(lcase t1' of nil -> t2 | h::t -> t3)

	(ST_LcaseNil)
(lcase nil T of nil -> t2 | h::t -> t3) --> t2

	(ST_LcaseCons)
(lcase (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_Lcase)
Gamma |- (lcase 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 *)
☐ The ability to form the fixed point of a function of type T->T for any T has some surprising consequences. In particular, it implies that every type is inhabited by some term. To see this, observe that, for every type T, we can define the term By T-Fix and T-Abs, this term has type T. By ST-FixAbs it reduces to itself, over and over again. Thus it is an undefined element of T.

Formalizing the Extensions

Exercise: 4 stars (STLC_extensions)

Formalizing the extensions 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

Note that, for brevity, we've chosen a compressed version of the numeric operations, with a single if0 form combining a zero test and a conditional.

Some variables, for use in examples...

Substitution

Reduction

Next we define the values of our language.

Typing

Next we define the typing rules. These are nearly direct transcriptions of the inference rules shown above.

Examples

Exercise: 2 stars (examples)

Finish the proofs.

(Warning: you may be able to typecheck fact but still have some rules wrong!)

(* Uncomment this once you've defined the [T_Lcase] constructor for
   the typing relation: *)
Hint Extern 2 (has_type _ (tm_lcase _ _ _ _ _) _) => eapply T_Lcase; auto.

☐

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.

Progress

Context Invariance

Preservation

☐