add instances for Equivalence, Op, and Predicate

[subttle]

PR for https://github.com/dmwit/universe/issues/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]

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