{-# LANGUAGE BlockArguments #-} {-# LANGUAGE TypeFamilies #-} {-| Module : Control.Monad.Cell.Class Description : An interface for the primitive cell operations in a propagator network. Copyright : (c) Tom Harding, 2020 License : MIT /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 'Control.Monad.MoriarT.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__. -} module Control.Monad.Cell.Class where import Data.JoinSemilattice.Class.Merge (Merge) import Data.Kind (Type) import Data.Tuple (swap) import Prelude -- | 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 'Control.Monad.MoriarT.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. class Monad m => MonadCell (m :: Type -> Type) where -- | The type of cells for this particular implementation. Typically, it's -- some sort of mutable reference ('Data.STRef.STRef', 'Data.IORef.IORef', or -- similar), but the implementation may attach further metadata to the -- individual cells. data Cell m :: Type -> Type -- | 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. discard :: 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. fill :: x -> m (Cell m x) -- | 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. watch :: 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. with :: Cell m x -> (x -> m ()) -> 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. write :: Merge x => Cell m x -> x -> 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. 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 () binary f xs ys zs = do let update x y z = do let ( x', y', z' ) = f ( x, y, z ) write xs x' write ys y' write zs z' watch xs \x -> with ys \y -> with zs \z -> update x y z watch ys \y -> with xs \x -> with zs \z -> update x y z watch zs \z -> with ys \y -> with xs \x -> update x y z -- | Create a cell with "no information", which we represent as 'mempty'. When -- we evaluate propagator computations written with the 'Data.Propagator.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 'Data.JoinSemilattice.Intersect.Intersect' of all -- 'Int' values, for example, is going to make things run /very/ slowly. make :: (MonadCell m, Monoid x) => m (Cell m x) make = fill mempty -- | 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". unify :: (MonadCell m, Merge x) => Cell m x -> Cell m x -> m () unify = unary swap -- | 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. unary :: (MonadCell m, Merge x, Merge y) => ((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m () unary f xs ys = do let update x y = do let ( x', y' ) = f ( x, y ) write xs x' *> write ys y' watch xs \x -> with ys \y -> update x y watch ys \y -> with xs \x -> update x y