Zulip Chat Archive

Stream: general

Topic: bundled in category_theory

Sean Leather (Oct 04 2018 at 12:53):

I just discovered bundled in category_theory.category:

structure bundled (c : Type u  Type v) :=
(α : Type u)
[str : c α]

This seems very useful. In particular, I'm thinking it can help me remove [decidable_eq α] that I have to state everywhere by allowing me to bundle the condition. So, I have a couple of questions:

1. I think it would be helpful to define this outside the category_theory directory because it's not inherently tied to category theory. Do people agree? Should it be in data/bundled.lean or somewhere else?
2. Do the [/] brackets do anything different from (/) here? #print bundled doesn't give any clue.
3. What does str abbreviate? I've typically seen str for string, but I don't think that makes sense here. Is it structure? If so, why? It seems more like a type function being bundled with its parameter, so I'm not clear where the structure comes in.

Kevin Buzzard (Oct 04 2018 at 12:57):

I believe that the only difference the [] makes within the structure is that you can use type class inference within the structure itself. So I am going to stick my neck out and suggest that in this case, where we don't need str to be inferred in any of the other fields, the [] is no different to (). Apologies if I've written something misleading / wrong here. I think the way to make type class inference pick up on str is to have the obvious instance immediately after the definition of the structure.

Scott Morrison (Oct 04 2018 at 13:05):

I think Johannes suggested the [ ] here, and I never thought too hard about it.

Scott Morrison (Oct 04 2018 at 13:06):

str is indeed for structure. We earlier had carrier instead of a.

Scott Morrison (Oct 04 2018 at 13:07):

Regarding bundled, I've found that it has limited use, because as soon as you're past the first round of examples, you want to bundle up multiple typeclasses, and you're back to writing a custom structure for each set of typeclasses you're interested in.

Sean Leather (Oct 04 2018 at 13:34):

I can see how it is not suitable for more involved structures. This applies as well to sigma, subtype, etc. (And, even for cases that fit those, it often seems better to define your own structure.) That said, it is still a unique point in the design space and useful for many cases in which you don't need/want to define a structure.

Sebastian Ullrich (Oct 04 2018 at 15:47):

The binder types (brackets) used in a structure declaration are reflected in the structure's constructor

Kevin Buzzard (Oct 04 2018 at 16:16):

Aah so my post is inaccurate. Thanks Sebastian.

Sean Leather (Oct 05 2018 at 06:05):

The binder types (brackets) used in a structure declaration are reflected in the structure's constructor

@Sebastian Ullrich Ah, of course. Thanks!

Sean Leather (Oct 05 2018 at 08:49):

Here's the resulting PR.

Johan Commelin (Oct 06 2018 at 08:04):

I added a comment: https://github.com/leanprover/mathlib/pull/390#discussion_r223174490

@[reducible] def Meas : Type (u+1) := bundled measurable_space
instance (x : Meas) : measurable_space x := x.inst

The comment says:
Would it be possible to autogenerate these instances? Everytime we bundle a class we want an instance like this. This probably means that bundled has to become meta. I don't know. But I think it would take away one of those "minor annoyances" if all these instances would just be there, automagically.

Mario Carneiro (Oct 06 2018 at 08:06):

You can't hook in to inductive aux theorem generation, but you can have a derive handler

Mario Carneiro (Oct 06 2018 at 08:07):

You could add an attribute to Meas that does the instance generation

Mario Carneiro (Oct 06 2018 at 08:07):

but I don't think you will gain much over just writing that one line

Mario Carneiro (Oct 06 2018 at 08:08):

it's not like there are that many bundled classes. This is a negligible fraction of the work

Last updated: Dec 20 2023 at 11:08 UTC