Data.Columbia.Theory

Here are some equivalences that explain how Columbia operations work. The ~== equivalence operator means equivalence under the object graph relation, and does not pay attention to addresses of data. These are moral equivalences and do not hold in the presence of interference with lock files or failure to lock. The object graph relation defines two Columbia files as equivalent iff the co-recursively structures built by traversing them are co-inductively equal.

• Assuming do { f d; m } ~== do { f d; return d }

do { writeOneLayer proxy f d; readOneLayer proxy m } ~== do { writeOneLayer proxy f d; return d }

• Assuming do { d <- m; f d } ~== return()

do { d <- readOneLayer proxy m; writeOneLayer proxy f d } ~== return()

• Assuming do { f d; f d } ~== f d

do { writeOneLayer proxy f d; writeOneLayer proxy f d } ~== writeOneLayer proxy f d

that is writeOneLayer is idempotent with regard to the object graph/term structure.

• Assuming effect m is non-observable, readOneLayer proxy m is also non-observable.
• For a strategy s that reads or writes,

do { n <- getWriterPosition; s; seekWriter n } == s,

That is well-behaved read/write strategies leave the stream seeked the way they found it.

Through co-inductive equality reasoning, it can be deduced that:

do { writeCompoundData d; readCompoundData } ~== do { writeCompoundData d; return d }

and

do { d <- readCompoundData; writeCompoundData d } ~== return()

because readCompoundData is just fixT rwProxy readOneLayer (similarly writeCompoundData).

• -----------------------------------------

withAddresses and writeBackAddresses are each equivalent to the identity where the type they work at is not an application of WithAddress type constructor.