Papers With

← All papers
First page of Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies

Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies

Eric Wieser

cs.LO Jun 1, 2023 · v2
mathlib formalization algebra type-theory
Read PDF arXiv abstract
TL;DR
Identifies and solves multiple-inheritance diamond hazards in Lean's mathlib algebraic hierarchy.
Abstract
Abstract algebra's hierarchy of properties can be arranged as a directed acyclic graph and encoded in theorem provers like Lean using typeclasses. Multiple inheritance is inevitable since, for example, a ring is both a semiring and an abelian group. With dependently-typed typeclasses consuming other typeclasses as parameters, the type of an outer typeclass depends on the resolution path, and unless all paths are judgmentally equal, problems arise. This paper provides concrete examples reduced from mathlib, compares implementation approaches, and outlines solutions including kernel support for eta-reduction of structures.
Problem

Encoding abstract algebra's hierarchy of properties using dependently-typed typeclasses in Lean leads to multiple-inheritance hazards where the type of an outer typeclass depends on the resolution path, causing problems when paths are not judgmentally equal.

Approach

The authors provide concrete examples reduced from Lean's Mathlib showing how multiple inheritance in dependently-typed algebraic hierarchies produces type-level mismatches. They compare implementation approaches including flat structures, bundled typeclasses, and various encoding strategies. They outline solutions including kernel support for eta-reduction of structures.

Results

The paper identifies specific failure modes in Mathlib's hierarchy encoding and proposes solutions, including changes to Lean's kernel for eta-reduction of structures, which would eliminate the class of problems identified.