Simply Typed Lambda Calculus

Representing types

The inductive type typ defined below is our representation of types.

type typ =
  | TUnit : typ
  | TArr  : typ -> typ -> typ

This is entirely straightforward: a constructor for each case in our type grammar, as described above.

Representing programs

The representation of program expressions is shown below:

let var = nat
type exp =
  | EUnit : exp
  | EVar  : var -> exp
  | ELam  : typ -> exp -> exp
  | EApp  : exp -> exp -> exp

This too is straightforward: a constructor for each case in our program grammar, as described above. We use a nat to represent variables var and ELam represents an annotated lambda term of the form \(\lambda _:t. e\), where the name of the binder is omitted, since we’re using de Bruijn’s representation.

Formalizing an Operational Semantics

The inductive type step below describes a single step of computation in what is known as a “small-step operational semantics”. The type step e e' is a relation between an initial program e and a program e' that results after taking one step of computation on some sub-term of e.

type step : exp -> exp -> Type =
  | Beta :
     t:typ ->
     e1:exp ->
     e2:exp ->
     step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)

  | AppLeft :
      #e1:exp ->
      e2:exp ->
      #e1':exp ->
      hst:step e1 e1' ->
      step (EApp e1 e2) (EApp e1' e2)

  | AppRight : 
      e1:exp ->
      #e2:exp ->
      #e2':exp ->
      hst:step e2 e2' ->
      step (EApp e1 e2) (EApp e1 e2')

• The constructor Beta represents the rule for \(\beta\) reduction. The most subtle part of the development is defining subst and sub_beta—we’ll return to that in detail shortly.

• AppLeft and AppRight allow reducing either the left- or right-subterm of EApp e1 e2.

type steps : exp -> exp -> Type =
  | Single : #e0:exp ->
             #e1:exp ->
             step e0 e1 -> 
             steps e0 e1

  | Many  : #e0:exp ->
             #e1:exp ->
             #e2:exp -> 
             step e0 e1 ->
             steps e1 e2 -> 
             steps e0 e2

Substitution: Failed Attempt

Defining substitution is the trickiest part of the system. Our first attempt will convey the main intuitions, but F* will refuse to accept it as well-founded. We’ll then enrich our definitions to prove that substitution terminates.

We’ll define a substitution as a total function from variables var to expressions exp.

let sub0 = var -> exp

These kind of substitutions are sometimes called “parallel substitutions”—the each variable is substituted independently of the others.

When doing a \(\beta\) reduction, we want to substitute the variable associated with de Bruijn index 0 in the body of the function with the argument e and then remove the \(\lambda\) binder—sub_beta0 does just that, replacing variable 0 with e and shifting other variables down by 1, since the \(\lambda\) binder of the function is removed.

let sub_beta0 (e:exp)
  : sub0
  = fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else EVar (y-1)    (* shift -1 *)

The function subst s e applies the substitution s to e:

let sub_inc0 : sub0 =  fun y -> EVar (y+1)

[@@expect_failure [19;19]]
let rec subst0 (s:sub0)
               (e:exp)
  : exp
  = match e with
    | EUnit -> EUnit
    | EVar x -> s x
    | EApp e1 e2 -> EApp (subst0 s e1) (subst0 s e2)
    | ELam t e1 -> ELam t (subst0 (sub_elam0 s) e1)

and sub_elam0 (s:sub0) 
  : sub0
  =  fun y ->
        if y=0
        then EVar y
        else subst0 sub_inc0 (s (y - 1))

• The EUnit case is trivial—there are no variables to substitute.

• In the variable case subst0 s (EVar x) just applies s to x.

• In the EApp case, we apply the substitution to each sub-term.

• The ELam case is the most interesting. To apply the substitution s to the body e1, we have to traverse a binder. The mutally recursive function sub_elam0 s adjusts s to account for this new binder, which has de Bruijn index 0 in the body e1 (at least until another binder is encountered).

  • In sub_elam0, if we are applying s to the newly bound variable at index 0, then we leave that variable unchanged, since s cannot affect it.

  • Otherwise, we have a variable with index at least 1, referencing a binder that is bound in an outer scope; so, we shift it down and apply s to it, and then increment all the variables in the resulting term (using sub_inc0) to avoid capture.

This definition of substitution is correct, but F* refuses to accept it since we have not convinced the typechecker that subst0 and sub_elam0 actually terminate. In fact, F* complains in two locations about a failed termination check.

Substitution, Proven Total

Informally, let’s try to convince ourselves why subst0 and sub_elam0 actually terminate.

• The recursive calls in the EApp case are applied to strictly smaller sub-terms (e0 and e1) of the original term e.

• In the ELam case, we apply subst0 to a smaller sub-term e1, but we make a mutally recursive call to sub_elam0 s first—so we need to check that that call terminates. This is the first place where F* complains.

• When calling sub_elam0, it calls back to subst0 on a completely unrelated term s (y - 1), and F* complains that this may not terminate. But, thankfully, this call makes use only of the sub_inc0 substitution, which is just a renaming substitution and which does not make any further recursive calls. Somehow, we have to convince F* that a recursive call with a renaming substitution is fine.

To distinguish renamings from general substitutions, we’ll use an indexed type sub r, shown below.

let sub (renaming:bool) = 
    f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }

• sub true is the type of renamings, substitutions that map variables to variables.

• sub false are substitutions that map at least one variable to a non-variable.

It’s easy to prove that sub_inc is a renaming:

let sub_inc 
  : sub true
  = fun y -> EVar (y+1)

The function sub_beta shown below is the analog of sub_beta0, but with a type that tracks whether it is a renaming or not.

let sub_beta (e:exp)
  : sub (EVar? e)
  = let f = 
      fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else (EVar (y-1))    (* shift -1 *)
    in
    if not (EVar? e)
    then introduce exists (x:var). ~(EVar? (f x))
         with 0 and ();
    f

• The type says that sub_beta e is a renaming if and only if e is itself a variable.

• Proving this type, particularly in the case where e is not a variable requires proving an existentially quantified formula, i.e., exists x. ~(EVar (subst_beta e) x). As mentioned previously, the SMT solver cannot always automatically instantiate existential quantifiers in the goal. So, we introduce the existential quantifier explicitly, providing the witness 0, and then the SMT solver can easily prove ~(EVar (subst_beta e) 0).

Finally, we show the definitions of subst and sub_elam below—identical to subst0 and sub_elam0, but enriched with types that allow expressing a termination argument to F* using a 4-ary lexicographic ordering.

let bool_order (b:bool) = if b then 0 else 1
let is_var (e:exp) : int = if EVar? e then 0 else 1

let rec subst (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order (EVar? e); 
                     bool_order r;
                     1;
                     e])
  = match e with
    | EUnit -> EUnit
    | EVar x -> s x
    | EApp e1 e2 -> EApp (subst s e1) (subst s e2)
    | ELam t e1 -> ELam t (subst (sub_elam s) e1)

