## Stream: maths

### Topic: bundling

#### Johan Commelin (Jun 13 2020 at 12:55):

I don't know what's going on, but I feel like I prefer unbundled objects, whereas we seem to be moving towards bundled "morphisms"...

#### Johan Commelin (Jun 13 2020 at 12:55):

Does anyone have some sort of explanation for this?

#### Chris Hughes (Jun 13 2020 at 13:15):

The instance for composition of unbundled homs doesn't work.

#### Reid Barton (Jun 13 2020 at 13:25):

You haven't fully embraced the wonder of bundled objects.

#### Johan Commelin (Jun 13 2020 at 13:26):

@Reid Barton If the errors in the DVR thread are examples of the "wonder of bundled objects", then...

#### Reid Barton (Jun 13 2020 at 13:26):

There are no bundled objects there though...?

#### Johan Commelin (Jun 13 2020 at 13:27):

I guess there are multiple levels of bundling

#### Johan Commelin (Jun 13 2020 at 13:27):

I agree that they are less bundled than R : Ring

#### Reid Barton (Jun 13 2020 at 13:27):

I mean bundling a type with its operations

#### Johan Commelin (Jun 13 2020 at 13:27):

Maybe I'm using the wrong term

#### Scott Morrison (Jun 13 2020 at 13:34):

R : Ring is kind of great. It's succinct and easy to work with, and you don't seem to give much up: there's still a coercion to Type, and a typeclass on that coercion, so you can still write x y : R, and x + x * y.

#### Johan Commelin (Jun 13 2020 at 13:35):

@Scott Morrison But what do you do if you want a PID?

#### Johan Commelin (Jun 13 2020 at 13:35):

Or a field, or a DVR?

#### Scott Morrison (Jun 13 2020 at 13:36):

You mean the opposite --- if you have a R : PID, and you just want a Ring?

#### Johan Commelin (Jun 13 2020 at 13:36):

Maybe I want a PID that is an algebra over a field.

#### Johan Commelin (Jun 13 2020 at 13:36):

How would you wish to write a variables line that says: let R be a PID that is an algebra over the field K?

#### Reid Barton (Jun 13 2020 at 13:37):

Probably something like R : Alg K h : is_PID R

#### Johan Commelin (Jun 13 2020 at 13:37):

What kind of parens around the thing on the right?

#### Scott Morrison (Jun 13 2020 at 13:38):

After which you can probably write PID.of R to obtain a bundled PID?

#### Scott Morrison (Jun 13 2020 at 13:39):

You would never get rid of the unbundled typeclasses. They are still there to mediate notation, and all the bundled types are just a pair consisting of a carrier type and a typeclass (perhaps several).

#### Johan Commelin (Jun 13 2020 at 13:39):

I don't like PID.of R. It's ok if we need it occasionally. But if we go full bundled objects... I guess this sort of repackaging will be all over the place.

#### Scott Morrison (Jun 13 2020 at 13:40):

So you can still do mixins when you want to talk about several interacting structures, and use X.of to recover the different bundled objects as needed.

#### Johan Commelin (Jun 13 2020 at 13:40):

You could get rid of unbundled typeclasses, and just keep only the notation classes, right?

#### Scott Morrison (Jun 13 2020 at 13:40):

Well -- I think Reid's answer above says no.

#### Reid Barton (Jun 13 2020 at 13:40):

Johan Commelin said:

What kind of parens around the thing on the right?

()

#### Scott Morrison (Jun 13 2020 at 13:41):

Reid doesn't like typeclasses. :-)

#### Scott Morrison (Jun 13 2020 at 13:42):

I had been thinking [], without which PID.of R wouldn't work.

#### Johan Commelin (Jun 13 2020 at 13:42):

I wish we could write

variables [principal_ideal_domain R]


and that it would be syntactic sugar for

variables {R : Type*} [ring R] [is_principal_ideal_domain R]


#### Reid Barton (Jun 13 2020 at 13:43):

Being a PID is a theorem, and the one thing Lean is really good at is proving theorems

#### Scott Morrison (Jun 13 2020 at 13:43):

It's a good point. There's "nothing" to bundle.

#### Johan Commelin (Jun 13 2020 at 13:43):

And if you do

instance : principal_ideal_domain R := _


it should really add instances of ring R (unless it exists already??) and is_principal_ideal_domain R...

#### Johan Commelin (Jun 13 2020 at 13:44):

But maybe the latter idea isn't even needed...

#### Johan Commelin (Jun 13 2020 at 13:45):

Just the syntactic sugar for introducing hypotheses would already help a lot to improve readability while keeping a flexible system.

#### Scott Morrison (Jun 13 2020 at 13:45):

Oh, you just reminded me of a bug in my R-Alg PR. I made separate semimodule and algebra instances, which then result in non-defeq semimodules via algebra.to_semimodule... Oops. I've done this several times already. :-(

#### Scott Morrison (Jun 13 2020 at 13:47):

Oh, scratch that, of course the semimodule instance was there all along. Hrm. Oh well, a problem for tomorrow.

Last updated: May 18 2021 at 06:15 UTC