Multiple-inheritance hazards in dependently-typed algebraic hierarchies

TL;DR

This paper examines the hazards of multiple inheritance in dependently-typed algebraic hierarchies within theorem provers, highlighting issues with typeclass resolution paths and proposing solutions like kernel support for $ta$-reduction.

Contribution

It provides a detailed analysis of multiple inheritance issues in dependently-typed hierarchies and compares implementation strategies, proposing solutions to improve typeclass management.

Findings

Identifies hazards of multiple inheritance in dependently-typed hierarchies.

Analyzes how different implementation approaches affect judgmental equality.

Proposes kernel support for $ta$-reduction to address identified issues.

Abstract

Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This graph perspective encodes naturally in the typeclass system of theorem provers such as Lean, where nodes can be represented as structures (or records) containing the requisite axioms. This design inevitably needs some form of multiple inheritance; a ring is both a semiring and an abelian group. In the presence of dependently-typed typeclasses that themselves consume typeclasses as type-parameters, such as a vector space typeclass which assumes the presence of an existing additive structure, the implementation details of structure multiple inheritance matter. The type of the outer typeclass is influenced by the path taken to resolve the typeclasses it consumes. Unless all possible paths are considered judgmentally equal, this is a recipe for disaster. This paper provides a concrete explanation of how these situations arise (reduced from real examples in mathlib), compares implementation approaches for multiple inheritance by whether judgmental equality is preserved, and outlines solutions (notably: kernel support for $\eta$-reduction of structures) to the problems discovered.