`These a b`, `Can a b`, `Wedge a b`, and `Smash a b` Types

[subttle]

Hello again! Thank you all again for this wonderful package and all your hard work on it. I am curious if you would be interested in adding a few more Finite instances to universe-instances-extended for the basic types found in the these package and smash package. The code I have now looks something like this, but if you would be interested in a PR, I would of course try to match your coding style (ditch the unicode, etc. [: ) :

Edit removed the UnicodeSyntax for you @phadej :]

import           Data.Can   (Can (..), can)
import           Data.Smash (Smash (..), smash, toSmash)
import           Data.These (These (..), these)
import           Data.Wedge (Wedge (..), wedge, toWedge)

instance (Universe a, Universe b) => Universe (Smash a b) where
  universe :: [Smash a b]
  universe = fmap toSmash universe

instance (Universe a, Universe b) => Universe (Wedge a b) where
  universe :: [Wedge a b]
  universe = fmap toWedge universe

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 (Universe a, Universe b) => Universe (These a b) where
  universe :: [These a b]
  universe = fmap toThese universe
    where
      toThese :: Either (Either a b) (a, b) -> These a b
      toThese = either (either This That) (uncurry These)

Leaving just the Finite instances, which are pretty straight forward.

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

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

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 (These a b) -> Can a b
      toCan = maybe Non (these One Eno Two)

instance (Finite a, Finite b) => Finite (These a b) where
  -- a + b + ab
  cardinality :: Tagged (These a b) Natural
  cardinality = liftA2 (\a b -> a + b + a * b) (retag (cardinality :: Tagged a Natural)) (retag (cardinality :: Tagged b Natural))
  universeF :: [These a b]
  universeF = fmap toThese universeF
    where
      toThese :: Either (Either a b) (a, b) -> These a b
      toThese = either (either This That) (uncurry These)

I won't be offended if you aren't interested and close the ticket, but let me know if you are interested and I would be happy to make a PR. Thank you for your time and consideration. Have a great day!

P.S. I have an awesome update in the works for my previous PR (regarding the Equivalence a type [and I've also added Comparison a]), thank you so much for your patience with that!

[phadej]

I think that datatype providing packages should depend on type class packages. So it should rather be smash and these depending on universe-base.

As maintainer of these I'm slightly perplexed. I guess that can be added there behind the flag, similarly as assoc instances. Re smash I cannot comment.

---

Please don't use UnicodeSyntax, especially ℕ makes me want to ignore this issue.

[subttle]

Please don't use UnicodeSyntax, especially ℕ makes me want to ignore this issue.

In my defense, I did say I would remove the Unicode in the event a PR was welcomed, but I updated the issue for you anyway :)

I think that datatype providing packages should depend on type class packages. So it should rather be smash and these depending on universe-base.

As maintainer of these I'm slightly perplexed. I guess that can be added there behind the flag, similarly as assoc instances. Re smash I cannot comment.

So based on what you're saying I'm thinking I should then close this ticket for now then and open tickets with those packages. Thank you for the advice. Please feel free to reopen if there is anything else to add. Have a nice day!

[dmwit]

FWIW, my own personal opinion here is that if the other packages won't accept a new dependency+instance, it should be fine to make our own instances. Though the whole universe-instances-extended situation seems mildly odd to me; we probably ought to have one universe-* for each package we write orphans for, with, say, a single module named Data.Universe.Instances.*. A metapackage universe-instances-extended that depends on all of them--or some curated subset of them--and re-exports the instances from Data.Universe.Instances seems completely plausible in that alternate world.

[phadej]

universe-instances-extended can be as well named unvierse-instance-kmett-universe, I don't see a point of replicating that hierarchy.

Also, it would be nice if say universe-instances-smash is not maintained by us. I'd like if the maintenance burden would decrease over time, not increase.