Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

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 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

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 .

AntidoteDB has 27 repositories available. Follow their code on GitHub.

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 :)

Implementing collaboration tools (issue tracker, code reviews, and more) in Radicle Collaboration data representation: the merge problem By “collaboration tools” we initially mean an issue tracker and a code review system. Over time more tools could be added (like a wiki, a more complex CMS, a project tracking system…). The implementation strategy is to build these tools on top of git. This means handling git as a database which the tools use as backing storage. Since the tools are collabora...

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

A JSON-like data structure (a CRDT) that can be modified concurrently by different users, and merged again automatically. - 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

CRDT implementations to use with Antidote. Contribute to AntidoteDB/antidote_crdt development by creating an account on GitHub.

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

Riak is a decentralized datastore from Basho Technologies. - 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