We will now formalize a simply-typed lambda-calculus and write an evaluator for it.
We will formalize only _well-typed_ terms, using a representation know as
Our type structure is very simple: only one base type [unit] and the [arrow] type
to type functions.
We define a shortcut notation for arrows in our AST of types.
A typing context will be a finite list of types.
The [In] inductive family represents _proofs_ of membership of an element in a list.
As you can see, the shape of proofs of [In] actually tells us the _index_ of the
element in the list. From this, we can define a type of expressions, with variables drawn from
a context, and of a given type
These are just the standard typing rules of simply-typed lambda calculus.
So [t : Expr Γ ty] is equivalent to [Γ |- t : ty]: [Expr] represents typing derivations
rather than just arbitrary terms. Let's look at the so-called "de Bruijn" encoding of variables. The identity function
on the unit type can be built using:
Printing all type annotations:
The constant unit function: (fun _ : unit => tt).
The following predicate [All P l] holds only if each and every element [x] of [l] has
a proof of [P x],
[All] is just a regular inductive familiy, we can hence write programs
by pattern-matching on it. Here we show that if [P x -> Q x] for all [x],
then [All P l -> All Q l] for all [l].
It is a variant of the [map] function, this time on [All] instead of [list] or [vec].
Assuming we have a proof the [All P xs] and that [x ∈ xs] ([In x xs]),
then we can fetch the proof of [P x] from the first argument.
This is the analogue of the safe lookup function on [vec] and [fin].
Indeed, given that we have a proof of [x ∈ xs], we know that the list [xs]
cannot be empty, and hence the [all_nil] case does not need to be considered.
We can similarly replace a proof/term of type [P x] inside an [All P xs] if [x ∈ xs]:
One should start thinking that [P x] might not just be "proofs" but
arbirarily indexed data. Indeed, what we will store in the [All] container
will be "values" for our evaluator, and not proofs of some proposition. Our evaluator will build well-typed values from well-typed terms, hence
[Val] is indexed by [Ty]. However, values will be closed, so no context indexes [Val].
To perform evaluation of an expression typable in context [Γ], one
will need to provide an environment of the same type. That is,
a dependently-typed list of values for each type in [Γ].
What we are building here are called "closures", which pair together a
function body and its environment: for each free variable of the body
we have a value.
This represents the empty closure [((λ x : unit. x), ]
This represents the closure [((λ x : unit. y), [y := tt]].
Our evaluator is a function from environments for Γ to values of type A.
(Ignore the argument (n : nat) for now).
Morally, taking an expression with free variables in Γ, it tries to evaluate
it to produce a value. When facing a λ-expression, it simply stops and produces
a closure using the current environment. At applications, it can unpack such
closures for the function part and continue evaluation of the bodies, assuming
the argument also evaluates to a value.
Dependent pattern-matching is used to ensure that from a well-typed term
of type [t] we always produce a value of the same type [t]: our evaluator is type-preserving
"by construction". In addition, thanks to the indexing by [Γ], we also know that at the
variable case, we will _always_ find a corresponding value in the environment.
[eval n Γ t e E] takes an expression with free variables
in [Γ] and type [t], along with an environment for [Γ] and produces (optionally) values in [t].
Here we are using a common idiom in Coq when we don't know how to prove the
termination of a function: we make it structurally recursive on an additional
argument [n] and when this reaches 0 we return an "out of domain" exception (here [None]).
The [n] argument acts as an amount of gas or fuel that the function is allowed
to spend and which must decrease at each recursive call for the function to be accepted
by Coq. It actually limits the longest depth of allowed recursive calls -- the
analogy with blockchain gas which counts exactly the cost of all instructions
of the program breaks down here.
That is why our evaluator is partial, i.e., it returns only _optionally_ a resulting value.
Remark that simply-typed lambda calculus is strongly normalizing, so in principle we could
also define this program by well-founded recursion on the proof of normalization. This is
simply beyond the scope of this example. Note also, on the other hand,
that we could extend the language here with imperative features like mutable references
that can lead to non-termination, and the evaluator would be fine with that, see
http://mattam82.github.io/Coq-Equations/examples/Examples.definterp.html for that example.
We can check that evaluation actually computes the right values:
we know already that it will have the right type.
Exercise: extend the base types with booleans and the expression language
with the constructors of booleans and the (well-typed) conditional (if .. then .. else).
Adapt the evaluator accordingly.
The treatment of the error cases and the environment passing is quite explicit here.
We can abstract on this by using an error monad combined with a reader monad for the environment.
Said differently, we will now write the evaluator as a _monadic_ program, producing
a computation that takes a (well-typed) environment and returns optionally a value.
The monad we are dealing with is defined as [M Γ A], and we will provide a few combinators on it:
The [bind] operation chains two [M] computations, the first produces a value of type A
while the second expects a value in [A] to produce a computation producing [B]'s.
The whole composition hence produces B's. In case the first computation fails (with [None]),
the whole computation fails.
The trivial [ret] combinator turns a value in [A] into a computation that returns it
and does not look at the environment [γ].
The [getEnv] computation just returns the enviroment it is passed as argument
The [usingEnv] combinator take an environment for [Γ], a computation expecting
an environment for [Γ] and produces a computation expecting an environment for [Γ']:
it simply ignores that last environment and uses the given one.
Finally, [timeout] is the computation that always fails.
Our evaluator can now be written as a _computation_-producing function,
and hide the abstraction on the environment and the error cases behind those
add a boolean type and a well-typed [if then else] construction
to this language.
b : bool
t : τ
f : τ
if b then t else f : τ
The constructors [true] and [false] should be values.
Exercise: define the negation [negb] function on booleans and show/test
that evaluating [negb true] evaluates to the [true] value.