lwwmap.hs

lwwmap.hs

{-
RGA + LWW + Counter -- combining we get Automerge!

So let's start with a List CRDT.
-}

type LWWMap

set :: Key -> Value -> LWWMap -> LWWMap
delete :: Key -> LWWMap -> LWWMap
merge :: LWWMap -> LWWMap -> LWWMap
empty :: LWWMap

observe :: LWWMap -> Map Key {Value}

sequential/set/delete :: forall (k :: Key) (v :: Value) (m :: LWWMap).
  observe (set k v (delete k m)) === observe (set k v m)

sequential/delete/set :: forall (k :: Key) (v :: Value) (m :: LWWMap).
  observe (delete k (set k b m)) === observe m

concurrent/set/delete :: forall (k :: Key) (v :: Value) (m :: LWWMap).
  observe (merge (set k v m) (delete k m)) === observe (set k v m)

concurrent/delete/set :: forall (k :: Key) (v :: Value) (m :: LWWMap).
  observe (merge (delete k m) (set k v m))
  ==> observe (merge (set k v m) (delete k m)) -- mergeCommutes
  ==> observe (set k v m) -- concurrent/set/delete

sequential/set/set :: forall (k :: Key) (v1 :: Value) (v2 :: Value) (m :: LWWMap).
  observe (set k v1 (set k v1 m)) === observe (set k v2 m)

concurrent/set/set :: forall (k :: Key) (v1 :: Value) (v2 :: Value) (m :: LWWMap).
  observe (merge (set k v1 m) (set k v2 m)) === Map.insert k {v1, v2} (observe m)

observeSet :: forall (k :: Key) (v :: Value) (m :: LWWMap).
  observe (set k v m) === Map.insert k {v} (observe m)

observeDelete :: forall (k :: Key) (m :: LWWMap).
  observe (delete k m) === Map.delete k (observe m)

mergeCommutes :: forall (m1 :: LWWMap) (m2 :: LWWMap).
  merge m1 m2 === merge m2 m1

mergeIdentity :: forall (m :: LWWMap).
  merge m empty === m

mergeAssoc :: forall (m1 :: LWWMap) (m2 :: LWWMap) (m3 :: LWWMap).
  merge m1 (merge m2 m3) === merge (merge m1 m2) m3

observeEmpty :: .
  observe empty === Map.empty