Persistent data structures

Xavier Leroy

Collège de France, chair of software sciences, 2022-2023

This is an English translation of Xavier Leroy's 2022-2023 lectures at Collège de France, "Structures de données persistantes".

Abstract

The performance of a program depends greatly on how it organizes the data it manipulates into algorithmically efficient structures. Most known data structures are ephemeral: updates modify the structure in place, rendering the state of the structure before modification inaccessible. In contrast, persistent data structures retain the complete history of the data: everything happens as if an update creates a new structure, independent of the previous one. This can be done in a time- and memory-efficient way if clever algorithms are used. These efficient persistent data structures play a crucial role in purely functional programming, where programs are mathematical definitions that can be reasoned about equationally. This course introduces the main persistent data structures in use today, some of which are implemented in a purely functional manner, while others use hidden imperative modifications. The course also describes the general principles that guide the design of these persistent structures as well as their complexity analysis.

Lectures

1. Nothing is lost, everything is created: an introduction to persistent data structures.
2. Balanced trees + path copying = persistent dictionaries.
3. Reconciling amortization and persistence: why laziness matters.
4. How to make an ephemeral data structure persistent?
5. Numerical representations and non-regular data types.
6. From formal derivatives to navigation in a structure: contexts, zippers, fingers.
7. In search of the lost vector: lower bounds and conclusions.

Seminar talks

Some talks were given in English, others in French. Video recordings and slides can be found on the seminar course pages.

1. Tobias Nipkow: Verification of Functional Data Structures: Correctness and Complexity.
2. Jean-Christophe Filliâtre: Structures de données semi-persistantes.
3. KC Sivaramakrishnan: Mergeable Replicated Data Types.
4. Arthur Charguéraud: Comment allier persistance et performance.
5. Pierre-Etienne Meunier: Une algèbre de modifications, ou : le contrôle de versions pour tous.