StlcThe Simply Typed Lambda-Calculus

Our job for this chapter: Formalize a small functional language and its type system.
Language: The simply typed lambda-calculus (STLC).
  • A small subset of Coq's built-in functional language...
  • ...but we'll use different concrete syntax (to avoid confusion, and for consistency with standard treatments)
Main new technical challenges:
  • variable binding
  • substitution

The STLC lives in the lower-left front corner of the famous lambda cube (also called the Barendregt Cube), which visualizes three sets of features that can be added to its simple core:
                               Calculus of Constructions
      type operators +--------+
                    /| /|
                   / | / |
     polymorphism +--------+ |
                  | | | |
                  | +-----|--+
                  | / | /
                  |/ |/
                  +--------+ dependent types
                STLC Moving from bottom to top in the cube corresponds to adding polymorphic types like ∀ X, X → X. Adding just polymorphism gives us the famous Girard-Reynolds calculus, System F.
Moving from front to back corresponds to adding type operators like list.
Moving from left to right corresponds to adding dependent types like ∀ n, array-of-size n.
The top right corner on the back, which combines all three features, is called the Calculus of Constructions. First studied by Coquand and Huet, it forms the foundation of Coq's logic.

Overview

Begin with some set of base types (here, just Bool)
Add:
  • variables
  • function abstractions
  • application
Informal concrete syntax:
       t ::= x (variable)
           | \x:T,t (abstraction)
           | t t (application)
           | true (constant true)
           | false (constant false)
           | if t then t else t (conditional)

Some examples:
  • \x:Bool, x
    The identity function for booleans.
  • (\x:Bool, x) true
    The identity function for booleans, applied to the boolean true.
  • \x:Bool, if x then false else true
    The boolean "not" function.
  • \x:Bool, true
    The constant function that takes every (boolean) argument to true.

  • \x:Bool, \y:Bool, x
    A two-argument function that takes two booleans and returns the first one. (As in Coq, a two-argument function in the lambda-calculus is really a one-argument function whose body is also a one-argument function.)
  • (\x:Bool, \y:Bool, x) false true
    A two-argument function that takes two booleans and returns the first one, applied to the booleans false and true.
    As in Coq, application associates to the left -- i.e., this expression is parsed as ((\x:Bool, \y:Bool, x) false) true.
  • \f:Bool→Bool, f (f true)
    A higher-order function that takes a function f (from booleans to booleans) as an argument, applies f to true, and applies f again to the result.
  • (\f:Bool→Bool, f (f true)) (\x:Bool, false)
    The same higher-order function, applied to the constantly false function.

Note that all functions are anonymous.
We'll see how to add named function declarations as "syntactic sugar" in the next chapter.

The types of the STLC include the base type Bool for boolean values and arrow types for functions.
      T ::= Bool
          | T → T
For example:
  • \x:Bool, false has type Bool→Bool
  • \x:Bool, x has type Bool→Bool
  • (\x:Bool, x) true has type Bool
  • \x:Bool, \y:Bool, x has type Bool→Bool→Bool (i.e., Bool → (Bool→Bool))
  • (\x:Bool, \y:Bool, x) false has type Bool→Bool
  • (\x:Bool, \y:Bool, x) false true has type Bool
What is the type of the following term?
       \f:Bool→Bool, f (f true)
(1) Bool → (Bool → Bool)
(2) (Bool→Bool) → Bool
(3) Bool→Bool
(4) Bool
(5) none of the above
How about this one?
         (\f:Bool→Bool, f (f true)) (\x:Bool, false)
(1) Bool→ (Bool → Bool)
(2) (Bool→Bool) → Bool
(3) Bool→Bool
(4) Bool
(5) none of the above

Syntax

We next formalize the syntax of the STLC.

Types

Inductive ty : Type :=
  | Ty_Bool : ty
  | Ty_Arrow : ty → ty → ty.

Terms

Inductive tm : Type :=
  | tm_var : string → tm
  | tm_app : tm → tm → tm
  | tm_abs : string → ty → tm → tm
  | tm_true : tm
  | tm_false : tm
  | tm_if : tm → tm → tm → tm.
