add instances for Equivalence, Op, and Predicate

[subttle]

PR for #44

Please let me know if you would like anything done differently, I will gladly make changes. Thank you for considering this PR.

[subttle]

Oh I need to add a conditional import for Applicative to support GHC <= 7.8.4. :)

[dmwit]

LGTM, up to Travis complaints I guess.

[phadej]

This is not right.

See https://oleg.fi/gists/posts/2019-06-03-compat-packages.html#s:3

[phadej]

what is Bell number, add a reference

[subttle]

I like the wolfram.com definition.

Suggested change

	where -- Compute the Bell number for the given cardinality.
	where -- Compute the Bell number for the given cardinality.
	-- The Bell number is the "number of ways a set of n elements can be partitioned into nonempty subsets"
	-- http://mathworld.wolfram.com/BellNumber.html

Do you think it is also worth stating somewhere the relation between equivalences and partitions? E.g.:
https://proofwiki.org/wiki/Fundamental_Theorem_on_Equivalence_Relations
https://proofwiki.org/wiki/Relation_Induced_by_Partition_is_Equivalence
Wikipedia says it nicely as:
"there is a natural bijection between the set of all possible equivalence relations on X and the set of all partitions of X"
And it is that bijection which enables the Bell number to compute the cardinality.
If you would like that in the comment, perhaps this is better:

Suggested change

	where -- Compute the Bell number for the given cardinality.
	where -- Compute the Bell number for the given cardinality.
	-- The Bell number is the "number of ways a set of n elements can
	-- be partitioned into nonempty subsets"
	-- http://mathworld.wolfram.com/BellNumber.html
	--
	-- https://en.wikipedia.org/wiki/Equivalence_relation#Fundamental_theorem_of_equivalence_relations
	-- The Fundamental Theorem on Equivalence Relations says, a natural
	-- bijection between the set of all possible equivalence relations
	-- on X and the set of all partitions of X, and said bijection
	-- enables the Bell number to be used for computing the `cardinality`.

Not sure if someone would like to state that (or something similar) more elegantly, but I think that provides good information to anyone who reads the code and wants to know why bell is used in computing the cardinality.

[phadej]

This implementation needs a commentary.

I have hard time convincing myself it's correct, thus I'd error on the fact, that it's probably wrong in some corner case. Help me.

[dmwit]

Some commentary:

Here's how we enumerate all the equivalence relations for a set X. First we choose an arbitrary element of X. Call it x. Then the equivalence relation can be described in two parts:

1. The equivalence class of x, that is, the set of elements which is equivalent to x. (This is required to contain x.)
2. The equivalence relation on all the elements not equivalent to x, which we compute recursively in the same way.

For each piece, we simply nondeterministically choose from among all possibilities. To efficiently track equivalence classes, we choose a fresh number to identify each class, and make a Map from elements of X to the identity of their class.

These ideas should shine through pretty clear in the code once you have them in mind:

-- choose an arbitrary element x of the set X, and set xs = X \ {x}
go n (x : xs) = do
    -- choose a subset eq of xs to be equivalent to x, and set notEq = xs \ eq
    (eq, notEq) <- partitionA (const [False, True]) xs
    -- recursively cook up an equivalence relation on the leftovers, bumping the class identifier up by one
    rest        <- go (n + 1) notEq
    -- map x and all the elements of eq to the current class identifier
    pure $ M.fromList [(x', n) | x' <- x : eq] `M.union` rest

It is okay to use the boring old list monad instead of our fancy helpers because everything involved here is finite.

[phadej]

These comments should be in a implementation.

What's the guarantee that [Equivalence a] doesn't contain same elements, i.e its' cardinality is correct. Still have to think too hard.

A test for 3/4/5 element sets would be 👍, (it turns out that Bell number is a count of partitions of a set)

Also if partitionA works so that it returns empty eq, will the first element of universe :: [Equivalence a] be Equivalence (==). If so, it could be checked as well.

Maybe there should be a big warning on this instance, as Bell numbers grow relatively fast/.

[dmwit]

These comments should be in a implementation.

No objection.

What's the guarantee that [Equivalence a] doesn't contain same elements

The usual (strong) inductive one: the call to partitionA doesn't return any duplicate equivalence classes for x, and by induction there are no duplicate equivalence relations in rest. I think this one is not even worth writing down.

[phadej]

See https://github.com/dmwit/universe/pull/47/files, adding such doctest would convince me (and readers of documentation) that this works. Using something like Three to demonstrate various Equivalence would be IMHO neat thing!

[phadej]

I merged Op and Predicate. This PR (probabably) does conflict now. I can take over it too (but not soon)

[subttle]

Nice! Thank you for that. I can certainly do it, I just won't be able to get to it right away, unfortunately. Realistically I could maybe have it done by next weekend. I realize of course it's not a big task, I just have a lot of work at the moment. No worries about having the conflict. :)