and sub_elam (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[1;
                     bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else subst sub_inc (s (y - 1))
    in
    assert (not r ==> (forall x. ~(EVar? (s x)) ==> ~(EVar? (f (x + 1)))));
    f

Let’s analyze the recursive calls of subst and subst_elam to see why this order works.

• Cases of subst:

  • The EUnit and EVar cases are trivial, as before.

  • In EApp, e is definitely not a variable, so bool_order (EVar? e) is 1. if e1 (respectively e2) are variables, then this recursive call terminates, the lexicographic tuple (0, _, _, _) << (1, _, _, _), regardles of the other values. Otherwise, the last component of the tuple decreases (since e1 and e2 are proper sub-terms of e), while none of the other components of the tuple change.

  • The call to sub_elam s in ELam terminates because the third component of the tuple decreases from 1 to 0, while the first two do not change.

  • The final recursive call to subst terminates for similar reasons to the recursive calls in the EApp case, since the type of sub_elam guarantees that sub_elam s is renaming if an only of s is (so the r bit does not change).

• Cases of sub_elam, in the recursive call to subst sub_inc (s (y - 1)), we have already proven that sub_inc is a renaming. So, we have two cases to consider:

  • If s (y - 1) is a variable, then bool_order (EVar? e), the first component of the decreases clause of subst is 0, which clearly precedes 1, the first component of the decreases clause of subst_elam.

  • Otherwwise, s (y - 1) is not a variable, so s is definitely not a renaming while sub_inc is. So, the second second component of the decreases clause decreases while the first component is unchanged.

Finally, we need to prove that sub_elam s is a renaming if and only if s is. For this, we need two things:

• First, strengthen the type of subst s to show that it maps variables to variables if and only if r is a renaming,

• Second, we need to instantiate an exisential quantifier in sub_elam, to show that if s is not a renaming, then it must map some x to a non-variable and, hence, sub_elam s (x + 1) is a non-variable too. One way to do this is by asserting this fact, which is a sufficient hint to the SMT solver to find the instantiation needed. Another way is to explicitly introduce the existential, as in the exercise below.

In summary, using indexed types combined with well-founded recursion on lexicographic orderings, we were able to prove our definitions total. That said, coming up with such orderings is non-trivial and requires some ingenuity, but once you do, it allows for relatively compact definitions that handle both substiutions and renamings.

let rec subst1 (#r:bool)
               (s:sub r)
               (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order r;
                     1;
                     e])
...

and sub_elam1 (#r:bool) (s:sub r)
  : Tot (sub r)
        (decreases %[bool_order r;
                     0;
                     EVar 0])

let rec subst1 (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order r;
                     1;
                     e])
  = match e with
    | EVar x -> s x
    | ELam t e1 -> ELam t (subst1 (sub_elam1 s) e1)
    | EApp e1 e2 -> EApp (subst1 s e1) (subst1 s e2)
    | EUnit -> EUnit

and sub_elam1 (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else match s (y - 1) with
             | EVar x -> sub_inc x
             | e -> subst1 sub_inc e
    in
    introduce not r ==> (exists x. ~ (EVar? (f x))) 
    with not_r. 
      eliminate exists y. ~ (EVar? (s y))
      returns _
      with not_evar_sy. 
        introduce exists x. ~(EVar? (f x))
        with (y + 1)
        and ()
    ;
    f

Environments

The code below shows our representation of typing environments env, a total function from variable indexes var to Some t or None.

let env = var -> option typ

let empty : env = fun _ -> None

let extend (t:typ) (g:env) 
  : env 
  = fun y -> if y = 0 then Some t
          else g (y-1)

• The empty environment maps all variables to None.

• Extending an an environment g associating a type t with a new variable at index 0 involves shifting up the indexes of all other variables in g by 1.

Typing Relation

The type system of STLC is defined by the inductively defined relation typing g e t shown below. A value of typing g e t is a derivation, or a proof, that e has type t in the environment g.

noeq 
type typing : env -> exp -> typ -> Type =
  | TyUnit :
      #g:env ->
      typing g EUnit TUnit

  | TyVar :
      #g:env ->
      x:var{Some? (g x)} ->
      typing g (EVar x) (Some?.v (g x))

  | TyLam :
      #g :env ->
      t:typ ->
      #e1:exp ->
      #t':typ ->
      hbody:typing (extend t g) e1 t' ->
      typing g (ELam t e1) (TArr t t')
            
  | TyApp :
      #g:env ->
      #e1:exp ->
      #e2:exp ->
      #t11:typ ->
      #t12:typ ->
      h1:typing g e1 (TArr t11 t12) ->
      h2:typing g e2 t11 ->
      typing g (EApp e1 e2) t12

• The type does not support decidable equality, since all its constructors contain a field g:env, a function-typed value without decidable equality. So, we mark the inductive with the noeq qualifier, as described previously.

• TyUnit says that the unit value EUnit has type TUnit in all environments.

• TyVar says that a variable x is well-typed only in an environment g that binds its type to Some t, in which case, the program EVar x has type t. This rule ensures that no out-of-scope variables can be used.

• TyLam says that a function literal ELam t e1 has type TArr t t' in environment g, when the body of the function e1 has type t' in an environment that extends g with a binding for the new variable at type t (while shifting and retaining all other ariables).

• Finally, TyApp allows applying e1 to e2 only when e1 has an arrow type and the argument e2 has the type of the formal parameter of e1—the entire term has the return type of e1.

Exercise

State and prove progress.

let is_value (e:exp) : bool = ELam? e || EUnit? e

let rec progress (#e:exp {~ (is_value e) })
                 (#t:typ)
                 (h:typing empty e t)
  : (e':exp & step e e')
  = let TyApp #g #e1 #e2 #t11 #t12 h1 h2 = h in
    match e1 with
    | ELam t e1' -> (| subst (sub_beta e2) e1', Beta t e1' e2 |)
    | _          -> let (| e1', h1' |) = progress h1 in
                   (| EApp e1' e2, AppLeft e2 h1'|)

Exercise

Use the substitution lemma to state and prove the substitution_beta lemma used in the proof of preservation.

let substitution_beta #e #v #t_x #t #g 
                      (h1:typing g v t_x)
                      (h2:typing (extend t_x g) e t)
  : typing g (subst (sub_beta v) e) t
  = let hs : subst_typing (sub_beta v) (extend t_x g) g =
        fun y -> if y = 0 then h1 else TyVar (y-1) in
    substitution (sub_beta v) h2 hs

Exercise

Prove a preservation lemma for multiple steps.

let rec preservation #e #e' #g #t (ht:typing g e t) (hs:steps e e') 
  : Tot (typing g e' t)
        (decreases hs)
  = match hs with
    | Single s -> 
      preservation_step ht s
    | Many s0 s1 -> 
      let ht' = preservation_step ht s0 in
      preservation ht' s1