Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes

Thomas Bagrel, Arnaud Spiwack

TL;DR

Destination Calculus develops bb, a pure functional λ-calculus with destinations that enables writing into holes within data structures while preserving immutability and safety. The key innovation is a modal, linear type system with an age semiring that tracks both linear usage and scope, allowing destinations to be first-class values stored inside structures with holes. The work provides concrete encodings of classic DPS concepts, develops data structures like lists and queues using holes and difference lists, and demonstrates a breadth of programs (e.g., breadth-first traversal) that are expressible in this framework. A formal type-safety proof in Coq underpins the language design, and an implementation strategy based on in-place mutations is outlined, connecting theory to practical memory-management ideas. Overall, bb offers a unified, verifiable foundation for reasoning about destination-passing in pure functional settings and informs future typed intermediate representations and DPS-inspired optimizations.

Abstract

Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.

Destination Calculus: A Linear λ-Calculus for Purely Functional Memory Writes

TL;DR

Destination Calculus develops bb, a pure functional λ-calculus with destinations that enables writing into holes within data structures while preserving immutability and safety. The key innovation is a modal, linear type system with an age semiring that tracks both linear usage and scope, allowing destinations to be first-class values stored inside structures with holes. The work provides concrete encodings of classic DPS concepts, develops data structures like lists and queues using holes and difference lists, and demonstrates a breadth of programs (e.g., breadth-first traversal) that are expressible in this framework. A formal type-safety proof in Coq underpins the language design, and an implementation strategy based on in-place mutations is outlined, connecting theory to practical memory-management ideas. Overall, bb offers a unified, verifiable foundation for reasoning about destination-passing in pure functional settings and informs future typed intermediate representations and DPS-inspired optimizations.

Abstract

Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.

Paper Structure

This paper contains 35 sections, 2 theorems, 9 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Working with Destinations
  3. Building up a Vocabulary
  4. Structures with Holes
  5. Memory Safety and Purity
  6. Tail-Recursive Map
  7. Linked Lists
  8. A Tail-Recursive Map Function
  9. Functional Queues, with Destinations
  10. Difference Lists
  11. Efficient Queue Using Difference Lists
  12. Scope Escape of Destinations
  13. Breadth-First Tree Traversal
  14. Type System
  15. Modes and the Age Semiring
  16. ...and 20 more sections

Key Result

theorem 1

If $\,\pmb{\vdash}\, \textcolor{ntcolor}{\mathsf{E}} [\, \textcolor{ntcolor}{\mathsf{t}} \,] \pmb{:} \textcolor{typcolor}{\mathsf{T}}$ and $\textcolor{ntcolor}{\mathsf{E}} ~[\, \textcolor{ntcolor}{\mathsf{t}} \,]~ ~\longrightarrow~ ~ \textcolor{ntcolor}{\mathsf{E}}' ~[\, \textcolor{ntcolor}{\mathsf{

Figures (3)

  • Figure 1: Difference list and queue implementation in equirecursive $\lambda_d$
  • Figure 2: Terms, types and modes of $\lambda_d$
  • Figure 3: Scope rules for $\textcolor{kwcolor}{\mathsf{ \pdfliteral direct {2 Tr 0.1 w} upd \pdfliteral direct {0 Tr 0 w} }}_{\textcolor{kwcolor}{\mathsf{ \pdfliteral direct {2 Tr 0.1 w} \ltimes \pdfliteral direct {0 Tr 0 w} }} }$ in $\lambda_d$

Theorems & Definitions (2)

  • theorem 1: Type preservation
  • theorem 2: Progress