Heterogeneous binary random-access lists

Abstract

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