Thanks for answers and sorry for goofy definitions and laws. I didn't think
it thoroughly enough.
In general I think I was looking for something slightly less powerful than
this CRDTs:
https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type
Basically I would like to find an algebraic structure which corresponds to
a versioned shared data-structure which can be synchronized using log
replication between multiple actors/applications/devices. Think if a
structure which can be used to synchronize chat room with messages or
friends list or notification panel content, etc. It should work over
intermittent connection, with a single source of truth (a server), can be
incrementally updated to the latest version based on some cached stale
version, etc. I think I need to think a bit more about this to find a
proper definitions and laws.
Cheers,
Gleb
On Tue, Apr 21, 2015 at 4:51 AM, Richard A. O'Keefe
You said in words that
Every S can be reconstructed from a sequence of updates:
but your formula
forall s. exists [a]. s == foldl update empty [a]
says that a (not necessarily unique) sequence of updates can be reconstructed from every S. I think you meant something like "there are no elements of S but those that can be constructed by a sequence of updates".
I'm a little confused by "a" being lower case.
There's a little wrinkle that tells me this isn't going to be simple.
type A = Bool newtype S = S [A]
empty :: S
empty = S []
update :: S -> A -> S
update o@(S (x:xs)) y | x == y = o update (S xs) y = S (y:xs)
reconstruct :: S -> [A]
reconstruct (S xs) = xs
Here update is *locally* idempotent: update (update s a) a == update s a But it's not *globally* idempotent: you can build up a list of any desired length, such as S [False,True,False,True,False], as long as the elements alternate.
Perhaps I have misunderstood your specification.