Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings

TL;DR

This paper formalizes a safe destination-passing style in pure functional programming, develops a core calculus with a modal type system, proves its safety, and demonstrates practical Haskell implementation benefits.

Contribution

It introduces a more expressive core calculus with a modal type system for safe destination passing and adapts it into Haskell, balancing safety and flexibility.

Findings

Type safety proven with Coq

Enhanced expressiveness over existing systems

Practical benefits in large data structure traversal

Abstract

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 {\lambda}-calculus with destinations, {\lambda_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.