一句话：提出按类型索引的异构二叉随机访问列表，为依赖类型求值器提供支持随机访问的环境表示。
论文以 simply typed lambda calculus 的依赖类型求值器为背景：为表示项中自由变量对应的值，通常需要按变量类型列表索引的异构环境，并通过 lookup 按引用查找取值。标题与摘要指向的核心是将二叉随机访问列表推广到异构、按类型索引的情形，使环境在保持依赖类型安全的同时支持随机访问，而不再局限于线性异构列表。摘要主要给出经典求值器示例与异构列表定义，未展开具体复杂度、定理或实验评估；因此其贡献可理解为面向依赖类型编程的环境数据结构设计与实现。
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