Consideration to add Universe and Finite instances for Wedge, Can, Smash

[subttle]

Hello again!

Thank you again for your wonderful project.

There is another very cool library universe, perhaps you're already aware of it, but briefly it is a library "for types where we know all the values". And I think it would be great to add instances of the Universe and Finite (Finite universes) classes for the data types in the smash library. I initially tried to add instances directly to the universe package, see dmwit/universe#62 but it was reasonably suggested that I should try to add the instances here first. The implementations are straight forward:

-- Data.Wedge
instance (Universe a, Universe b) => Universe (Wedge a b) where
  universe :: [Wedge a b]
  universe = fmap toWedge universe
 
instance (Finite a, Finite b) => Finite (Wedge a b) where
  -- 1 + a + b
  cardinality :: Tagged (Wedge a b) Natural
  cardinality = liftA2 (\a b -> 1 + a + b) (retag (cardinality :: Tagged a Natural)) (retag (cardinality :: Tagged b Natural))
  universeF :: [Wedge a b]
  universeF = fmap toWedge universeF

-- Data.Smash
instance (Universe a, Universe b) => Universe (Smash a b) where
  universe :: [Smash a b]
  universe = fmap toSmash universe
instance (Finite a, Finite b) => Finite (Smash a b) where
  -- 1 + ab
  cardinality :: Tagged (Smash a b) Natural
  cardinality = liftA2 (\a b -> 1 + a * b) (retag (cardinality :: Tagged a Natural)) (retag (cardinality :: Tagged b Natural))
  universeF :: [Smash a b]
  universeF = fmap toSmash universeF

-- Data.Can
instance (Universe a, Universe b) => Universe (Can a b) where
  universe :: [Can a b]
  universe = fmap toCan universe
    where
      toCan :: Maybe (These a b) -> Can a b
      toCan = maybe Non (these One Eno Two)
instance (Finite a, Finite b) => Finite (Can a b) where
  -- 1 + a + b + ab
  cardinality :: Tagged (Can a b) Natural
  cardinality = liftA2 (\a b -> 1 + a + b + a * b) (retag (cardinality :: Tagged a Natural)) (retag (cardinality :: Tagged b Natural))
  universeF :: [Can a b]
  universeF = fmap toCan universeF
    where
      toCan :: Maybe (Either (Either a b) (a, b)) -> Can a b
      toCan = maybe Non (either (either One Eno) (uncurry Two))

And in the event the These type becomes available (either through this package or directly from the these package [I'll be opening a ticket there next]), toCan ideally would instead be written:

      toCan :: Maybe (These a b) -> Can a b
      toCan = maybe Non (these One Eno Two)

Here's some example usage in GHCi:

λ> universe @ (Wedge () Bool)
[Nowhere, Here (), There False, There True]
λ> universeF @ (Smash Bool Ordering)
[Nada, Smash False LT, Smash False EQ, Smash False GT, Smash True LT, Smash True EQ, Smash True GT]
λ> cardinality @ (Smash Bool Ordering)
Tagged 7

The cardinality feature is particularly awesome because it allows one to compute the cardinality efficiently using simple arithmetic instead of using the default definition which would expand the entire universe (i.e. create a list of all the values) and then have to take the length of said list.

I'm not sure if you're interested in adding these instances, I won't be offended if you aren't but I figure it is worth asking. Have a great day!

[emilypi]

Hi @subttle, welcome back! I'm not the biggest fan of that library, preferring finitary: https://hackage.haskell.org/package/finitary-2.1.1.0. I'd welcome an addition via that package, but only once my issue is addressed for the next version https://notabug.org/koz.ross/finitary/issues/11

[subttle]

Hi @emilypi! :) No worries at all, thanks for letting me know. For now I'll just close the ticket if that's alright because of the issue you cited and additionally I'm not familiar with finitary (at a glance, however, it looks pretty cool). But if the issue you pointed to gets resolved and I end up familiarizing with finitary in order to rewrite the instances I'll post an update :) Thank you for your consideration!!!

[emilypi]

Thanks @subttle! no worries