Writing an evaluator for the simply typed lambda calculus is a classic example of a dependently typed program that appears in numerous tutorials (McBride, 2004; Norell, 2009, 2013; Abel, 2016). The central idea is to represent the well-typed lambda terms over some universe U using an inductive family (Figure 1). Before writing the evaluator for such terms, we need to define a type of environments, capturing the values associated with the free variables in a term. This is typically done using a heterogeneous list, indexed by a list of the free variables’ types: data Env : Ctx → Setwhere Nil : Env Nil Cons : Val u → Env ctx → Env (u :: ctx) lookup : Env ctx → Ref ctx u → Val u lookup (Cons x ctx) Top = x lookup (Cons x ctx) (Pop ref) = lookup ctx ref

@article{Swierstra20,
  title = {Heterogeneous binary random-access lists},
  author = {WOUTER SWIERSTRA},
  journal = {Journal of Functional Programming},
  volume = {30},
  year = {2020},
  doi = {10.1017/s0956796820000064}
}