Eric Wieser
Cambridge University Engineering Department
We explore a hazard at the intersection of
in the context of algebraic hierarchies.
The slides in this talk show Lean 3 code,
but this is not just about Lean.
Partial Coq and Lean 4 translations are available online at
github.com/eric-wieser/lean-multiple-inheritance
Don't want to repeat the same lemma for every type:
example (a b : ℤ) :
a + b = b + a :=
int.add_comm a b
example (a b : ℚ) :
a + b = b + a :=
rat.add_comm a b
example (a b : ℝ) :
a + b = b + a :=
real.add_comm _ _
⋯
Solutions include
example {R : Type*} [ring R] (a b : R) :
a + b = b + a :=
add_comm _ _
example {R : Ring} (a b : R.carrier) :
a + b = b + a :=
R.add_comm _ _
Ring is of course still not general enough…
class ring (α) extends
semiring α, add_comm_group α
class semiring (α) extends
add_comm_monoid α :=
(one : α) (mul : α → α → α)
class add_comm_group (α) extends
add_group α, add_comm_monoid α
class add_comm_monoid (α) extends
add_monoid α
class add_group (α) extends
add_monoid α :=
(neg : α → α)
class add_monoid (α) :=
(zero : α) (add : α → α → α)
(proof fields like add_comm omitted)
extends isn't part of the type theory;
what should it elaborate to?
How can extends be implemented?
class ring (α) extends
semiring α, add_comm_group α
class ring (α) :=
(to_semiring : semiring α)
(to_add_comm_group : add_comm_group α)
attribute [instance] ring.to_semiring
attribute [instance] ring.to_add_comm_group
Doesn't work because there are two adds!
How can extends be implemented?
class ring (α) extends
semiring α, add_comm_group α
class ring (α) :=
(zero : α) (add : α → α → α)
(one : α) (mul : α → α → α)
(neg : α → α)
variables (α) [i : ring α]
instance ring.to_semiring :
semiring α := { ..i }
instance ring.to_add_comm_group :
add_comm_group α := { ..i }
class ring (α) :=
(to_semiring : semiring α)
(neg : α → α)
variables (α) [i : ring α]
attribute [instance] ring.to_semiring
instance ring.to_add_comm_group :
add_comm_group α :=
{ to_add_group :=
{ to_add_monoid := sorry, ..i }, ..i }
instance ring.to_semiring :
semiring α := { ..i }
instance ring.to_add_comm_group :
add_comm_group α := { ..i }
attribute [instance] ring.to_semiring
instance ring.to_add_comm_group :
add_comm_group α :=
{ to_add_group :=
{ to_add_monoid := sorry, ..i }, ..i }
Nested
avoids unpacking into a new term (orange), which we call preferred
(→) …
…but only for some parents;
for others, both give the non-preferred
(⇢) path.
With nested inheritance, paths are eitherpreferred
(→) or non-preferred
(⇢)
Every class must have one preferred
(→) parent
Many arrangements are possible;
this particular one will be used in this talk.
class ring (α) :=
(zero : α) (add : α → α → α)
(one : α) (mul : α → α → α)
(neg : α → α)
Lean 3's old_structure_cmd,
Coq's Hierarchy Builder
.
No Lean 4 support.
class ring (α) :=
(to_semiring : semiring α)
(neg : α → α)
Incomplete Lean 3 support.
Full Lean 4 support.
Yes!
source: 1 million lines of mathlib ported
from Lean 3 (flat) to Lean 4 (nested)!
-- The additive monoid $M$ is an $R$-module
class module (R M : Type) [semiring R] [add_comm_monoid M] :=
(smul : R → M → M)
(one_smul : ∀ (x : M), smul 1 x = x)
(mul_smul : ∀ (r s : R) (x : M), smul (r * s) x = smul r (smul s x))
(add_smul : ∀ (r s : R) (x : M), smul (r + s) x = smul r x + smul s x)
(zero_smul : ∀ (x : M), smul 0 x = 0)
-- The additive monoid $M$ is an $R$-module
class module (R M : Type) [semiring R] [add_comm_monoid M] :=
(smul : R → M → M)
(one_smul : ∀ (x : M), smul 1 x = x)
(mul_smul : ∀ (r s : R) (x : M), smul (r * s) x = smul r (smul s x))
(add_smul : ∀ (r s : R) (x : M), smul (r + s) x = smul r x + smul s x)
(zero_smul : ∀ (x : M), smul 0 x = 0)
-- The semiring $A$ is an $R$-algebra
class algebra (R A : Type) [comm_semiring R] [semiring A]
-- There is a $\star$ operator compatible with the existing ring structure on $R$
class star_ring (R : Type) [non_unital_semiring R]
-- The existing norm, $\star$, and ring structure are suitable to declare $R$ a $C^\star$-ring
class cstar_ring (R : Type) [non_unital_normed_ring R] [star_ring R]
class module (R M : Type) [semiring R] [add_comm_monoid M] := (smul : R → M → M)
instance semiring.to_module (R) [iS : semiring R] :
module R R :=
{ smul := semiring.mul }
lemma neg_smul {R M} [iR : ring R] [iG : add_comm_group M]
[module R M]
(r : R) (m : M) :
module.smul (-r) m = -(module.smul r m) := sorry
example {R} [iR : ring R] (r : R) (r' : R) :
module.smul (-r) r' = -(module.smul r r') :=
neg_smul r r'error: failed to synthesize type class instance for
⊢ module R R
Everything works correctly with flat
inheritance
… but this is not so with nested
inheritance!
class module (R M : Type) [semiring R] [add_comm_monoid M] := (smul : R → M → M)
instance semiring.to_module (R) [iS : semiring R] :
module R R :=
{ smul := semiring.mul }
lemma neg_smul {R M} [iR : ring R] [iG : add_comm_group M]
[module R M]
(r : R) (m : M) :
module.smul (-r) m = -(module.smul r m) := sorry
example {R} [iR : ring R] (r : R) (r' : R) :
module.smul (-r) r' = -(module.smul r r') :=
by haveI : module R R := semiring.to_module R; exact
neg_smul r r'error: failed to synthesize type class instance for
_inst : module R R
⊢ module R R
Telling lean where the instance is doesn't help!
class module (R M : Type) [semiring R] [add_comm_monoid M] := (smul : R → M → M)
instance semiring.to_module (R) [iS : semiring R] :
@module R R _ _ :=
{ smul := semiring.mul }
lemma neg_smul {R M} [iR : ring R] [iG : add_comm_group M]
[@module R M _ _]
(r : R) (m : M) :
module.smul (-r) m = -(module.smul r m) := sorry
example {R} [iR : ring R] (r : R) (r' : R) :
module.smul (-r) r' = -(module.smul r r') :=
by haveI : module R R := semiring.to_module R; exact
neg_smul r r'error: failed to synthesize type class instance for
_inst : @module R R _ _
⊢ @module R R _ _
module R R isn't showing us the full picture…
class module (R M : Type) [semiring R] [add_comm_monoid M] := (smul : R → M → M)
instance semiring.to_module (R) [iS : semiring R] :
@module R R iS (@semiring.to_add_comm_monoid R iS) :=
{ smul := semiring.mul }
lemma neg_smul {R M} [iR : ring R] [iG : add_comm_group M]
[@module R M @ring.to_semiring R iR (@add_comm_group.to_add_comm_monoid M iG)]
(r : R) (m : M) :
module.smul (-r) m = -(module.smul r m) := sorry
example {R} [iR : ring R] (r : R) (r' : R) :
module.smul (-r) r' = -(module.smul r r') :=
by haveI : module R R := semiring.to_module R; exact
neg_smul r r'error: failed to synthesize type class instance for
_inst : @module R R
(@ring.to_semiring R iR)
(@semiring.to_add_comm_monoid R (@ring.to_semiring R iR))
⊢ @module R R
(@ring.to_semiring R iR)
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R iR))
Instance
@module R R iS (@semiring.to_add_comm_monoid R iS)
Set iS = @ring.to_semiring R iR to get
_inst : @module R R
(@ring.to_semiring R iR)
(@semiring.to_add_comm_monoid R (@ring.to_semiring R iR))
Lemma
@module R M @ring.to_semiring R iR (@add_comm_group.to_add_comm_monoid M iG)
iS = @ring.to_semiring R iR, iG = @ring.to_add_comm_group R iR
⊢ @module R R
(@ring.to_semiring R iR)
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R iR))
The semiring R terms are (definitionally) equal
Are the add_comm_monoid R terms?
Instance
_inst : @module R R
(@ring.to_semiring R iR)
(@semiring.to_add_comm_monoid R (@ring.to_semiring R iR))
Lemma
⊢ @module R R
(@ring.to_semiring R iR)
(@add_comm_group.to_add_comm_monoid R (@ring.to_add_comm_group R iR))
The semiring R terms are (definitionally) equal
Are the add_comm_monoid R terms?
example :
@semiring.to_add_comm_monoid R
(@ring.to_semiring R iR)
=
@add_comm_group.to_add_comm_monoid R
(@ring.to_add_comm_group R iR) :=
rfl
Not with nested
inheritance in Lean 3 (or Coq)!
ring
semiring
add_comm_group
add_comm_monoid
@semiring.to_add_comm_monoid R
(@ring.to_semiring R iR)
@add_comm_group.to_add_comm_monoid R
(@ring.to_add_comm_group R iR)
ring
semiring
add_comm_group
add_comm_monoid
@semiring.to_add_comm_monoid R
(@ring.to_semiring R iR)
@add_comm_group.to_add_comm_monoid R
(@ring.to_add_comm_group R iR)
add_comm_monoid.mk iACM.to_add_monoid
iACM : add_comm_monoid R
This cannot be solved by
… including poorer structures into richer ones; this way, “deducing” one structure from the other always amounts to erasure of dataCompeting Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi
(as add and zero already agree!)
Let's switch to a type theory where
structure point := (x y : ℤ)
-- fails in Lean 3, succeeds in Lean 4
example (p : point) : p = { x := p.x, y := p.y } := rfl
example (p : point) : p = point.mk p.x p.y := rfl
Nice equalities:
example (e : A ≃ B) :
e.symm.symm = e := rfl
fixes diamonds of the form:
example (S : Subalgebra A A) (s : S) :
⟨algebraMap S S s.val, _⟩ = algebraMap S S s := rfl
| Coq | ✗* |
Can be enabled with Primitive Projections.Hierarchy Builderuses flatinheritance so does not need this. |
|---|---|---|
| Agda | ✓* | Can be disabled with no-eta-equality |
| Lean 3 | ✗ | nestedinheritance used rarely in practice |
| Lean 4 (— Feb 2023) |
✗* | Not during typeclass search |
| (Feb — May 2023) | ✗* | … unless using synthInstance.etaExperiment |
| (May 2023 —) | ✓ |
What if we're stuck in a type theory
without $\eta$ for structures?
If the language supports flat inheritance, use it.
(recall: ⇢ indicates paths with (some) eta expansion)
If it doesn't, add a hack …
Swapping the preferred
paths
makes our square commute
Likely possible to do this to any graph,
but not to so by hand to all of mathlib!
module
class module (R M : Type)
[semiring R]
[add_comm_monoid M] :=
(smul : R → M → M)
→
class module (R M : Type)
[has_zero R] [has_add R] [has_one R] [has_mul R]
[has_zero M] [has_add M] :=
(smul : R → M → M)
The has_* classes are all roots of the typeclass graph, so paths always commute.
Much larger term sizes
6 arguments instead of two,
each of which is itself a larger term.
Not always possible
Works in this case because none of the types depend on the proof fields of semiring e.t.c.
Packedstructures
Is this just a typeclass problem?
structure packed_semiring := (carrier : Type) [semiring carrier]
structure packed_add_comm_monoid := (carrier : Type) [add_comm_monoid carrier]
A naïve encoding of a module:
structure packed_module :=
(R : packed_semiring) (M : packed_add_comm_monoid) [module R.carrier M.carrier]
This type is immune, as it's not dependent!
This type is hard to use, as it's not dependent!
structure linear_map (V W : packed_module) (hVW : V.R = W.R) : Type :=
(to_fun : V.M.carrier → W.M.carrier)
(map_smul : ∀ (r : V.R.carrier) v,
to_fun (r • v) = cast (congr_arg _ h) r • to_fun v)
(We want both modules to be over the same ring)
Packedstructures
Is this just a typeclass problem?
structure packed_semiring := (carrier : Type) [semiring carrier]
structure packed_add_comm_monoid := (carrier : Type) [add_comm_monoid carrier]
A realistic encoding of a module:
structure packed_module (R : packed_semiring) :=
(M : packed_add_comm_monoid M) [module R.carrier M.carrier]
structure linear_map (R : packed_semiring) (V W : packed_module R) :=
(to_fun : V.M.carrier → W.M.carrier)
(map_smul : ∀ (r : R.carrier) v, to_fun (r • v) = r • to_fun v)
Packedstructures
Is this just a typeclass problem?
structure packed_semiring := (carrier : Type) [semiring carrier]
structure packed_add_comm_monoid := (carrier : Type) [add_comm_monoid carrier]
A realistic encoding of a module:
structure packed_module (R : packed_semiring) :=
(M : packed_add_comm_monoid M) [module R.carrier M.carrier]
The $\eta$ problem reappears for the R argument, this time for paths from packed_comm_ring to packed_semiring:
example (R : packed_comm_ring) :
packed_module R.to_packed_ring.to_packed_semiring
= packed_module R.to_packed_comm_semiring.to_packed_semiring :=
rfl
Packed structures have the same problem
In practice, nested
inheritance is only compatible with dependent types if $\eta$-reduction of structures is supported.
Not typeclass-specific; canonical structures (implemented via packed structures) hit the same problem.
Other systems avoided the issue by chance:
Hierarchy builderused flat structures for simplicity
old_structure_cmdStructural $\eta$-reduction in Lean 4 was crucial to porting mathlib from Lean 3 to Lean 4.
class add_monoid (α : Type) :=
(zero : α) (add : α → α → α)
class add_comm_monoid (α : Type) :=
(zero : α) (add : α → α → α)
instance add_comm_monoid.to_add_monoid
(α : Type) [i : add_comm_monoid α] : add_monoid α := { ..i }
class semiring (α : Type) :=
(zero : α) (add : α → α → α)
(one : α) (mul : α → α → α)
instance semiring.to_add_comm_monoid
(α : Type) [i : semiring α] : add_comm_monoid α := { ..i }
class add_group (α : Type) :=
(zero : α) (add : α → α → α)
(neg : α → α)
instance add_group.to_add_monoid
(α : Type) [i : add_group α] : add_monoid α := { ..i }
class add_comm_group (α : Type) :=
(zero : α) (add : α → α → α) (neg : α → α)
instance add_comm_group.to_add_group
(α : Type) [i : add_comm_group α] : add_group α := { ..i }
instance add_comm_group.to_add_comm_monoid
(α : Type) [i : add_comm_group α] : add_comm_monoid α := { ..i }
class ring (α : Type) :=
(zero : α) (add : α → α → α) (neg : α → α)
instance ring.to_semiring
(α : Type) [i : ring α] : semiring α := { ..i }
instance ring.to_add_comm_group
(α : Type) [i : ring α] : add_comm_group α := { ..i }
class add_monoid (α : Type) :=
(zero : α) (add : α → α → α)
class add_comm_monoid (α : Type) :=
(to_add_monoid : add_monoid α)
attribute [instance] add_comm_monoid.to_add_monoid
class semiring (α : Type) :=
(to_add_comm_monoid : add_comm_monoid α)
(one : α) (mul : α → α → α)
attribute [instance] semiring.to_add_comm_monoid
class add_group (α : Type) :=
(to_add_monoid : add_monoid α)
(neg : α → α)
attribute [instance] add_group.to_add_monoid
class add_comm_group (α : Type) :=
(to_add_group : add_group α)
attribute [instance] add_comm_group.to_add_group
@[priority 100] instance add_comm_group.to_add_comm_monoid
{α : Type} [i : add_comm_group α] : add_comm_monoid α :=
{ to_add_monoid := i.to_add_group.to_add_monoid, ..i }
class ring (α : Type) :=
(to_semiring : semiring α)
(neg : α → α)
attribute [instance] ring.to_semiring
@[priority 100] instance ring.to_add_comm_group
(α : Type) [i : ring α] : add_comm_group α :=
{ to_add_group :=
{ to_add_monoid :=
i.to_semiring.to_add_comm_monoid.to_add_monoid, ..i },
.. i }