AI 中文总结
本文提出将代数效应与处理程序框架扩展至参数化场景的Cambria语言，通过步长索引逻辑关系证明参数化性，实现资源抽象，支持用户定义资源分配效应，且已完成实际验证。
AI 中文摘要
代数效应与处理程序范式将编程语言中计算效应的接口与实现关注点相分离。本文提出了Cambria，一种将该框架扩展至参数化场景的语言。效应签名可使用由处理程序随操作实现一同实例化的抽象参数类型。参数对内存位置、线程ID等资源进行抽象，使代数效应能够编码动态分配；它们在类型系统中是一等实体，但在运行时被擦除，无需强制转换或类型导向归约。我们通过步长索引逻辑关系证明了参数化性，形式化了参数化处理程序提供的抽象保证；还建立了类型安全性，并对类型推断算法完备性所需的注解进行分类。我们通过实际实现验证了Cambria的实用性，提供的示例包括局部状态、波利亚瓮模型（Pólya's urn）以及并发线程管理——后者是一种参数化效应，其抽象线程ID在并发计算间共享，超出了标准实例的范畴。Cambria是首个具备用户定义资源分配效应的演算，它通过参数化性保证客户端代码无法依赖处理程序对其资源的表示方式。
英文摘要
The algebraic effects and handlers paradigm separates the concerns of the interface and implementation of computational effects in programming languages. We present Cambria, a language that extends this framework to the parametrized setting. Effect signatures may use abstract parameter types that are instantiated by the handler along with the operation implementations. Parameters abstract over resources, such as memory locations or thread IDs, permitting algebraic effects to encode dynamic allocation. They are first-class in the type system but erased at runtime, requiring no coercions or type-directed reduction. We prove parametricity via a step-indexed logical relation, formalizing the abstraction guarantee provided by parametrized handlers. We also establish type safety and classify the annotations needed for completeness of the type inference algorithm. We demonstrate Cambria's practicality with a working implementation and provide examples including local state, Pólya's urn, and concurrent thread management. The last is a parametrized effect whose abstract thread IDs are shared between concurrent computations, going beyond standard instances. Cambria is the first calculus with user-defined resource-allocating effects that guarantees, via parametricity, that client code cannot depend on how a handler represents its resources.
