content: {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE KindSignatures #-}
  
  {-|
  Module      : Control.Monad.Watson
  Description : Performant join semilattice-based knowledge-merging.
  Copyright   : (c) Tom Harding, 2020
  License     : MIT
  
  = Join semilattices
  
  A __join semilattice__ is a 'Monoid' with two extra laws:
  
  prop> x <> y === y <> x -- Commutativity
  prop> x <> x === x      -- Idempotence
  
  Within every cell, we store a join semilattice, and all writes are added into
  the cell using '(<>)'. Adding the above laws introduces enough structure to
  ensure that all functions between cells are __monotonic__. In other words, if
  we assume that @x@ "implies" @y@ if @x <> y === x@, the value /after/ a write
  will always imply the value /before/.
  
  We can therefore see each value as "moving up" some chain towards the final
  answer. More interestingly, the final answer implies /every value/ that has
  ever been in the cell. I like to use the intuition of __knowledge__ for join
  semilattices:
  
  - 'mempty' represents "knowing nothing" about a value.
  - '(<>)' is a function that /combines/ two knowledge bases into one.
  - @x@ implies @y@ if @y@ tells us nothing that @x@ doesn't already tell us.
  
  When we think about pure functions and referential transparency, we tend to say
  that "the value of a variable never changes". In the language of propagator
  networks, we can tweak this a little to say, "the value /being described/ by a
  cell's knowledge never changes".
  
  = Merging
  
  In a naïve system, we could simply define the join semilattice class as
  follows:
  
  @
  class Monoid x => JoinSemilattice (x :: Type)
  @
  
  (It would need no methods as it's really just some extra assertions on '(<>)').
  This would be fine, but there are a few shortcomings when we come to implement
  our 'Control.Monad.Cell.Class.write' operation:
  
  - We don't want to trigger propagators if we don't need to, so we'd want to
    check whether the result is different to the value that was there before.
    We'd most likely do this with a standard '(==)' comparison, but this could be
    quite expensive!
  
  - We don't have a notion of "failure state", so we don't know when we can
    discard branches. If we don't know when to /discard/ branches, we either have
    to implement assertions elsewhere (which puts more work onto the user) /or/
    discard nothing (which makes many problems intractably slow to compute).
  
  The cleanest solution I could find to this is expressed in the 'Result' type,
  which allows the type simultaneously to compute the merge result /and/ the
  resulting effect on the cell or network. In theory, it should respect the
  '(<>)' operation's behaviour, but with the added 'Failure' state. Not every
  type /needs/ to have a 'Failure' state, but it means that the user needn't
  write their own assertion boilerplate for the usual suspects (such as the
  'Data.JoinSemilattice.Defined.Conflict' constructor).
  
  -}
  module Data.JoinSemilattice.Class.Merge where
  
  import Data.Hashable (Hashable)
  import Data.JoinSemilattice.Defined (Defined (..))
  import Data.JoinSemilattice.Intersect (Intersect (..))
  import qualified Data.JoinSemilattice.Intersect as Intersect
  import Data.Kind (Type)
  
  -- | The result of merging some news into a cell's current knowledge.
  data Result (x :: Type)
    = Unchanged -- ^ We've learnt nothing; no updates elsewhere are needed.
    | Changed x -- ^ We've learnt something; fire the propagators!
    | Failure   -- ^ We've hit a failure state; discard the computation.
    deriving stock (Eq, Functor, Ord, Show)
  
  instance Semigroup x => Semigroup (Result x) where
    Changed x <> Changed y = Changed (x <> y)
  
    Failure <> _ = Failure
    _ <> Failure = Failure
  
    Unchanged <> y = y
    x <> Unchanged = x
  
  instance Semigroup x => Monoid (Result x) where
    mempty = Unchanged
  
  instance Applicative Result where
    pure = Changed
  
    Failure <*> _ = Failure
    _ <*> Failure = Failure
  
    Unchanged <*> _ = Unchanged
    _ <*> Unchanged = Unchanged
  
    Changed f <*> Changed x = Changed (f x)
  
  -- | Join semilattice '(<>)' specialised for propagator network needs. Allows
  -- types to implement the notion of "knowledge combination".
  class Monoid x => Merge (x :: Type) where
  
    -- | Merge the news (right) into the current value (left), returning an
    -- instruction on how to update the network.
    (<<-) :: x -> x -> Result x
  
  instance Eq content => Merge (Defined content) where
    Conflict <<- _ = Failure
    _ <<- Conflict = Failure
  
    _       <<- Unknown = Unchanged
    Unknown <<- that    = Changed that
  
    Exactly this <<- Exactly that
      | this == that = Unchanged
      | otherwise    = Failure
  
  instance (Bounded x, Enum x, Ord x, Hashable x)
      => Merge (Intersect x) where
    before <<- news = case before <> news of
      joined | Intersect.size joined < 1                     -> Failure
             | Intersect.size joined < Intersect.size before -> Changed joined
             | otherwise                                     -> Unchanged
  
  