Equivalence a Type

[subttle]

Hi, I think this project is really great, thank you for all the work you do on it!

I had an idea which I think is worth mentioning. Going with the description of "... for types where we know all the values" I think their is a good case for Finite a => Finite (Equivalence a) (the Equivalence a type being from http://hackage.haskell.org/package/contravariant-1.5/docs/Data-Functor-Contravariant.html#t:Equivalence). But I'm not sure if that is too specific for your library.

For the cardinality I think if you wanted to avoid computing universeF to get the length you could just compute the corresponding Bell number:
https://en.wikipedia.org/wiki/Equivalence_relation#Counting_possible_partitions

To actually generate the list of partitions I've been using:

-- partitions of a set
-- partitions {0..2} = [ [[0],[1],[2]]
--                     , [[0],[2,1]]
--                     , [[2,0],[1]]
--                     , [[1,0],[2]]
--                     , [[2,1,0]]
--                     ]
partitions ∷ (Foldable t) ⇒ t a → [[NonEmpty a]]
partitions = Foldable.foldl (\xs → (xs >>=) . go) [[]]
   where go ∷ a → [NonEmpty a] → [[NonEmpty a]]
         go x []       = [[ x :| [] ]]
         go x (y : ys) = fmap (y :) (go x ys) <> [(x :| NE.toList y) : ys]

And then just in case you are interested here are the helper functions:

-- for each list (which represents an equivalence class), check if both a₁ and a₂ are in it
-- if for any list two are in the same list return true, otherwise false
toEquivalence ∷ (Finite a, Foldable t) ⇒ t (NonEmpty a) → Equivalence a
toEquivalence parts = Equivalence (\a₁ a₂ → any (\xs → (a₁ `elem` xs) && (a₂ `elem` xs)) parts)

fromEquivalence ∷ ∀ a . (Finite a) ⇒ Equivalence a → [NonEmpty a]
fromEquivalence (Equivalence r) = unfoldr go universeF
      where go ∷ [a] → Maybe (NonEmpty a, [a])
            go []       = Nothing
            go (x : xs) = Just (x :| p, np)
                    where (p, np) = List.partition (r x) xs

So then for the Finite instance, you would potentially be able to do something like:

  universeF ∷ [Equivalence a]
  universeF = fmap toEquivalence (partitions universeF)

Fair warning, I haven't written any of this with performance in mind, but I still think the idea is worth mentioning. If you don't see a use for it please close the ticket I would not take offense!

Have a nice day!

[phadej]

An Finite a => Finite (Equivalence a) instance would fit universe-universe-extended, as well as instances for Op and Predicate (Comparison would be tricky to do).

An implementation using Ord a would be preferable. If a is Finite, for sure it's Ord too (or can be Orded).
E.g. we have (Finite a, Ord a, Universe b) => Universe (a -> b).

PR welcome.

[subttle]

Hi, I had some time to implement the Equivalence a part this weekend, so I'm just giving a quick update.

I had to add an Eq a constraint so it is now:
instance (Finite a, Eq a) => Finite (Equivalence a)

Also, I typically prefer to use NonEmpty lists where possible, especially if I'm going to use head and last which I ended up doing for the bell function:

        cardinality = Tagged (bell (genericLength (universeF :: [a])))
              where bell :: Natural -> Natural
                    bell n = NE.head (nth n (\ns -> NE.scanl1 (+) (NE.last ns NE.:| NE.toList ns)) (1 NE.:| []))
                       where nth n = foldr (.) id . replicate (fromIntegral n)

But I can of course just refactor NonEmpty a to [a] once I know the NonEmpty a version works.
As far as dependencies go, would you prefer I depend on the contravariant package or base-4.12.0.0 and similarly semigroups or base-4.9.0.0 (or I can refactor as I mentioned). Currently the cabal file for universe-instances-extended has the dependency set to base >=4.3 && <4.13
Please just let me know what you prefer, thanks!

[dmwit]

Can we use cardinality instead of genericLength universeF, please? (That's what it's for!) Also genericReplicate instead of replicate (fromIntegral n) -- we choose correctness over speed everywhere else in this library. Yes, it's ridiculous to use this instance for types where the difference matters; but that should be the user's dumb choice to make, not ours. ;-)

I think 4.9 is recent enough (Jan 2017) that it would be desirable to do a tiny bit of CPP so that we can support both before and after smoothly.

[subttle]

@phadej I apologize because I thought you meant for the Ord constraint to be for the Predicate instance (so I could use Data.Set for an efficient implementation), I hadn't realized I should've tried that for Equivalence too otherwise I would have tried that approach before posting! Thankfully, @dmwit helped me make the improvement :)

Also, I made the changes noted in the previous comment, I had meant to substitute in the cardinality but I am admittedly a Data.Tagged novice, but I think I understand the basics now. I ran some checks to make sure I had it right:

> cardinality :: Tagged (Equivalence Ordering) Natural
Tagged 5
> cardinality :: Tagged (Equivalence (Maybe Ordering)) Natural
Tagged 15
> cardinality :: Tagged (Equivalence (Maybe (Maybe Ordering))) Natural
Tagged 52

Here is the progress:
subttle@a4a3d55

Unless you have other feedback, I'll move on to Predicate next!

• Equivalence
• Predicate
• Op
• Testing