semitlattices - Haskell

So I've been looking at CRDTs and one of the versions of them is a join-semilattice. One of the data structures I'm looking at is basically Cofree. So I did some playing around and wrote an instance for a join-semilattice for ZipList and used checkers to check the laws. I believe that Cofree will also have an instance if f is an Applicative and also forms a semilattice. I can't seem to use checkers to check this because I think I run into generating infinite ZipList :sob:. Can a big brain in here help me figure this out or confirm my intuition is correct? Here's the code:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Control.Applicative (ZipList(..), liftA2)
import Control.Comonad.Cofree
import Data.Functor.Classes (Eq1, Show1)
import Data.Semilattice.Join
import Test.QuickCheck
import Test.QuickCheck.Checkers

instance (Join a) => Join (ZipList a) where
  as \/ bs = liftA2 (\/) as bs

instance Eq a => EqProp (ZipList a) where
  (=-=) = eq

deriving instance Show1 ZipList
deriving instance Eq1 ZipList

instance (Applicative f, Join a) => Join (Cofree f a) where
  (a :< as) \/ (b :< bs) = a \/ b :< liftA2 (\/) as bs

instance (Arbitrary1 f, Arbitrary a) => Arbitrary (Cofree f a) where
  arbitrary = do
    a <- arbitrary
    f <- arbitrary1
    pure (a :< f)

instance (Eq1 f, Eq a) => EqProp (Cofree f a) where
  (=-=) = eq

-- Check idempotence
idempotence :: Property
idempotence = idempotent2 @(Cofree ZipList Ordering) (\/)

-- Check associativity

-- Check commutativity

-- Check idempotence
-- idempotent :: (Show a, Arbitrary a, EqProp a) => (a -> a) -> Property
idempotenceZL :: Property
idempotenceZL = idempotent2 @(ZipList Ordering) (\/)

-- Check commutativity
commutativityZL :: Property
commutativityZL = isCommut @(ZipList Ordering) (\/)

-- Check associativity
associativityZL :: Property
associativityZL = isAssoc @(ZipList Ordering) (\/)

Running quickBatch ("semilattice", [("idempotence", idempotence)]) in ghci will hang

my guess is that those deriving instances are giving you infinite loops

nevermind, you should derive the newtype instances

pure blah :: ZipList blah is an infinite list

which i guess means equality will never terminate

likewise for your equality Cofree instance

Right that's what I was thinking was the case. Is there another way to prove the laws hold?

make a newtype that doesn't get bigger than 10 elements inside a zip list?

To be honest, I think I might need something a little bit more nuanced than a ziplist anyway. If two users make concurrent edits they should resolve if they're distinct.
So if they both start off with [a,b] and then Bob adds c and Alice adds d, I'd like to end up with either [a,b,c,d] or [a,b,d,c].

prove they hold for that and then induction

Sounds like a big brain idea

newtype ZipListButIt's10 a

i feel like we don't use apostrophes in names often enough

https://www.stackage.org/haddock/lts-15.1/lens-4.18.1/Control-Lens-Combinators.html#v:isn-39-t this is the only one i can think of

I feel we do it too often :stuck_out_tongue:

Ya that's the one I'm thinking of :joy:

Do you mind if I ask why you are looking into CRDTs? I only ask because I was thinking it would be fun to work on a Haskell client for antidote db https://github.com/antidotedb .

Sup @Jonathan Lorimer! I'm looking into CRDTs because I'm working on a decentralized project https://radicle.xyz/. You can check out our conversations so far: https://radicle.community/t/radicle-collaboration-tools/105.
We just had a conversation this morning and I think we came to a conclusion which I'll do a write up summarising it all. I'll link that when it's up :)

Haven't heard of antidote. I did come across this though https://github.com/automerge/automerge

Do you know what kind of CRDTs are used on the backend of antidote?

https://github.com/AntidoteDB/antidote_crdt here is the repo for it

I also know that riak is another distributed db written in erlang and based on CRDTs, but it is noSQL

https://github.com/basho/riak

Ah I see! Well we're gonna go the op-based route. There's a chance we may roll our own but have to see yet