一句话：提出上下文嵌入技术，用实例解析在易用高阶接口与一阶表示间建立类型安全的上下文导向同构。
在嵌入式语言中表示绑定变量长期面临表达力与易用性的权衡：一阶的 de Bruijn 索引性质好但难读难写，高阶表示可复用宿主语言绑定器但各有代价。现有最优方案 unembedding 在高阶与一阶表示间来回翻译，然而其类型安全依赖外部元理论论证，限制了潜力。本文提出一种新的嵌入技术，利用实例解析定义从易用高阶接口到一阶表示的上下文导向同构，从而在语言内部获得类型安全。与以往技术不同，该方法还适用于具有模态与子结构（如线性）类型系统的嵌入式语言，使 unembedding 能服务于现代语言。
Representing bound variables in embedded languages is a challenging problem, often requiring painful trade-offs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read and write. On the other hand, higher-order representations can piggy-back on the host language's binders to offer a more ergonomic interface, at a variety of costs depending on the technique. The current state-of-the-art is unembedding, i.e. a translation from the higher-order representation to the first-order and back again to get the best of both worlds. Unfortunately, the fact that this translation is type-safe relies on external metatheoretic arguments, holding unembedding back from its true potential. We solve this problem with a new embedding technique that uses instance resolution to define a context-directed isomorphism between an ergonomic higher-order interface and a first-order representation. Unlike previous techniques, this also applies to embedded languages with modal and substructural (e.g. linear) type systems, making unembedding relevant for modern languages.
@article{FrohlichFKW26,
title = {Contextual Embeddings: Implementing Bound Variables through Instance Resolution},
author = {Samantha Frohlich and Jessica Foster and G. A. Kavvos and Meng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808269}
}