Note that an abstraction \x:T,t (formally, tm_abs x T t) is always annotated with the type T of its parameter, in contrast to Coq (and other functional languages like ML, Haskell, etc.), which use type inference to fill in missing annotations. We're not considering type inference at all here.

Examples...
Notation idB :=
  <{\x:Bool, x}>.
Notation idBB :=
  <{\x:Bool→Bool, x}>.
Notation idBBBB :=
  <{\x:((Bool→Bool)->(Bool→Bool)), x}>.
Notation k := <{\x:Bool, \y:Bool, x}>.
Notation notB := <{\x:Bool, if x then false else true}>.

Operational Semantics

To define the small-step semantics of STLC terms...
  • We begin by defining the set of values.
  • Next, we define free variables and substitution. These are used in the reduction rule for application expressions.
  • Finally, we give the small-step relation itself.

Values

To define the values of the STLC, we have a few cases to consider.
First, for the boolean part of the language, the situation is clear: true and false are the only values. An if expression is never a value.

Second, an application is not a value: it represents a function being invoked on some argument, which clearly still has work left to do.

Third, for abstractions, we have a choice:
  • We can say that \x:T, t is a value only when t is a value -- i.e., only if the function's body has been reduced (as much as it can be without knowing what argument it is going to be applied to).
  • Or we can say that \x:T, t is always a value, no matter whether t is one or not -- in other words, we can say that reduction stops at abstractions.
Our usual way of evaluating expressions in Gallina makes the first choice -- for example,
         Compute (fun x:bool ⇒ 3 + 4) yields:
         fun x:bool ⇒ 7 But Gallina is rather unusual in this respect. Most real-world functional programming languages make the second choice -- reduction of a function's body only begins when the function is actually applied to an argument.
We also make the second choice here.

Inductive value : tm → Prop :=
  | v_abs : ∀ x T2 t1,
      value <{\x:T2, t1}>
  | v_true :
      value <{true}>
  | v_false :
      value <{false}>.

STLC Programs

Finally, we must consider what constitutes a complete program.
Intuitively, a "complete program" must not refer to any undefined variables. We'll see shortly how to define the free variables in a STLC term. A complete program, then, is one that is closed -- that is, that contains no free variables.
(Conversely, a term that may contain free variables is often called an open term.)

Having made the choice not to reduce under abstractions, we don't need to worry about whether variables are values, since we'll always be reducing programs "from the outside in," and that means the step relation will always be working with closed terms.

Substitution

Now we come to the heart of the STLC: the operation of substituting one term for a variable in another term. This operation is used below to define the operational semantics of function application, where we will need to substitute the argument term for the function parameter in the function's body. For example, we reduce
       (\x:Bool, if x then true else x) false to
       if false then true else false by substituting false for the parameter x in the body of the function.
In general, we need to be able to substitute some given term s for occurrences of some variable x in another term t. Informally, this is written [x:=s]t and pronounced "substitute s for x in t."

Here are some examples:
  • [x:=true] (if x then x else false) yields if true then true else false
  • [x:=true] x yields true
  • [x:=true] (if x then x else y) yields if true then true else y
  • [x:=true] y yields y
  • [x:=true] false yields false (vacuous substitution)
  • [x:=true] (\y:Bool, if y then x else false) yields \y:Bool, if y then true else false
  • [x:=true] (\y:Bool, x) yields \y:Bool, true
  • [x:=true] (\y:Bool, y) yields \y:Bool, y
  • [x:=true] (\x:Bool, x) yields \x:Bool, x
The last example is key: substituting x with true in \x:Bool, x does not yield \x:Bool, true! The reason for this is that the x in the body of \x:Bool, x is bound by the abstraction: it is a new, local name that just happens to be spelled the same as some global name x.

Here is the definition, informally...
       [x:=s]x = s
       [x:=s]y = y if x ≠ y
       [x:=s](\x:T, t) = \x:T, t
       [x:=s](\y:T, t) = \y:T, [x:=s]t if x ≠ y
       [x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
       [x:=s]true = true
       [x:=s]false = false
       [x:=s](if t1 then t2 else t3) =
                       if [x:=s]t1 then [x:=s]t2 else [x:=s]t3

... and formally:
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
  match t with
  | tm_var y ⇒
      if String.eqb x y then s else t
  | <{\y:T, t1}> ⇒
      if String.eqb x y then t else <{\y:T, [x:=s] t1}>
  | <{t1 t2}> ⇒
      <{([x:=s] t1) ([x:=s] t2)}>
  | <{true}> ⇒
      <{true}>
  | <{false}> ⇒
      <{false}>
  | <{if t1 then t2 else t3}> ⇒
      <{if ([x:=s] t1) then ([x:=s] t2) else ([x:=s] t3)}>
  end

where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).

