## Stream: general

### Topic: finset implementation

#### 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?

#### 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.

#### Kenny Lau (Sep 08 2018 at 17:16):

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

#### 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

#### 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.

great

#### Kenny Lau (Sep 08 2018 at 23:27):

could you help me think of a name?

#### 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.

#### 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?

#### 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

#### 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.

#### Mario Carneiro (Sep 08 2018 at 23:34):

I would suggest something like qfinset or stacked_finset

#### Mario Carneiro (Sep 08 2018 at 23:34):

I'm not seeing where the gains are though

#### Kevin Buzzard (Sep 08 2018 at 23:35):

you can have union without decidable equality :-)

gains plural

:-)

#### 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?

#### 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

#### 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

gotcha

#### Mario Carneiro (Sep 08 2018 at 23:38):

But all these functions already exist, between finset and multiset

#### 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.

#### 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