Zulip Chat Archive

Stream: maths

Topic: bundling


view this post on Zulip 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"...

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:55):

Does anyone have some sort of explanation for this?

view this post on Zulip Chris Hughes (Jun 13 2020 at 13:15):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 13:25):

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

view this post on Zulip 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...

view this post on Zulip Reid Barton (Jun 13 2020 at 13:26):

There are no bundled objects there though...?

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:27):

I guess there are multiple levels of bundling

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:27):

I agree that they are less bundled than R : Ring

view this post on Zulip Reid Barton (Jun 13 2020 at 13:27):

I mean bundling a type with its operations

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:27):

Maybe I'm using the wrong term

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:35):

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

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:35):

Or a field, or a DVR?

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:36):

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

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:36):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jun 13 2020 at 13:37):

Probably something like R : Alg K h : is_PID R

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:37):

What kind of parens around the thing on the right?

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:38):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:40):

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

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:40):

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

view this post on Zulip Reid Barton (Jun 13 2020 at 13:40):

Johan Commelin said:

What kind of parens around the thing on the right?

()

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:41):

Reid doesn't like typeclasses. :-)

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:42):

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

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jun 13 2020 at 13:43):

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jun 13 2020 at 13:44):

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

view this post on Zulip 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.

view this post on Zulip 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. :-(

view this post on Zulip 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