Technical note: Substitution also becomes trickier to define if we consider the case where s, the term being substituted for a variable in some other term, may itself contain free variables.

For example, using the definition of substitution above to substitute the open term
      s = \x:Bool, r (where r is a free reference to some global resource) for the free variable z in the term
      t = \r:Bool, z where r is a bound variable, we would get
      \r:Bool, \x:Bool, r where the free reference to r in s has been "captured" by the binder at the beginning of t.

Why would this be bad? Because it violates the principle that the names of bound variables do not matter. For example, if we rename the bound variable in t, e.g., let
      t' = \w:Bool, z then [z:=s]t' is
      \w:Bool, \x:Bool, r which does not behave the same as the original substitution into t:
      [z:=s]t = \r:Bool, \x:Bool, r That is, renaming a bound variable in t changes how t behaves under substitution.

Fortunately, since we are only interested here in defining the step relation on closed terms (i.e., terms like \x:Bool, x that include binders for all of the variables they mention), we can sidestep this extra complexity, but it must be dealt with when formalizing richer languages.
What is the result of the following substitution?
       [x:=s](\y:T1, x (\x:T2, x))
(1) (\y:T1, x (\x:T2, x))
(2) (\y:T1, s (\x:T2, s))
(3) (\y:T1, s (\x:T2, x))
(4) none of the above

Reduction

value v2 (ST_AppAbs)  
(\x:T2,t1) v2 --> [x:=v2]t1
t1 --> t1' (ST_App1)  
t1 t2 --> t1' t2
value v1
t2 --> t2' (ST_App2)  
v1 t2 --> v1 t2'
(plus the usual rules for conditionals).

This is call by value reduction: to reduce an application (t1 t2), we
  • first reduce t1 to a value (a function)
  • then reduce the argument t2 to a value
  • then reduce the application itself by substituting t2 for the bound variable x in the body t1.
The ST_AppAbs rule is often called beta-reduction.

