Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC