!4#3168

Stream: mathlib4

[Jihoon Hyun]

In line 143, the code fails to synthesize an instance TopologicalSemiring R. However, even after manually adding it in the definition, the code doesn't recognize the declared instance. How should I fix it?

[Eric Wieser]

@Jeremy Tan beat me to it; this is lean4#2074

[Scott Morrison]

i.e. you need set_option synthInstance.etaExperiment true (as Jeremy has already commited).

[Sebastien Gouezel]

Is it time to make our base algebra structures flat by hand (by extending hasZero, hasOne and so on) until CommRing, say? (This should solve most of our issues with lean4#2074, if I understand correctly). Or should we wait for a more proper fix (for instance based on the flat modifier proposed by @Mario Carneiro in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/eta.20ftw/near/337950035*)?

[Ruben Van de Velde]

If we do it manually, do the lean maintainers have anything left to test any fix on?

[Jireh Loreaux]

Let's not flatten during porting at the very least. We can use etaExperiment to finish porting and then afterwards decide how to fix it.

[Eric Wieser]

If we had a flat modifier then I think doing it during porting would be fine

[Eric Wieser]

Because that makes it more similar to the Lean 3 version, not less

[Adam Topaz]

I agree with Eric -- such a flat modifier would be essentially a way to simulate "old_structure_cmd".

[Eric Wieser]

I'll make a PR quickly outlining the other approach

[Kevin Buzzard]

My worry with this approach is that I thought that recently we were actually beginning to see the disadvantages of flattening structures which Leo had predicted years ago and which many of us in the maths community had fought against.

[Kevin Buzzard]

On the other hand we're also beginning to understand the disadvantages of new structures too...

[Eric Wieser]

Our choices are either eta for TC (which has performance problems in Lean 4), old-style classes, or we redesign all our dependent typeclasses like module and star_ring

[Kevin Buzzard]

I still find it very hard to explain to mathematicians that "a topological field is an additive group" is actually something which causes us problems.

[Eric Wieser]

I don't understand your comment, that's not even possible to state in Lean with mathlib

[Kevin Buzzard]

I am extremely grateful and happy that there are clearly several people in the community who have a profound understanding of these typeclass issues by the way, it's the thing which convinces me that the issues will ultimately be resolved.

[Kevin Buzzard]

My example of the field and the group is just a generic statement trying to explain that typeclass inference solves problems which do not exist as far as mathematicians are concerned

[Matthew Ballard]

I think more knobs on the existing machine is probably better than wholesale revamp. At least as a first pass.

[Eric Wieser]

Eric Wieser said:

I'll make a PR quickly outlining the other approach

Done: https://github.com/leanprover-community/mathlib4/pull/3171

[Sebastian Ullrich]

@Eric Wieser Feel free to use !bench on the PR as soon as the build passes (or if it has already passed locally)

[Eric Wieser]

I doubt it will pass as is

[Adam Topaz]

Why does extending FlatHack flatten things?

[Eric Wieser]

I was just fed up of trying to explain the hack in the meeting, and figured an incomplete PR would be clearer

[Eric Wieser]

Because it causes all the other base classes to overlap

[Eric Wieser]

Note that One, Zero, Add, and Mul don't have this base class, but their non-overlap shouldn't matter

[Eric Wieser]

Unfortunately it seems that I'm not allowed to set default value for fields

[Eric Wieser]

Lean complains (in yellow) if two flattened ancestors try to set a default for the same fields. Can I silence the complaint?

[Sebastien Gouezel]

Eric Wieser said:

Our choices are either eta for TC (which has performance problems in Lean 4), old-style classes, or we redesign all our dependent typeclasses like module and star_ring

Isn't there also the option to have very carefully crafted classes to make sure that all diamonds are definitional without eta? For instance, there is a diamond from Ring to AddCommMonoid going through Semiring or AddCommGroup which is not definitional without eta currently, if I am not mistaken.

But we could make it definitional by defining Ring to extend Semiring and hasNeg, and letting AddCommGroup extend AddCommMonoid and hasNeg, and letting Semiring extend AddCommMonoid and registering by hand an instance from Ring to AddCommGroup for which the AddCommGroup fields would beRing.tohasNeg and Ring.toSemiring.toAddCommMonoid. But getting this right everywhere would be extremely hard -- isn't it what Hierarchy Builder is trying to do in Coq?

[Eric Wieser]

I think as your heirarchy grows the only way to simultaneously satisfy everything is to make everything flat.

[Eric Wieser]

Note that the actual problem is brought on by docs4#Module and docs4#StarRing

[Eric Wieser]

These force particular typeclass resolution paths for their *Ring arguments, and the path taken is encoded in the instances

[Patrick Massot]

I wouldn't be surprised at all if writing a huge hierarchy becomes impossible to do by hand and some tool is needed. It doesn't have to be precisely Hierarchy Builder but it would certainly share a number of goals with this system.

[Jeremy Tan]

I do not support flattening the hierarchy. I do support a computer-made hierarchy, Hierarchy Builder-style

[Sebastien Gouezel]

Eric Wieser said:

I think as your heirarchy grows the only way to simultaneously satisfy everything is to make everything flat.

I'm not convinced by this. Rather, I'm convinced it's possible, but much more painful than the "everything flat" solution. So if performance are comparable, we should definitely go with everything flat.

[Jeremy Tan]

After all, the ugly details will be hidden from the enduser

[Eric Wieser]

There is another rather strange way to solve the problem here:

class Module (R M) [Zero R] [Add R] [One R] [Mul R] [Zero M] [Add M]
...

[Eric Wieser]

This means that the argument to Module is always a projection right to the bottom of the lattice of diamonds, so the unification during TC search never needs eta

[Eric Wieser]

I'd be surprised if this approach works everywhere though

[Matthew Ballard]

(deleted)

[Eric Wieser]

I wonder if an explanation of all these options is worth a CICM paper...

[Yaël Dillies]

Jeremy Tan said:

I do not support flattening the hierarchy. I do support a computer-made hierarchy, Hierarchy Builder-style

We're not talking about flattening the hierarchy. We're talking about flattening the inheritance.

[Jireh Loreaux]

Kevin Buzzard said:

My worry with this approach is that I thought that recently we were actually beginning to see the disadvantages of flattening structures which Leo had predicted years ago and which many of us in the maths community had fought against.

This is exactly my concern as well. It's my understanding that preferring new structures over old was to reduce term size and increase performance. It would be a shame to give this up if we can avoid it in other ways (e.g., making TC eta work without being slow), especially if it means we have to do a major redesign to the hierarchy (like the Ring R extends One R, Zero R, Add R, Mul R, Neg R, NatCast R, IntCast R, ... proposal). However, if Eric's FlatHack works and is relatively easy to remove (modulo etaExperiment changes), then it would be nice to know what the performance differences truly are.