AI 中文总结
本文提出基于依赖类型Lean的编排库ChorLean，通过携带证明的定位值实现完全端点投影，消除部分性问题，支持与MultiChor相同功能。
AI 中文摘要
随着分布式软件系统的复杂性不断增长，其维护与推理愈发具有挑战性。在实现分布式协议时，开发者必须手动确保不同组件能够适配。编排编程通过在单个程序中指定全局协议并将其投影为称为端点的通信进程，解决了这一挑战。近期的编排方法被设计为编程库，将该范式嵌入Haskell或Rust等宿主语言中。在这些设计中，我们观察到常见的部分性情况：端点投影（EPP）中的不可达分支和定位值访问可能触发运行时错误或未定义行为，依赖于库维护者的手动规范而非静态类型检查。此外，一些程序要求用户编写不可达的虚拟分支，例如对和类型进行分支时。为填补这一空白，我们使用依赖类型的Lean编程语言实现了一个类似的编排库。我们展示了如何从部分EPP函数转向完全EPP函数，还消除了用户代码中对和类型进行模式匹配时的部分性情况。ChorLean通过携带证明的定位值确保完全EPP和安全的值访问，通过Lean的 totality 检查，无未定义情况，同时支持与MultiChor等库相同的功能集。
英文摘要
With growing complexity, distributed software systems become increasingly challenging to maintain and reason about. When implementing a distributed protocol, developers must ensure manually that the different components fit together. Choreographic programming addresses this challenge by specifying global protocols in a single program and projecting them into communicating processes, so-called endpoints. Recent choreographic approaches are designed as programming libraries that embed this paradigm into a host language like Haskell or Rust. In these designs, we observe common cases of partiality: unreachable branches in endpoint projection (EPP) and located-value access can trigger runtime errors or undefined behavior, relying on manual discipline of library maintainers rather than being statically type-checked. Also, some programs require users to write down dummy branches that should not be reachable, for example when branching on sum types. To close this gap, we use the dependently typed Lean programming language to implement a similar choreographic library. We show how we are able to move from a partial EPP to a total EPP function, and also eliminate cases of partiality in user-written code with pattern matching on sum types. ChorLean ensures total EPP and safe value access via proof-carrying located values, passing Lean's totality checker without undefined cases, while supporting the same feature set as libraries like MultiChor.
