<div dir="ltr">Thanks for answers and sorry for goofy definitions and laws. I didn't think it thoroughly enough.<div><br></div><div>In general I think I was looking for something slightly less powerful than this CRDTs:<br><div><a href="https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type">https://en.wikipedia.org/wiki/Conflict-free_replicated_data_type</a><br></div><div><br></div><div>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.</div></div><div><br></div><div>Cheers,</div><div>Gleb</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 21, 2015 at 4:51 AM, Richard A. O'Keefe <span dir="ltr"><<a href="mailto:ok@cs.otago.ac.nz" target="_blank">ok@cs.otago.ac.nz</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You said in words that<br>
<span class=""><br>
> Every S can be reconstructed from a sequence of updates:<br>
<br>
</span>but your formula<br>
<span class=""><br>
>     forall s. exists [a]. s == foldl update empty [a]<br>
<br>
</span>says that a (not necessarily unique) sequence of updates<br>
can be reconstructed from every S.  I think you meant<br>
something like "there are no elements of S but those<br>
that can be constructed by a sequence of updates".<br>
<br>
I'm a little confused by "a" being lower case.<br>
<br>
There's a little wrinkle that tells me this isn't going to<br>
be simple.<br>
<br>
type A = Bool<br>
newtype S = S [A]<br>
<br>
empty :: S<br>
<br>
empty = S []<br>
<br>
update :: S -> A -> S<br>
<br>
update o@(S (x:xs)) y | x == y = o<br>
update   (S xs) y              = S (y:xs)<br>
<br>
reconstruct :: S -> [A]<br>
<br>
reconstruct (S xs) = xs<br>
<br>
Here update is *locally* idempotent:<br>
update (update s a) a == update s a<br>
But it's not *globally* idempotent:<br>
you can build up a list of any desired length,<br>
such as S [False,True,False,True,False],<br>
as long as the elements alternate.<br>
<br>
Perhaps I have misunderstood your specification.<br>
<br>
</blockquote></div><br></div>