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 very much on how it organizes the data it manipulates into algorithmically efficient structures. Most data structures known today are ephemeral: updates to the structure modify it in place, making 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 recreates a new structure, independent of the previous one; this can be done in a time- and memory-efficient way, provided that clever algorithms are used. These efficient persistent data structures play a crucial role in purely functional programming, where programs take the form of mathematical definitions that can be reasoned about in an equational manner. The course presents the main persistent data structures known today, some implemented in a purely functional way and others using hidden imperative modifications, and describes the general principles guiding the design of these persistent structures as well as their complexity analysis.

Lectures

1. Nothing is lost, everything is created: 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.