Inductive step : tm → tm → Prop :=
  | ST_AppAbs : ∀ x T2 t1 v2,
         value v2 →
         <{(\x:T2, t1) v2}> --> <{[x:=v2]t1}>
  | ST_App1 : ∀ t1 t1' t2,
         t1 --> t1' →
         <{t1 t2}> --> <{t1' t2}>
  | ST_App2 : ∀ v1 t2 t2',
         value v1 →
         t2 --> t2' →
         <{v1 t2}> --> <{v1 t2'}>
  | ST_IfTrue : ∀ t1 t2,
      <{if true then t1 else t2}> --> t1
  | ST_IfFalse : ∀ t1 t2,
      <{if false then t1 else t2}> --> t2
  | ST_If : ∀ t1 t1' t2 t3,
      t1 --> t1' →
      <{if t1 then t2 else t3}> --> <{if t1' then t2 else t3}>

where "t '-->' t'" := (step t t').
What does the following term step to?
    (\x:Bool→Bool, x) (\x:Bool, x) --> ???
(1) \x:Bool, x
(2) \x:Bool→Bool, x
(3) (\x:Bool→Bool, x) (\x:Bool, x)
(4) none of the above
What does the following term step to?
   (\x:Bool→Bool, x)
       ((\x:Bool→Bool, x) (\x:Bool, x))
   --> ???
(1) \x:Bool, x
(2) \x:Bool→Bool, x
(3) (\x:Bool→Bool, x) (\x:Bool, x)
(4) (\x:Bool→Bool, x) ((\x:Bool→Bool, x) (\x:Bool, x))
(5) none of the above
What does the following term normalize to?
   (\x:Bool→Bool, x) notB true -->* ??? where notB abbreviates \x:Bool, if x then false else true
(1) \x:Bool, x
(2) true
(3) false
(4) notB
(5) none of the above
What does the following term normalize to?
  (\x:Bool, x) (notB true) -->* ???
(1) \x:Bool, x
(2) true
(3) false
(4) notB true
(5) none of the above
Do values and normal forms coincide in the language presented so far?
(1) yes
(2) no

Typing

Next we consider the typing relation of the STLC.

Contexts

Question: What is the type of the term "x y"?
Answer: It depends on the types of x and y!
I.e., in order to assign a type to a term, we need to know what assumptions we should make about the types of its free variables.
This leads us to a three-place typing judgment, informally written Gamma |-- t ∈ T, where Gamma is a "typing context" -- a mapping from variables to their types.
Following the usual notation for partial maps, we write (X ⊢> T, Gamma) for "update the partial function Gamma so that it maps x to T."
Definition context := partial_map ty.

Typing Relation

Gamma x = T1 (T_Var)  
Gamma |-- x ∈ T1
x ⊢> T2 ; Gamma |-- t1 ∈ T1 (T_Abs)  
Gamma |-- \x:T2,t1 ∈ T2->T1
Gamma |-- t1 ∈ T2->T1
Gamma |-- t2 ∈ T2 (T_App)  
Gamma |-- t1 t2 ∈ T1
   (T_True)  
Gamma |-- true ∈ Bool
   (T_False)  
Gamma |-- false ∈ Bool
Gamma |-- t1 ∈ Bool    Gamma |-- t2 ∈ T1    Gamma |-- t3 ∈ T1 (T_If)  
Gamma |-- if t1 then t2 else t3 ∈ T1
We can read the three-place relation Gamma |-- t ∈ T as: "under the assumptions in Gamma, the term t has the type T."

Examples

Example typing_example_1 :
  empty |-- \x:Bool, x \in (Bool → Bool).
Proof. eauto. Qed.

Note that, since we added the has_type constructors to the hints database, auto can actually solve this one immediately.
Example typing_example_1' :
  empty |-- \x:Bool, x \in (Bool → Bool).
Proof. auto. Qed.

More examples:
       empty |-- \x:A, \y:A→A, y (y x)
             \in A → (A→A) → A.

Example typing_example_2 :
  empty |--
    \x:Bool,
       \y:Bool→Bool,
          (y (y x)) \in
    (Bool → (Bool → Bool) → Bool).
Proof. eauto 20. Qed.

       empty |-- \x:Bool→B, \y:Bool→Bool, \z:Bool,
                   y (x z)
             \in T.

We can also show that some terms are not typable. For example, let's check that there is no typing derivation assigning a type to the term \x:Bool, \y:Bool, x y -- i.e.,
    ¬∃ T,
        empty |-- \x:Bool, \y:Bool, x y \in T.

Example typing_nonexample_1 :
  ¬∃ T,
      empty |--
        \x:Bool,
            \y:Bool,
               (x y) \in
        T.
Proof.
  intros Hc. destruct Hc as [T Hc].
  (* The clear tactic is useful here for tidying away bits of
     the context that we're not going to need again. *)
  inversion Hc; subst; clear Hc.
  inversion H4; subst; clear H4.
  inversion H5; subst; clear H5 H4.
  inversion H2; subst; clear H2.
  discriminate H1.
Qed.
Another nonexample:
    ¬(∃ S T,
          empty |-- \x:S, x x \in T).
Which of the following propositions is not provable?
(1) y:Bool |-- \x:Bool, x ∈ Bool→Bool
(2) ∃ T, empty |-- \y:Bool→Bool, \x:Bool, y x ∈ T
(3) ∃ T, empty |-- \y:Bool→Bool, \x:Bool, x y ∈ T
(4) ∃ S, x:S |-- \y:Bool→Bool, y x ∈ (Bool→Bool)->S
Which of these is not provable?
(1) ∃ T, empty |-- \y:Bool→Bool→Bool, \x:Bool, y x ∈ T
(2) ∃ S T, x:S |-- x x x ∈ T
(3) ∃ S U T, x:S, y:U |-- \z:Bool, x (y z) ∈ T
(4) ∃ S T, x:S |-- \y:Bool, x (x y) ∈ T