future unbundled class hierarchy

Stream: general

[Kevin Buzzard]

Sebastian Ullrich said (in the multiset thread)

Just idle speculation, I suppose in a future unbundled class hierarchy we would rather have an instance is_zero ∅ (multiset a) instead of has_zero (multiset a)?

Does this say "in Lean 4, the whole type class system is going to change a lot"?

I realised over the last two weeks that mathematicians think "G is a group" is a proposition, but that Hyp : group G is not. Maybe if a mathematician is pushed they might concede that actually it's "the pair (G,*) is a group" which is the proposition, but Lean still wants more (identity and inverse). I guess what I'm saying is that questions from students have made me myself question why things are set up this way.

[Mario Carneiro]

The last bit has to do with constructivity in type theory

[Mario Carneiro]

Even if a function is uniquely defined in the relational sense, it's not quite the same as a function in type theory

[Kevin Buzzard]

I thought it might do. So if someone decided to make the fundamental typeclass is_group we'd end up carrying around all three things (mul, inv, identity)

[Mario Carneiro]

So while in ZFC it suffices to have (G,*) since 1 is unique, in lean you really want a concrete witness to this

[Kevin Buzzard]

What about making G plus mul + inv + 1 into a structure, and making is_group a propositional typeclass?

[Mario Carneiro]

In classical lean, you can nevertheless define 1 from * if you wanted, but its definitional reductions won't be great

[Kevin Buzzard]

I'm just trying to question the way we do it, not because of groups, but because of diamonds in general. Presumably if every typeclass was a Prop the diamond problems would go away

[Mario Carneiro]

That option has been discussed (group_struct plus is_group)

[Mario Carneiro]

My response is, if group_struct isn't useful on its own it's not worth the definition

[Kevin Buzzard]

I was wondering whether Sebastian's comments meant that some changes would be implemented

[Mario Carneiro]

if every interesting group_struct is also a group then it may as well be bundled in the definition

[Kevin Buzzard]

Remember there were problems with product of metric / top spaces (which I think were solved) and problems with modules over rings (which I think were not)

[Kevin Buzzard]

Can this sort of approach be used to solve them?

[Mario Carneiro]

Sebastian's comments relate to Leo's plans with the new algebraic hierarchy

[Kevin Buzzard]

If every interesting group_struct were a group, but this caused problems later down the line, then this would be an argument for not bundling.

[Mario Carneiro]

i.e. the @[algebra] classes

[Mario Carneiro]

that's a rather vague worry

[Kevin Buzzard]

Where do I read about Leo's plans and the @[algebra] classes?

[Mario Carneiro]

there's a wiki page for it

[Mario Carneiro]

https://github.com/leanprover/lean/wiki/Refactoring-structures

[Mario Carneiro]

I remain skeptical. I will wait for Leo's implementation before considering anything along these lines

[Kevin Buzzard]

So here we are just waiting to see what happens in Lean 4 and then we go with whatever changes get made?

[Mario Carneiro]

pretty much

[Mario Carneiro]

it's not like there is any other option

[Kevin Buzzard]

I thought that another vague plan was to get a whole bunch of maths out of core Lean

[Mario Carneiro]

I believe that will happen as well

[Kevin Buzzard]

and then it's up to mathlib to decide whether it's group or is_group

[Mario Carneiro]

It's possible that changes to simp will necessitate a certain design

[Mario Carneiro]

And it's not just "leo broke today's system", it could just as easily be "Leo's new system is way better and we would be stupid not to use it"

[Mario Carneiro]

I predict that most of the large scale structural changes in mathlib after lean 4 will be done because we want to take advantage of some new feature, not to fix a breaking change

[Kevin Buzzard]

I'd seen that wiki page several times before, and my interpretation of it was "it's mostly CS stuff that I don't understand, but it documents an old change to the structure command which was already made"

[Kevin Buzzard]

I now think this interpretation might be incorrect -- it might say "even though there is use_old_structure_command or whatever it's called, there are still some things here which are not in Lean and might in the future be in Lean"