{-# 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 (Result x -> Result x -> Bool
(Result x -> Result x -> Bool)
-> (Result x -> Result x -> Bool) -> Eq (Result x)
forall x. Eq x => Result x -> Result x -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result x -> Result x -> Bool
$c/= :: forall x. Eq x => Result x -> Result x -> Bool
== :: Result x -> Result x -> Bool
$c== :: forall x. Eq x => Result x -> Result x -> Bool
Eq, a -> Result b -> Result a
(a -> b) -> Result a -> Result b
(forall a b. (a -> b) -> Result a -> Result b)
-> (forall a b. a -> Result b -> Result a) -> Functor Result
forall a b. a -> Result b -> Result a
forall a b. (a -> b) -> Result a -> Result b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Result b -> Result a
$c<$ :: forall a b. a -> Result b -> Result a
fmap :: (a -> b) -> Result a -> Result b
$cfmap :: forall a b. (a -> b) -> Result a -> Result b
Functor, Eq (Result x)
Eq (Result x)
-> (Result x -> Result x -> Ordering)
-> (Result x -> Result x -> Bool)
-> (Result x -> Result x -> Bool)
-> (Result x -> Result x -> Bool)
-> (Result x -> Result x -> Bool)
-> (Result x -> Result x -> Result x)
-> (Result x -> Result x -> Result x)
-> Ord (Result x)
Result x -> Result x -> Bool
Result x -> Result x -> Ordering
Result x -> Result x -> Result x
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall x. Ord x => Eq (Result x)
forall x. Ord x => Result x -> Result x -> Bool
forall x. Ord x => Result x -> Result x -> Ordering
forall x. Ord x => Result x -> Result x -> Result x
min :: Result x -> Result x -> Result x
$cmin :: forall x. Ord x => Result x -> Result x -> Result x
max :: Result x -> Result x -> Result x
$cmax :: forall x. Ord x => Result x -> Result x -> Result x
>= :: Result x -> Result x -> Bool
$c>= :: forall x. Ord x => Result x -> Result x -> Bool
> :: Result x -> Result x -> Bool
$c> :: forall x. Ord x => Result x -> Result x -> Bool
<= :: Result x -> Result x -> Bool
$c<= :: forall x. Ord x => Result x -> Result x -> Bool
< :: Result x -> Result x -> Bool
$c< :: forall x. Ord x => Result x -> Result x -> Bool
compare :: Result x -> Result x -> Ordering
$ccompare :: forall x. Ord x => Result x -> Result x -> Ordering
$cp1Ord :: forall x. Ord x => Eq (Result x)
Ord, Int -> Result x -> ShowS
[Result x] -> ShowS
Result x -> String
(Int -> Result x -> ShowS)
-> (Result x -> String) -> ([Result x] -> ShowS) -> Show (Result x)
forall x. Show x => Int -> Result x -> ShowS
forall x. Show x => [Result x] -> ShowS
forall x. Show x => Result x -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result x] -> ShowS
$cshowList :: forall x. Show x => [Result x] -> ShowS
show :: Result x -> String
$cshow :: forall x. Show x => Result x -> String
showsPrec :: Int -> Result x -> ShowS
$cshowsPrec :: forall x. Show x => Int -> Result x -> ShowS
Show)

instance Semigroup x => Semigroup (Result x) where
  Changed x
x <> :: Result x -> Result x -> Result x
<> Changed x
y = x -> Result x
forall x. x -> Result x
Changed (x
x x -> x -> x
forall a. Semigroup a => a -> a -> a
<> x
y)

  Result x
Failure <> Result x
_ = Result x
forall x. Result x
Failure
  Result x
_ <> Result x
Failure = Result x
forall x. Result x
Failure

  Result x
Unchanged <> Result x
y = Result x
y
  Result x
x <> Result x
Unchanged = Result x
x

instance Semigroup x => Monoid (Result x) where
  mempty :: Result x
mempty = Result x
forall x. Result x
Unchanged

instance Applicative Result where
  pure :: a -> Result a
pure = a -> Result a
forall x. x -> Result x
Changed

  Result (a -> b)
Failure <*> :: Result (a -> b) -> Result a -> Result b
<*> Result a
_ = Result b
forall x. Result x
Failure
  Result (a -> b)
_ <*> Result a
Failure = Result b
forall x. Result x
Failure

  Result (a -> b)
Unchanged <*> Result a
_ = Result b
forall x. Result x
Unchanged
  Result (a -> b)
_ <*> Result a
Unchanged = Result b
forall x. Result x
Unchanged

  Changed a -> b
f <*> Changed a
x = b -> Result b
forall x. x -> Result x
Changed (a -> b
f a
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
  Defined content
Conflict <<- :: Defined content -> Defined content -> Result (Defined content)
<<- Defined content
_ = Result (Defined content)
forall x. Result x
Failure
  Defined content
_ <<- Defined content
Conflict = Result (Defined content)
forall x. Result x
Failure

  Defined content
_       <<- Defined content
Unknown = Result (Defined content)
forall x. Result x
Unchanged
  Defined content
Unknown <<- Defined content
that    = Defined content -> Result (Defined content)
forall x. x -> Result x
Changed Defined content
that

  Exactly content
this <<- Exactly content
that
    | content
this content -> content -> Bool
forall a. Eq a => a -> a -> Bool
== content
that = Result (Defined content)
forall x. Result x
Unchanged
    | Bool
otherwise    = Result (Defined content)
forall x. Result x
Failure

instance (Bounded x, Enum x, Ord x, Hashable x)
    => Merge (Intersect x) where
  Intersect x
before <<- :: Intersect x -> Intersect x -> Result (Intersect x)
<<- Intersect x
news = case Intersect x
before Intersect x -> Intersect x -> Intersect x
forall a. Semigroup a => a -> a -> a
<> Intersect x
news of
    Intersect x
joined | Intersect x -> Int
forall x. Intersectable x => Intersect x -> Int
Intersect.size Intersect x
joined Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1                     -> Result (Intersect x)
forall x. Result x
Failure
           | Intersect x -> Int
forall x. Intersectable x => Intersect x -> Int
Intersect.size Intersect x
joined Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Intersect x -> Int
forall x. Intersectable x => Intersect x -> Int
Intersect.size Intersect x
before -> Intersect x -> Result (Intersect x)
forall x. x -> Result x
Changed Intersect x
joined
           | Bool
otherwise                                     -> Result (Intersect x)
forall x. Result x
Unchanged