Papers With

← All papers
First page of Use and abuse of instance parameters in the Lean mathematical library

Use and abuse of instance parameters in the Lean mathematical library

Anne Baanen

cs.LO Feb 3, 2022 · v3
mathlib tooling type-theory
Read PDF arXiv abstract
TL;DR
Analyzes typeclass design patterns and scaling challenges in Lean's mathlib library.
Abstract
The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.
Problem

Lean's mathematical library mathlib makes extensive use of the typeclass pattern (instance parameters) for organizing mathematical structures. At the scale of mathlib, complications arise that are not evident in smaller projects.

Approach

The paper analyzes representative examples of design patterns involving instance parameters in the Lean 3 version of mathlib. It focuses on complications arising at scale, including diamond inheritance, default instances, and performance issues with instance search, and documents how the mathlib community addresses them.

Results

The analysis identifies recurring patterns and pitfalls: diamonds in algebraic hierarchies, forgetful inheritance, out-parameters for synthesis, and bundled vs. unbundled structures. The paper documents community solutions and trade-offs, serving as a reference for other projects using typeclasses at scale.