Representing Data Structures with Invariants in Haskell: The Cases of BST and AVL

Invariants are an essential aspect to take into account for the correct implementation of data structures and their operations. This paper explores how to encode and enforce invariants at type level in Haskell, using Binary Search Trees (BSTs) and AVL trees as case studies. This means the encoding of invariants at type level using advanced features of Haskell type system and their later verification by the type checker. We compare three approaches for the type-level encoding of invariants: fully externalist, externalist, and internalist, each offering a different balance between modularity, safety, and complexity. We also show how to systematically extract standard implementations from correct, invariant-based code.