# LANGUAGE DeriveFunctor #
# LANGUAGE DerivingStrategies #
# LANGUAGE KindSignatures #

| 
 Module       : Control .  . Watson 
 Description :  join semilattice - based knowledge - merging . 
 Copyright    : ( c )   , 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 = = =  , 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 : 

 - '  ' 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@ does n'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 do n't want to trigger propagators if we do n'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 do n't have a notion of " failure state " , so we do n't know when we can 
   discard branches . If we do n'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 need n't 
 write their own assertion boilerplate for the usual suspects ( such as the 
 ' Data . JoinSemilattice . Defined . Conflict ' constructor ) . 


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


 Commutativity 
 Idempotence 
 Commutativity
 Idempotence
 | The result of merging some news into a cell's current knowledge.
 ^ We've learnt nothing; no updates elsewhere are needed.
 ^ We've learnt something; fire the propagators!
 ^ We've hit a failure state; discard the computation.
 | Join semilattice '(<>)' specialised for propagator network needs. Allows
 types to implement the notion of "knowledge combination".
 | Merge the news (right) into the current value (left), returning an
 instruction on how to update the network.
# LANGUAGE DeriveFunctor #
# LANGUAGE DerivingStrategies #
# LANGUAGE KindSignatures #

| 
 Module       : Control .  . Watson 
 Description :  join semilattice - based knowledge - merging . 
 Copyright    : ( c )   , 2020 
 License      : MIT 

 = Join semilattices 

 A _ _ join semilattice _ _ is a ' Monoid ' with two extra laws : 


 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 = = =  , 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 : 

 - '  ' 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@ does n'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 do n't want to trigger propagators if we do n'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 do n't have a notion of " failure state " , so we do n't know when we can 
   discard branches . If we do n'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 need n't 
 write their own assertion boilerplate for the usual suspects ( such as the 
 ' Data . JoinSemilattice . Defined . Conflict ' constructor ) . 


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:


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)

data Result (x :: Type)
  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)

class Monoid x => Merge (x :: Type) where

  (<<-) :: 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

