Transaction type safety

Question

I have a Transaction monad that looks like:

newtype Transaction t m a = .. my monad stack here ..

t is a phantom type I use to make sure the transactions I chain up apply to the same backend store.

My main loop's iteration uses a type like:

Transaction DB IO (Widget (Transaction DB IO ()))

The above type means: "A transaction that generates a UI Widget whose user inputs translate to transactions to execute".

Additionally, I have:

data Property m a = Property { get :: m a, set :: a -> m () }

which is extremely useful (especially due to its ability to compose with FCLabels.

I make an awful lot of use of Property (Transaction t m) to generate my transactions.

Now, I want the type system to guarantee that the Transaction that generates the Widget is a read-only transaction, and the transactions the widget generates are allowed to be read-write transactions.

Apparently, I could just add another phantom type to the transaction, but this has two problems:

• It would require explicit conversions from Transaction ReadOnly to Transaction ReadWrite or type-class hackery to allow monadic composition between read and write primitives. This I think I can solve.

• The Property data constructor, in order to contain the writer, always requires a read/write operation which would force the "m" to be a ReadWrite transaction. I would not be able to re-use a property in the context of both a read-write and a read-only transaction.

I am looking for a good way to get the above-mentioned type-safety without losing the above traits of the design.

Answer 1

If you want the type-checker to enforce a distinction between Read-Only and Read-Write transactions, then the two must necessarily be distinct types. Working from there, this solution presents itself:

data Property rm wm a = Property { get :: rm a, set :: a -> wm () }

There are a lot of variations of this approach. Instead of distinct monads, you could have a monad with different context parameters:

newtype Transaction t c m a = .. my monad stack here

data Property mc c1 c2 a = Property { get :: mc c1 a, set :: a -> mc c2 () }

Here mc is a monad constructor; it needs the context parameter to make a monad. Even though this uses more parameters, I prefer it because it emphasizes the similarities of the monads.

For functions that require reading or writing, consider using type classes.

newtype ReadOnly = ReadOnly

newtype ReadWrite = ReadWrite

class ReadContext rm where

class WriteContext rm where

instance ReadContext ReadOnly where
instance ReadContext ReadWrite where

instance WriteContext ReadWrite where

someGetter :: ReadContext c => Transaction t c m a

someSetter :: WriteContext c => a -> Transaction t c m ()

This should limit the amount of casts/lifting you need to do, while still enforcing type safety.