content: {-# 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
  