**Matthieu Sozeau**

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 "intrinsically-typed syntax". 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].