Control.Monad.Cell.Class

Are you just trying to use the library? If so, the contents of this module shouldn't matter to you, so feel free to head straight over to the main Data.Holmes module instead!

A cell is the unit of storage in a propagator network. We can think of it as "a description of a value", which is refined over the course of a computation. Because we're functional programmers, the described value is referentially transparent and pure: a cell's description must always be of the same value, and it can't change during the course of a computation.

Instead of functions from one cell to another, we should try to think about relationships between cells. Addition, for example, could be seen as a function with two inputs, but it could also be seen as a relationship between three values: the two components and their sum. The reason why this helps us is that we might very well, for whatever reason, learn the sum before we learn both of the inputs. In these cases, it's useful to allow information to flow in multiple direcitons. Why restrict ourselves to the one-way flow of input-to-output when we can happily re-arrange equations on paper?

Once we've built up our vocabulary for relationships, we just need a way to lift them over cells. Intuitively, we should think of all relationships as invariants. As cells' values are refined, these relationships are constantly re-evaluated, and any new information can be spread around the network to trigger, we hope, more learnings that bring us closer to a solution.

The MoriarT type provides a good reference implementation for this interface, so head over there to see how we can use the class to implement ideas like provenance and backtracking.

Documentation

class Monad m => MonadCell (m :: Type -> Type) where

The DSL for network construction primitives. The following interface provides the building blocks upon which the rest of the library is constructed.

If you are looking to implement the class yourself, you should note the lack of functionality for ambiguity/searching. This is deliberate: for backtracking search (as opposed to truth maintenance-based approaches), the ability to create computation branches dynamically makes it much harder to establish a reliable mechanism for tracking the effects of these choices.

For example: the approach used in the MoriarT implementation is to separate the introduction of ambiguity into one definite, explicit step, and all parameters must be declared ahead of time so that they can be assigned indices. Other implementations should feel free to take other approaches, but these will be implementation-specific.

Associated Types

data Cell m :: Type -> Type

The type of cells for this particular implementation. Typically, it's some sort of mutable reference (STRef, IORef, or similar), but the implementation may attach further metadata to the individual cells.

Methods

discard :: m x

Mark the current computation as failed. For more advanced implementations that utilise backtracking and branching, this is an indication that we should begin a different branch of the search. Otherwise, the computation should simply fail without a result.

fill :: x -> m (Cell m x)

Create a new cell with the given value. Although this value's type has no constraints, it will be immutable unless it also implements Merge, which exists to enforce monotonic updates.

watch :: Cell m x -> (x -> m ()) -> m ()

Create a callback that is fired whenever the value in a given cell is updated. Typically, this callback will involve potential writes to other cells based on the current value of the given cell. If such a write occurs, we say that we have propagated information from the first cell to the next.

with :: Cell m x -> (x -> m ()) -> m ()

Execute a callback with the current value of a cell. Unlike watch, this will only fire once, and subsequent changes to the cell should not re-trigger this callback. This callback should therefore not be "registered" on any cell.

write :: Merge x => Cell m x -> x -> m ()

Write an update to a cell. This update should be merged into the current value using the '(Data.JoinSemilattice.Merge.<<-)' operation, which should behave the same way as '(<>)' for commutative and idempotent monoids. This therefore preserves the monotonic behaviour: updates can only refine a value. The result of a write must be more refined than the value before, with no exception.

Instances

MonadCell Holmes

Defined in Control.Monad.Holmes

Associated Types

data Cell Holmes a :: Type

Methods

discard :: Holmes x

fill :: x -> Holmes (Cell Holmes x)

watch :: Cell Holmes x -> (x -> Holmes ()) -> Holmes ()

with :: Cell Holmes x -> (x -> Holmes ()) -> Holmes ()

write :: Merge x => Cell Holmes x -> x -> Holmes ()

PrimMonad m => MonadCell (MoriarT m)

Defined in Control.Monad.MoriarT

Associated Types

data Cell (MoriarT m) a :: Type

Methods

discard :: MoriarT m x

fill :: x -> MoriarT m (Cell (MoriarT m) x)

watch :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m ()

with :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m ()

write :: Merge x => Cell (MoriarT m) x -> x -> MoriarT m ()

MonadCell (Watson h)

Defined in Control.Monad.Watson

Associated Types

data Cell (Watson h) a :: Type

Methods

discard :: Watson h x

fill :: x -> Watson h (Cell (Watson h) x)

watch :: Cell (Watson h) x -> (x -> Watson h ()) -> Watson h ()

with :: Cell (Watson h) x -> (x -> Watson h ()) -> Watson h ()

write :: Merge x => Cell (Watson h) x -> x -> Watson h ()

binary :: (MonadCell m, Merge x, Merge y, Merge z) => ((x, y, z) -> (x, y, z)) -> Cell m x -> Cell m y -> Cell m z -> m ()

In our regular Haskell coding, a binary function usually looks something like x -> y -> z. When we view it as a relationship, we see that it's actually a relationship between three values: x, y, and z.

Given a function that takes everything we currently know about these three values, and returns three "updates" based on what each can learn from the others, we can lift our three-way relationship (which, again, we can intuit as a multi-directional binary function) into a network as a three-way propagator. As an illustrative example, we might convert the '(+)' function into something like:

addR :: (Int, Int, Int) -> (Int, Int, Int)
addR ( a, b, c ) = ( c - b, c - a, a + b )

In practice, these values must be Merge values (unlike Int), and so any of them could be mempty, or less-than-well-defined. This function will take the three results as updates, and Merge it into the cell, so they will only make a difference if we've learnt something new.

make :: (MonadCell m, Monoid x) => m (Cell m x)

Create a cell with "no information", which we represent as mempty. When we evaluate propagator computations written with the Prop abstraction, this function is used to create the result cells at each node of the computation.

It's therefore important that your mempty value is reasonably efficient to compute, as larger computations may involve producing many of these values as intermediaries. An Intersect of all Int values, for example, is going to make things run very slowly.

unify :: (MonadCell m, Merge x) => Cell m x -> Cell m x -> m ()

This function takes two cells, and establishes propagators between them in both directions. These propagators simply copy across any updates that either cell receives, which means that the two cells end up holding exactly the same value at all times.

After calling this function, the two cells are entirely indistinguishable, as they will always be equivalent. We can intuit this function as "merging two cells into one".

unary :: (MonadCell m, Merge x, Merge y) => ((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()

A standard unary function goes from an input value to an output value. However, in the world of propagators, it is more powerful to rethink this as a relationship between two values.

A good example is the negate function. It doesn't matter whether you know the input or the output; it's always possible to figure out the one you're missing. Why, then, should our program only run in one direction? We could rephrase negate from 'Int -> Int' to something more like:

negateR :: ( Maybe Int, Maybe Int ) -> ( Maybe Int, Maybe Int )
negateR ( x, y ) = ( x | fmap negate y, y | fmap negate x )

Now, if we're missing one of the values, we can calculate it using the other! This, and the binary function's description above, give us an idea of how functions and relationships differ. The unary function simply lifts one of these expressions into a two-way propagator between two cells.

The Merge constraint means that we can use mempty to represent "knowing nothing" rather than the Maybe in the above example, which makes this function a little more generalised.