Representing Data Structures with Invariants in Haskell: the cases of BST and AVL
summary
Three concrete encodings for BSTs and AVLs in Haskell are implemented and compared: a proof-paired EBST paired with proof that stores a separate inductive proof term, an externalized variant that attaches preservation proofs to each operation, and an integrated IBST correctness-by-construction type that forces invariants at construction time. Keys are promoted to type-level naturals via proxies, insertion is implemented as coupled type- and value-level functions with instance-resolution synthesis of proofs, compilation time rises exponentially with tree size, and a systematic translation to undecorated code yields standard, efficient BST/AVL implementations after removing proof baggage.
AI-written summary · about
chapters (11)
- 0:00Invariants in Haskell data structures
- 1:49Approaches to enforce invariants
- 3:19BST structure in Haskell
- 8:19Externalist approach with proofs
- 12:50Type-safe BST operations
- 16:50Explicit proof approach
- 20:44Correctness by construction
- 23:13Drawbacks of invariant checking
- 24:23Efficient implementations
- 27:30AVL trees with invariants
- 28:13Comparing approaches
related talks
10mFunctional Data Structures
57mApplied category theory and abstract algebra
27mIntrinsically Correct Sorting in Cubical Agda
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
59mHaskell Design Patterns for Genericity & Asynchronous Behavior
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
01h 08mType Arithmetic and the Yoneda Lemma
40mADTs For The Win!