Zulip Chat Archive

Stream: general

Topic: finset implementation


view this post on Zulip Kenny Lau (Sep 08 2018 at 12:04):

What is the advantage of implementing finset as it is now, over implementing it as multiset quotient by extensionality?

view this post on Zulip Chris Hughes (Sep 08 2018 at 12:13):

I'm guessing efficiency of computation, but also perhaps some of the proofs are easier, since the functions are more or less identical to the multiset versions. Something like finset.sum is harder to implement with finsets as a quotient.

view this post on Zulip Kenny Lau (Sep 08 2018 at 17:16):

But if we implement it as a quotient, then we can have finset.union

view this post on Zulip Chris Hughes (Sep 08 2018 at 17:17):

Without decidable_eq you mean? Hooray. On the downside we'll need decidable_eq for finset.sum and finset.card

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:27):

@Kenny Lau I think both implementations can be valuable. Find a different name and then you can provide that new implementation.

view this post on Zulip Kenny Lau (Sep 08 2018 at 23:27):

great

view this post on Zulip Kenny Lau (Sep 08 2018 at 23:27):

could you help me think of a name?

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:28):

One benefit of finset's current implementation is in writing programs that are meant to be executed. Keeping the list minimal is more economical on memory.

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:31):

The most obvious candidate would be finset' but I'm not sure that it's good. We could go with variations on finset (like finite_set) but I think that's more confusing than anything else. How about no_eq.finset?

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:31):

The other alternative would be to change the name of the current implementation to compact.finset or minimal.finset or efficient.finset

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:33):

I like your idea. Your kind of implementation makes a set that is easier to use as a monad and as a traversable collection.

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:34):

I would suggest something like qfinset or stacked_finset

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:34):

I'm not seeing where the gains are though

view this post on Zulip Kevin Buzzard (Sep 08 2018 at 23:35):

you can have union without decidable equality :-)

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:35):

gains plural

view this post on Zulip Kevin Buzzard (Sep 08 2018 at 23:35):

:-)

view this post on Zulip Kevin Buzzard (Sep 08 2018 at 23:36):

Presumably this means that the two definitions can't be proved to be equal without decidable equality?

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:36):

For the most part anything you can do with a stacked finset you can also do with a multiset

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:37):

There is a computable function finset -> qfinset but the reverse is erase_dup which requires decidable eq

view this post on Zulip Kevin Buzzard (Sep 08 2018 at 23:37):

gotcha

view this post on Zulip Mario Carneiro (Sep 08 2018 at 23:38):

But all these functions already exist, between finset and multiset

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:41):

I can see three reasons for using stacked sets.

1. you mean it to form a monad (or a similar kind of functor)
2. you need it to be traversable
3. you want to work with finite sets while using set equality directly without translating back and forth between set and multiset.

view this post on Zulip Simon Hudon (Sep 08 2018 at 23:43):

qfinset is then like set+ finiteness invariant, similarly to multiset


Last updated: May 07 2021 at 00:30 UTC