Copyright | (c) Tom Harding 2020 |
---|---|

License | MIT |

Safe Haskell | None |

Language | Haskell2010 |

*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**.

## Synopsis

- class Monad m => MonadCell (m :: Type -> Type) where
- 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 ()
- make :: (MonadCell m, Monoid x) => m (Cell m x)
- unify :: (MonadCell m, Merge x) => Cell m x -> Cell m x -> m ()
- unary :: (MonadCell m, Merge x, Merge y) => ((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()

# Documentation

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

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.

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) Source #

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 () Source #

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 () Source #

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 () Source #

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 Source # | |

Defined in Control.Monad.Holmes | |

PrimMonad m => MonadCell (MoriarT m) Source # | |

Defined in Control.Monad.MoriarT discard :: MoriarT m x Source # fill :: x -> MoriarT m (Cell (MoriarT m) x) Source # watch :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m () Source # with :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m () Source # write :: Merge x => Cell (MoriarT m) x -> x -> MoriarT m () Source # | |

MonadCell (Watson h) Source # | |

Defined in Control.Monad.Watson |

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 () Source #

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) Source #

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 () Source #

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 () Source #

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.