denotational automerge

denotational_automerge.hs

type OpSet
type Op
type Value = Map Id (Either (Seq ElemId Elem) (Map Key ShallowValue))
type Map k v
type Seq
type Register = Map Id (Either Id Primitive)
type ElemId = Either Head Id
type Elem = ShallowValue
type ShallowValue = Register
type Primitive
type Key
type Id
type Property = Either Key Nat

-- Map
insert : k -> v -> Map k v -> Map k v

-- OpSet
view : Id -> Property -> OpSet -> Optional Value
update : Id -> Property -> Value -> OpSet -> Optional (Id, OpSet)
delete : Id -> Property -> OpSet -> OpSet
merge : OpSet -> OpSet -> OpSet
empty : OpSet
frontier : OpSet -> OpSet -- alternative, frontier : OpSet -> Frontier

id, prop, value, opset => view (update id prop value opset) === Some value

id, prop, opset => view id prop (delete id prop opset) === None

id, prop, value, opset => frontier (delete id prop (update id prop value opset)) === frontier opset

id, prop, value, opset =>
  frontier (update id prop value (update id prop value opset)) === frontier (update id prop value opset)

id, id', prop, value, opset =>
  frontier (update id' prop value (update id prop value opset)) === frontier (update id' prop value opset)

id, id', prop, prop', value, value', opset, opset' =>
  let merged = merge (update id prop value opset) (update id' prop' value' opset'))
  (view id prop merged === Some value) && (view id' prop' merged === Some value')

opset => frontier (frontier opset) === frontier opset

opset => merge opset (frontier opset) === opset -- not sure about this being implementable

opset, id, prop => merge (frontier (delete id prop opset)) opset === undefined

opset, f => merge (frontier f opset) opset === f (merge (frontier opset) opset)?????

opset, f => merge (f opset) opset === f opset

opset, opset', f => merge (f opset) opset' === f (merge opset opset')
opset, opset', f => merge opset (f opset') === f (merge opset opset')

--- Monoid + Semilattice
x => merge empty x === x
x => merge x empty === x
x, y, z => merge (merge x y) z === merge x (merge y z)
x, y => merge x y === merge y x
x => merge x x === x

-- Seq
view : OpSet -> Nat -> Seq -> Optional ShallowValue
update : OpSet -> Nat -> ShallowValue -> Seq -> Optional Seq
delete : OpSet -> Nat -> Seq -> Seq

-- Registers
read : OpSet -> Register -> Map Id (Either Id Primitive)

insert : Id -> Either Id Primitive -> Register -> Register
insert = Map.insert

delete : Id -> Register -> Register

merge : Register -> Register -> Register

-- Id
(>) : Id -> Id -> Id

-- Op
findPredecessors : Id -> OpSet -> Optional [Op]
findPredecessors id set = find id set <$> predecessors

find : Id -> OpSet -> Optional Op
predecessors : Op -> [Op]