Bundled and unbundled

Stream: new members

[Eric Wieser]

What exactly do "bundled" and "unbundled" mean in the context of lean? Is there a [Note: ...] or manual pages somewhere that summarizes how to choose between them when designing structure?

I've seen some posts here suggesting that extends another_type_class is a bundled type class and [another_type_class] is an unbundled one. I've seem some other discussions suggesting that struct is bundled and class is unbundled.

Is this a mathematics term that I'm unfamiliar with, or a lean concept?

[Johan Commelin]

It's not maths. It's about the amount of things that you package into your structure vs keeping them as arguments.

[Eric Wieser]

The version with more things in the structure is considered the bundled one?

[Eric Wieser]

As for my second point then, is there anything in the lean / mathlib docs about how those choices are made internally? In particular, how there seem to be large swathes of deprecated "unbundled" code - it would be nice to learn and apply the same rationale elsewhere

[Mario Carneiro]

The deprecated directory primarily contains unbundled homs, which have been discussed on Zulip many times before

[Mario Carneiro]

We're trying to move away from [is_group_hom (f : G -> H)] to (f : G ->* H)

[Eric Wieser]

Is there anything I can read to understand the motivation? Perhaps some notable zulip threads?
(I'm not saying I disagree with it, I just want to avoid making the same mistake in my own code)

[Mario Carneiro]

The plan has been around for so long (more than a year) that it's tricky finding a good reference

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/How.20to.20handle.20transfer.20to.20bundled.20homs

[Jalex Stark]

I feel like I gained some clarity on these things by reading the mathlib paper

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/bundling.20mul_homs

[Utensil Song]

image.png

[Utensil Song]

We primarily use semi-bundled definitions for type classes in mathlib, with all operations being bundled except for the carrier types.

[Utensil Song]

When entering the bundled world, I wonder if we need to worry about the old/new or nested/flat structure thing at this stage? I felt reluctant to enter the bundled world ( and using inheritance ) because I read about these technical issues, and they don't look pretty or natural when reading the code in mathlib. And my goal was to make Lean code look like ordinary math as much as possible.

Also, I can't tell when to worry about lower instance priority either.

[Kevin Buzzard]

The linter will tell you about instance priority issues. And you will have to make a decision about old/new structures, but it's one decision per structure. The general rule of thumb is to make everything an old structure. The changes were made because of a scaling issue which we don't really see in mathematical structures so a lot of mathlib still uses old structures

[Utensil Song]

It seems a whole lot of algebra stuff in mathlib is using the new structure (nested) and my code heavily relies on algebra part so I might stay new for now. And it frightens me that old structures struggle to extend new structures (https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/DVRs/near/200764626).

[Eric Wieser]

Kinda related to this conversation - can a type class be fully unbundled (have no fields)?

[Kevin Buzzard]

There are typeclasses which extend other classes and have no fields.

[Kevin Buzzard]

class comm_ring (α : Type u) extends ring α, comm_semigroup α

(that's it)

[Eric Wieser]

Is class comm_ring (α : Type u) [ring α] [comm_semigroup α] legal?

[Kevin Buzzard]

I should think so.

[Kevin Buzzard]

But then if you wanted a commutative ring you'd have to write [ring R] [comm_semigroup R] [comm_ring R]

[Eric Wieser]

You've predicted exactly the trouble I was about to run into

[Eric Wieser]

What's the rule for picking between class comm_ring (α : Type u) extends ring α and class comm_ring (α : Type u) := (r : s ring α)?

[Kevin Buzzard]

This is a computer science question. I don't really understand these issues properly at all.

[Eric Wieser]

Seems in my case that only the latter is legal, so lets try that approach

[Kevin Buzzard]

Once you've actually got your use case compiling, you might want to run it past the people in #maths to see what the experts think of it. (me doing this last week)

[Eric Wieser]

Good idea, thanks

[Eric Wieser]

On the note of compiling... If there's one type class argument that lean is having trouble inferring, can I specify it explicitly without having to insert a tonne of placeholders to pad all the arguments that lean guesses correctly?

[Bryan Gin-ge Chen]

Not in Lean 3 as far as I know, but there's hope that the syntax for this will be better in Lean 4.

[Kevin Buzzard]

You only have to pad the ones to the left of the one that Lean had trouble inferring.

[Eric Wieser]

How do I deal with cases where lean wants a ring R but I have comm_ring R?

[Kevin Buzzard]

But there are other workarounds. For example haveI or letI in tactic mode.

[Kevin Buzzard]

If you have a comm_ring, Lean's type class inference system should have no trouble inferring the ring structure.

[Eric Wieser]

type mismatch at application
  module (A 0) G
term
  graded_algebra_components.zc
has type
  comm_ring (A 0)
but is expected to have type
  ring (A 0)

[Eric Wieser]

I've had to pass the type class explicitly because I was attempting to bundle it

[Kevin Buzzard]

That's not what I interpreted your question as meaning

[Kevin Buzzard]

import tactic

example (R : Type) [comm_ring R] : ring R := by apply_instance

[Eric Wieser]

I'm taking about the first question in combination with the second one

[Kevin Buzzard]

This is xy. You shouldn't be passing explicit proofs that something is a ring. The whole point of the type class inference system is to do this for you.

[Eric Wieser]

This is "what happens if I try what I asked in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Bundled.20and.20unbundled/near/202583368"

[Kevin Buzzard]

The answer to the question you asked is to run that example above but instead give it a name and then #print it so you know what the function which eats a comm_ring and spits out a ring is called.

[Kevin Buzzard]

But the real issue is that nobody should need to know the name of that function, so if you need to know it then there is something more fundamentally wrong

[Kevin Buzzard]

Type class inference will fill in that field, and if it doesn't, then don't fill it in manually, but instead figure out why it didn't, and fix the actual problem

[Kevin Buzzard]

Eric Wieser said:

This is "what happens if I try what I asked in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Bundled.20and.20unbundled/near/202583368"

There is a typo in what you posted (a random s) but assuming it's not supposed to be there then instead of the round brackets you should make them square brackets, and you might have to manually tag the structure projection with @[instance]

[Kevin Buzzard]

What I'm saying is that the infrastructure is there, I believe, to make the set-up work.

[Eric Wieser]

The full repro is:

class graded_algebra_components
  -- a type for each grade.
  (A : ℕ → Type u)
:=
  -- (A 0) is the scalar type
  [zc: comm_ring (A 0)]

  -- all the types form commutative vector spaces
  [b: ∀ n, add_comm_group (A n)]
  [c: ∀ n, module (A 0) (A n)]


class graded_algebra_hom
  (A : ℕ → Type u) (G: Type u)
  [g : graded_algebra_components A]
  [add_comm_group G]
  [@module (A 0) G begin haveI r := g.zc, apply_instance end _] :=
(to_fun : ∀n, A n →ₗ[A 0] G)

Your apply_instance and haveI tip was enough to get it to compile, thanks

[Kevin Buzzard]

import tactic

universe u

class comm_ring' (α : Type u) :=
[r : ring α]

#print prefix comm_ring'

attribute [instance] comm_ring'.r

example (R : Type) [comm_ring' R] : ring R := by apply_instance -- works

[Eric Wieser]

Oh nice

[Eric Wieser]

Thanks!

[Eric Wieser]

Is there an inline syntax for that?

[Eric Wieser]

That solves my problem perfectly

[Kevin Buzzard]

I don't know an inline syntax -- you mean making zc (and b and c) an instance whilst defining graded_algebra_components? I don't know.

[Eric Wieser]

Yeah, some kind of @[instance] marker