Zulip Chat Archive

Stream: general

Topic: bundled in category_theory


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

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

view this post on Zulip Scott Morrison (Oct 04 2018 at 13:05):

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

view this post on Zulip Scott Morrison (Oct 04 2018 at 13:06):

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

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

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

view this post on Zulip Sebastian Ullrich (Oct 04 2018 at 15:47):

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

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 16:16):

Aah so my post is inaccurate. Thanks Sebastian.

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

view this post on Zulip Sean Leather (Oct 05 2018 at 08:49):

Here's the resulting PR.

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

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 08:07):

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

view this post on Zulip Mario Carneiro (Oct 06 2018 at 08:07):

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

view this post on Zulip 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: May 14 2021 at 00:42 UTC