A DBVar m delta is a mutable reference to a Haskell value of type a . The type delta is a delta encoding for this value type a , that is we have a ~ Base delta .

The Haskell value is cached in memory, in weak head normal form (WHNF). However, whenever the value is updated, a copy of will be written to persistent storage like a file or database on the hard disk; any particular storage is specified by the Store type. For efficient updates, the delta encoding delta is used in the update.

Concurrency:

• Updates are atomic and will block other updates.
• Reads will not be blocked during an update (except for a small moment where the new value atomically replaces the old one).

Read the current value of the DBVar .

Update the value of the DBVar using a delta encoding.

The new value will be evaluated to weak head normal form.

Modify the value in a DBVar .

The new value will be evaluated to weak head normal form.

Maybe modify the value in a DBVar

If updated, the new value will be evaluated to weak head normal form.

Initialize a new DBVar for a given Store .

Create a DBVar by loading its value from an existing Store Throws an exception if the value cannot be loaded.

A Store is a storage facility for Haskell values of type a ~ Base da . Typical use cases are a file or a database on the hard disk.

A Store has many similarities with an Embedding . The main difference is that storing value in a Store has side effects. A Store is described by three action:

• writeS writes a value to the store.
• loadS loads a value from the store.
• updateS uses a delta encoding of type da to efficiently update the store. In order to avoid performing an expensive loadS operation, the action updateS expects the value described by the store as an argument, but no check is performed whether the provided value matches the contents of the store. Also, not every store inspects this argument.

A Store is characterized by the following properties:

• The store need not contain a properly formatted value : Loading a value from the store may fail, and this is why loadS has an Either result. For example, if the Store represents a file on disk, then the file may corrupted or in an incompatible file format when first opened. In such a case of failure, the result Left (e :: SomeException ) is returned, where the exception e gives more information about the failure.

  However, loading a value after writing it should always succeed, we have

  writeS s a >> loadS s  =  pure (Right a)

• The store is redundant : Two stores with different contents may describe the same value of type a . For example, two files with different whitespace may describe the same JSON value. In general, we have

  loadS s >>= either (const $ pure ()) (writeS s) ≠  pure ()

• Updating a store commutes with apply : We have

  updateS s a da >> loadS s  =  pure $ Right $ apply a da

  However, since the store is redundant, we often have

  updateS s a da  ≠  writeS s (apply a da)

• Exceptions : It is expected that the functions loadS , updateS , writeS do not throw synchronous exceptions. In the worst case, loadS should return Left after reading or writing to the store was unsuccessful.
• Concurrency : It is expected that the functions updateS and writeS are atomic : Either they succeed in updating / writing the new value in its entirety, or the old value is kept. In particular, we expect this even when one of these functions receives an asynchronous exception and needs to abort normal operation.

An in-memory Store from a mutable variable ( TVar ). Useful for testing.

$EitherSomeException

NOTE: [EitherSomeException]

In this version of the library, the error case returned by loadS and load is the general SomeException type, which is a disjoint sum of all possible error types (that is, members of the Exception class).

In a future version of this library, this may be replaced by a more specific error type, but at the price of introducing a new type parameter e in the Store type.

For now, I have opted to explore a region of the design space where the number of type parameters is kept to a minimum. I would argue that making errors visible on the type level is not as useful as one might hope for, because in exchange for making the types noisier, the amount of type-safety we gain is very small. Specifically, if we encounter an element of the SomeException type that we did not expect, it is entirely ok to throw it. For example, consider the following code: let ea :: Either SomeException () ea = [..] in case ea of Right _ -> "everything is ok" Left e -> case fromException e of Just (AssertionFailed _) -> "bad things happened" Nothing -> throw e In this example, using the more specific type ea :: Either AssertionFailed () would have eliminated the need to handle the Nothing case. But as we are dealing with exceptions, this case does have a default handler, and there is less need to exclude it at compile as opposed to, say, the case of an empty list.

Failure that occurs when calling loadS on a newStore that is empty.

Combine two Stores into a store for pairs.

WARNING: The updateS and writeS functions of the result are not atomic in the presence of asynchronous exceptions. For example, the update of the first store may succeed while the update of the second store may fail. In other words, this combinator works for some monads, such as m = STM , but fails for others, such as m = IO .

Obtain a Store for one type a1 from a Store for another type a2 via an Embedding' of the first type into the second type.

Note: This function is exported for testing and documentation only, use the more efficient embedStore instead.