[subttle]

Thank you for your patience, it is much appreciated :)

A small update, I worked on this a bit today and finally have a reference for the topic:
"section 7.2.1.5: Generating all set partitions" from Donald Knuth's The Art of Computer Programming, (Fascicle 3B, Page 28):
https://www-cs-faculty.stanford.edu/~knuth/fasc3b.ps.gz
Up until now I could only find one reference for an actual algorithm and it was behind a paywall so I hadn't bothered.

I am curious to try a new approach which would reuse code from the Predicate a instances and see how efficient it would turn out. If time is of the essence for this PR, by all means @phadej you should take over but if not, I don't mind continuing work :)

P.S.: There are some more fascicles from Knuth which may be of use here too:
http://www.cs.utsa.edu/~wagner/knuth/

[phadej]

@subttle any progress?

[subttle]

Yes, I had a few mindblowingly busy months at work but I actually have a weekend to work on this coming up and I have a great idea of how I want to implement it :D

[subttle]

Update: I haven't been able to implement it yet but my experimenting has been very rewarding. I was thinking about the bitstring representation for any given Finite a => Predicate a.

type Fin₄ = Fin Nat.Nat4

bits :: (Finite a) ⇒ Predicate a → String
bits (Predicate p) = fmap (toBit . p) universeF
  where
    toBit :: Bool → Char
    toBit False = '0'
    toBit True  = '1'

λ> let equivs = [[[0],[1],[2],[3]],[[0],[1],[2,3]],[[0],[1,3],[2]],[[0,3],[1],[2]],[[0],[1,2],[3]],[[0],[1,2,3]],[[0,3],[1,2]],[[0,2],[1],[3]],[[0,2],[1,3]],[[0,2,3],[1]],[[0,1],[2],[3]],[[0,1],[2,3]],[[0,1,3],[2]],[[0,1,2],[3]],[[0,1,2,3]]] :: [[[Fin₄]]]
λ> fmap (fmap (Predicate . flip elem)) equivs
[[1000,0100,0010,0001],[1000,0100,0011],[1000,0101,0010],[1001,0100,0010],[1000,0110,0001],[1000,0111],[1001,0110],[1010,0100,0001],[1010,0101],[1011,0100],[1
100,0010,0001],[1100,0011],[1101,0010],[1110,0001],[1111]]
λ> mapM_ print it`
[1000,0100,0010,0001]
[1000,0100,0011]
[1000,0101,0010]
[1001,0100,0010]
[1000,0110,0001]
[1000,0111]
[1001,0110]
[1010,0100,0001]
[1010,0101]
[1011,0100]
[1100,0010,0001]
[1100,0011]
[1101,0010]
[1110,0001]
[1111]
λ> 

Here each line represents a partitioning whose union makes up a whole. For example, [1000,0100,0010,0001] would be {0},{1},{2},{3} while [1111] would be {0,1,2,3}. And furthermore:
[1000,0111] (=0), (≠0)
[1011,0100] (≠1), (=1)
[1101,0010] (≠2), (=2)
[1110,0001] (≠3), (=3)

And then all of the lines together make up all possible partitions.
I think for this example in particular it is perhaps better to think in terms of Predicates using ≤ which makes it more obvious that there is a bounded join-semilattice.

-- 1000
lteq0 :: Predicate Fin₄
lteq0 = Predicate (≤ 0)

-- 1100
lteq1 :: Predicate Fin₄
lteq1 = Predicate (≤ 1)

-- 1110
lteq2 :: Predicate Fin₄
lteq2 = Predicate (≤ 2)

-- 1111
lteq3 :: Predicate Fin₄
lteq3 = Predicate (≤ 3)

meaning we could also of course think of
[1000,0111], for example, to be the set consisting of the two predicates (≤0), (≰0), etc.

Now I will just think out loud to myself (I'm not asking anyone questions in particular, I'm just sharing my current thought process).
There are some really interesting patterns to be found there involving complements (maybe turning Predicate a into a Group? I'm sure I'll figure that out) and also I'm currently thinking it might be interpreted with some sort of derivative, but I will say for sure when I am done with my current experiment. For the derivative(ish?) aspect, I was thinking there would be a way to exploit the relationship:

-- N.B. `Equivalence` has laws!
convert ∷ Predicate (a, a) → Equivalence a
convert (Predicate p) = Equivalence (curry p)

where I can just fix different parts at a time.

I will try to make more time this week (hopefully in the next few days) to finish up here, but if not I will continue to update! Thanks for your patience!

I don't know what to make of these slides yet, but it might be useful for me:
http://users.cecs.anu.edu.au/~jon/grayslides.pdf