Store represents a facility for storing one value of a given type. Typically, this type is a collection type, for example Map Integer String, so that we actually stores multiple values.

The key benefit of a Store is that it can store the value outside of volatile memory (RAM) — for example, the value can be stored in a database file on disk, that is on persistent storage.

• Read-access is done on parts of the value, through a query GADT that is an instance of the Query class. In this way, we do not need to load the stored value fully into volatile memory.
• Updates are incremental and use delta types, see Data.Delta. In this way, we can modify the persistent storage incrementally.

Conversely, there is no need to use Store if the value only ever lives in volatile memory — in this case, it is much simpler to use a plain Haskell value, introduced with let, where, or as a function argument.

Any implementation of Store is expected to satisfy the properties specified in this section. We make no attempt at enforcing these properties on the type-level. However, the module Test.Store provides QuickCheck code for these properties for automated testing.

The most fundamental operations on a Store are

• loadS — loads the value contained in the Store into memory.
• writeS — writes a value from memory into the Store.

These two operations are characterized by the following design:

1. 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)

2. The store is redundant.

   Two stores with different internal contents may contain the same value of type a. For example, two files with different whitespace may describe the same JSON value. In general, loading a value and writing it again may change the internal store contents, i.e.

   loadS s >>= either (\_ -> pure ()) (writeS s)  ≠  pure ()

In order to update the store content without loading all of it into memory, Store supports the operation

• updateS — updates the value contained in the Store using a Delta type.

This operation is characterized by the following law:

• Updating a store commutes with apply.

  We have

  updateS s (Just a) da >> loadS s  =  pure $ Right $ apply a da

  However, since the store is redundant, we often have

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

The combination of loadS, writeS, updateS has many similarities with an Embedding of delta types. However, the main difference is that manipulating a Store involves side effects.

In order to query parts of the store content without loading all of it into memory, Store supports the operation

• queryS — run a specialized Query on the value contained in the Store.

This operation is characterized by the following law:

• Querying a store commutes with query:

   ∀q. query q <$> (loadS s >>= either throw pure)  =  queryS s q

The monad m in Store m da provides the storage space for the value. Put differently, we like to think of m as a State monad whose state contains the value. However, this monad m could have additional side effects such as exceptions, concurrency, non-determinism, and so on. We would have to specify how a Store should behave with regards to these effects, which complicates matters significantly. (In fact, the equality sign = for the laws above has to be interpreted "… equal effects as far as the Store is concerned". A proper approach to a specification would involve Hoare logic.)

For simplicity, we now assume that the monad m only has the effects state and exceptions — we make no attempt at specifying how an implementation should behave for concurrent usage of, say, updateS. This assumption ensures some composability of the Store abstraction. However, it also implies that choosing m ~ STM results in specified semantics, whereas choosing m ~ IO can result in unspecified behavior. (TODO: Perhaps create a type class MonadSequential to keep track of this on the type level?)

More specifically, the interaction between Store functions and effects are as follows:

• State: The laws presented above specify the essentials of how the store state changes. However, this specification is not complete, other "expected" rules such as

  writeS s a >> writeS s b  =  writeS s b

  etc. should also hold.

• Exceptions:

  • loadS should not throw a synchronous exception, but return Left instead.
  • queryS should throw a synchronous exception iff loadS returns Left. Moving the error case into the monad m simplifes the use of this operation.
  • writeS and loadS should not throw synchronous exceptions. However, in case they do throw an exception, the contents of the Store should be treated as corrupted, and loadS should return Left subsequently.

• Concurrency: We do not specify behavior under concurrent operation. Concurrent access to a Store is a frequent desideratum — but you will have to implement it yourself.

  One design pattern is to use a custom monad m ~ MyMonad that has a way of executing state changes atomically,

  atomically :: MyMonad a -> IO a

  Specifically, atomically either applies all state changes, or none of the state changes. For instance, SQL transactions can be used for this, see e.g. https://www.sqlite.org/lang_transaction.html. Then, you can implement a Store MyMonad by composing smaller Store, and use atomically in a scope where you want to use the Store rather than implement it.

  Use hoistStore atomically to map a Store MyMonad to a Store IO where the monad has less atomicity.

• Non-determinism or other effects: Here be dragons.

The function updateS applies a delta to the content of the Store. Depending on the implementation of the Store, this operation may require large parts of the content to be loaded into memory, which is expensive. In some use cases such as DBVar, the value is already available in memory and can be used for executing the update. For these cases, the first argument of updateS may provide the in-memory value. We expect that the following property holds:

  updateS s Nothing da
=
  loadS s >>= \(Right a) -> updateS s (Just a) da

The helper loadWhenNothing is useful for handling this argument.

In the error case that the store does not contain a value, loadS returns a Left value of type SomeException. This type is a disjoint sum of all possible error types (that is, members of the Exception class).

We could parametrize Store by an additional type parameter e representing the possible error cases. However, we have opted to explore a region of the design space where the number of type parameters is kept to a minimum.

In fact, I would argue that making errors visible on the type level is not very useful: we add much noise to the type level, but we gain little type-safety in exchange. Specifically, if we encounter an element of the SomeException type that we did not expect, we can always 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 Nothing case. However, this case has the sensible default value: throw e, we rethrow the exception that we did not expect. Ruling out this case on the type-level adds almost no value.