Destination-passing style programming introduces destinations, which represent the address of a write-once memory cell. These destinations can be passed as function parameters, allowing the caller to control memory management: the callee simply fills the cell instead of allocating space for a return value. While typically used in systems programming, destination passing also has applications in pure functional programming, where it enables programs that were previously unexpressible using usual immutable data structures. In this thesis, we develop a core λ-calculus with destinations, {λ_d}. Our new calculus is more expressive than similar existing systems, with destination passing designed to be as flexible as possible. This is achieved through a modal type system combining linear types with a system of ages to manage scopes, in order to make destination-passing safe. Type safety of our core calculus was proved formally with the Coq proof assistant. Then, we see how this core calculus can be adapted into an existing pure functional language, Haskell, whose type system is less powerful than our custom theoretical one. Retaining safety comes at the cost of removing some flexibility in the handling of destinations. We later refine the implementation to recover much of this flexibility, at the cost of increased user complexity. The prototype implementation in Haskell shows encouraging results for adopting destination-passing style programming when traversing or mapping over large data structures such as lists or data trees.

翻译：目标传递风格编程引入了目标（destinations），其代表一次性写入内存单元的地址。这些目标可作为函数参数传递，使调用方能够控制内存管理：被调用方仅需填充该单元，而无需为返回值分配空间。虽然目标传递通常用于系统编程，但它在纯函数式编程中也有应用价值，能够实现传统不可变数据结构无法表达的程序。本论文开发了带目标的核心λ演算系统{λ_d}。这一新演算系统比现有类似系统更具表达力，其目标传递机制被设计为尽可能灵活。这是通过结合线性类型与年龄系统的模态类型系统实现的，该系统用于管理作用域以确保目标传递的安全性。我们使用Coq证明助手对核心演算的类型安全性进行了形式化证明。随后，我们探讨了如何将该核心演算适配到现有的纯函数式语言Haskell中——其类型系统弱于我们定制的理论系统。保持安全性需要以牺牲目标处理的灵活性为代价。我们后续改进了实现方案，在增加用户使用复杂度的前提下恢复了大部分灵活性。基于Haskell的原型实现表明，在遍历或映射列表、数据树等大型数据结构时，采用目标传递风格编程具有令人鼓舞的应用前景。