-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Tools and combinators for solving constraint problems.
--
-- A reference library for constraint-solving with propagators and CDCL.
@package holmes
@version 0.3.2.0
-- | Simplistically, search problems are solved by running the computation
-- with different input combinations, looking for any combinations that
-- satisfy the constraints. In reality, we play some tricks to avoid
-- running every possible input combination, but the principle is the
-- same:
--
-- This module exposes the Config type, which stores an initial
-- assignment for the input parameters (typically something close to
-- mempty), and a function that generates possible refinements for
-- those inputs.
--
-- For example, we might have a variable we know must be a number between
-- 1 and 10. A good initial value for this might be a
-- mempty value such as Unknown, with the refinements being
-- Exactly the ten possible values.
--
-- The initial values are first fed into the computation before
-- the propagators are established. Sometimes, these initial propagators
-- can produce new information (such as advancing a few steps forward in
-- a sudoku puzzle) before we even start to refine the inputs. The
-- benefit here is that we can sometimes discover that a variable's
-- search space is smaller than we realise, and so we end up with much
-- less work to do!
module Data.Input.Config
-- | An input configuration.
--
-- This stores both an initial configuration of input parameters,
-- as well as a function that can look for ways to refine an
-- input. In other words, if the initial value is an
-- Data.JoinSemilattice.Intersect of [1 .. 5], the
-- refinements might be singleton values of every remaining
-- possibility.
data Config (m :: Type -> Type) (x :: Type)
Config :: [x] -> (x -> m [x]) -> Config (m :: Type -> Type) (x :: Type)
[initial] :: Config (m :: Type -> Type) (x :: Type) -> [x]
[refine] :: Config (m :: Type -> Type) (x :: Type) -> x -> m [x]
-- | The simplest way of generating an input configuration is to say that a
-- problem has m variables that will all be one of n
-- possible values. For example, a sudoku board is 81 variables
-- of 9 possible values. This class allows us to generate these
-- simple input configurations like a game of countdown: "81
-- from 1 .. 9, please, Carol!"
class Input (x :: Type) where {
-- | Different parameter types will have different representations for
-- their values. The Raw type means that I can say 81
-- from [1 .. 9], and have the parameter type determine how
-- it will represent 1, for example. It's a little bit of
-- syntactic sugar for the benefit of the user, so they don't need to
-- know as much about how the parameter types work to use the library.
type family Raw x :: Type;
}
-- | Generate m variables who are one of n values. 81
-- from [1 .. 9], 5 from [ True, False ], and
-- so on.
from :: (Input x, Applicative m) => Int -> [Raw x] -> Config m x
-- | For debugging purposes, produce a HashSet of all possible
-- refinements that a Config might produce for a given problem.
-- This set could potentially be very large!
permute :: (Applicative m, Eq x, Hashable x) => Config m x -> m (HashSet [x])
-- | The Defined type simplifies the join semilattice-shaped
-- knowledge down to its simplest form, by saying there are only three
-- possible states of knowledge:
--
--
-- - I don't know anything about this value.
-- - I know exactly what this value is.
-- - I'm getting conflicting information.
--
--
-- The simplicity of the type makes it incredibly helpful when we're
-- trying to lift regular computations into the world of propagators.
module Data.JoinSemilattice.Defined
-- | Defines simple "levels of knowledge" about a value.
data Defined (x :: Type)
-- | Nothing has told me what this value is.
Unknown :: Defined (x :: Type)
-- | Everyone who has told me this value agrees.
Exactly :: x -> Defined (x :: Type)
-- | Two sources disagree on what this value should be.
Conflict :: Defined (x :: Type)
instance GHC.Num.Num x => GHC.Num.Num (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Enum.Bounded x => GHC.Enum.Bounded (Data.JoinSemilattice.Defined.Defined x)
instance Data.Hashable.Class.Hashable x => Data.Hashable.Class.Hashable (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Generics.Generic (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Base.Functor Data.JoinSemilattice.Defined.Defined
instance GHC.Show.Show x => GHC.Show.Show (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Classes.Ord x => GHC.Classes.Ord (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Classes.Eq x => GHC.Classes.Eq (Data.JoinSemilattice.Defined.Defined x)
instance GHC.Enum.Enum content => GHC.Enum.Enum (Data.JoinSemilattice.Defined.Defined content)
instance GHC.Base.Applicative Data.JoinSemilattice.Defined.Defined
instance GHC.Classes.Eq content => GHC.Base.Semigroup (Data.JoinSemilattice.Defined.Defined content)
instance GHC.Classes.Eq content => GHC.Base.Monoid (Data.JoinSemilattice.Defined.Defined content)
instance GHC.Real.Real content => GHC.Real.Real (Data.JoinSemilattice.Defined.Defined content)
instance GHC.Real.Integral content => GHC.Real.Integral (Data.JoinSemilattice.Defined.Defined content)
instance GHC.Real.Fractional x => GHC.Real.Fractional (Data.JoinSemilattice.Defined.Defined x)
instance Data.Input.Config.Input (Data.JoinSemilattice.Defined.Defined content)
-- | When we play games like Guess Who?, we start with a set of possible
-- candidates, and eliminate subsets of them as the game progresses. The
-- Intersect type works in a similar way: each cell stores a list
-- of its potential values, and the merging operation takes the
-- intersect of the current candidates and the new candidates.
module Data.JoinSemilattice.Intersect
-- | A set type with intersection as the (<>) operation.
newtype Intersect (x :: Type)
Intersect :: HashSet x -> Intersect (x :: Type)
[toHashSet] :: Intersect (x :: Type) -> HashSet x
class (Bounded content, Enum content, Ord content, Hashable content) => Intersectable content
lift2 :: (Intersectable this, Intersectable that, Intersectable result) => (this -> that -> result) -> Intersect this -> Intersect that -> Intersect result
-- | Create an Intersect from a list of candidates.
fromList :: (Eq x, Hashable x) => [x] -> Intersect x
-- | Return a list of candidates stored within an Intersect.
toList :: (Bounded x, Enum x, Eq x) => Intersect x -> [x]
-- | Run an action only if a single candidate remains.
decided :: (Applicative m, Intersectable x) => (x -> m ()) -> Intersect x -> m ()
-- | Delete a candidate from an Intersect.
delete :: Intersectable x => x -> Intersect x -> Intersect x
-- | Return an Intersect of all possible candidates except
-- those in the given Intersect. The Intersect of
-- all candidates is assumed to be mempty.
except :: Intersectable x => Intersect x -> Intersect x
-- | Filter an Intersect with a predicate.
filter :: (x -> Bool) -> Intersect x -> Intersect x
-- | Convert a Set to an Intersect.
fromSet :: (Eq x, Hashable x) => Set x -> Intersect x
-- | Map over an Intersect with a given function.
map :: (Eq y, Hashable y) => (x -> y) -> Intersect x -> Intersect y
powerSet :: (Bounded x, Enum x, Hashable x, Ord x) => Intersect x -> Intersect (Intersect x)
-- | Create a singleton Intersect.
singleton :: Hashable x => x -> Intersect x
-- | Count the candidates in an Intersect.
size :: Intersectable x => Intersect x -> Int
-- | Convert an Intersect to a Set.
toSet :: Ord x => Intersect x -> Set x
-- | Merge two Intersect values with set union.
union :: Intersectable x => Intersect x -> Intersect x -> Intersect x
-- | Produce a Config with the given initial value, where the
-- refine function just tries each remaining candidate as a
-- singleton.
using :: (Applicative m, Intersectable x) => [Intersect x] -> Config m (Intersect x)
instance Data.Hashable.Class.Hashable x => Data.Hashable.Class.Hashable (Data.JoinSemilattice.Intersect.Intersect x)
instance Data.Foldable.Foldable Data.JoinSemilattice.Intersect.Intersect
instance GHC.Show.Show x => GHC.Show.Show (Data.JoinSemilattice.Intersect.Intersect x)
instance GHC.Classes.Ord x => GHC.Classes.Ord (Data.JoinSemilattice.Intersect.Intersect x)
instance GHC.Classes.Eq x => GHC.Classes.Eq (Data.JoinSemilattice.Intersect.Intersect x)
instance (GHC.Enum.Bounded content, GHC.Enum.Enum content, GHC.Classes.Ord content, Data.Hashable.Class.Hashable content) => Data.JoinSemilattice.Intersect.Intersectable content
instance Data.JoinSemilattice.Intersect.Intersectable content => GHC.Base.Monoid (Data.JoinSemilattice.Intersect.Intersect content)
instance (Data.JoinSemilattice.Intersect.Intersectable content, GHC.Num.Num content) => GHC.Num.Num (Data.JoinSemilattice.Intersect.Intersect content)
instance (Data.JoinSemilattice.Intersect.Intersectable x, GHC.Real.Fractional x) => GHC.Real.Fractional (Data.JoinSemilattice.Intersect.Intersect x)
instance Data.JoinSemilattice.Intersect.Intersectable x => Data.Input.Config.Input (Data.JoinSemilattice.Intersect.Intersect x)
instance (GHC.Classes.Eq content, Data.Hashable.Class.Hashable content) => GHC.Base.Semigroup (Data.JoinSemilattice.Intersect.Intersect content)
-- | 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 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
-- | 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 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 (STRef, IORef, or
-- similar), but the implementation may attach further metadata to the
-- individual cells.
data family 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 :: MonadCell m => 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 :: MonadCell m => 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 :: MonadCell m => 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 :: MonadCell m => Cell m x -> (x -> m ()) -> m ()
-- | Write an update to a cell. This update should be merged into
-- the current value using the (<<-) 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 :: (MonadCell m, 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 ()
-- | Create a cell with "no information", which we represent as
-- mempty. When we evaluate propagator computations written with
-- the 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 Intersect of all
-- Int values, for example, is going to make things run
-- very slowly.
make :: (MonadCell m, Monoid x) => m (Cell m x)
-- | 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 ()
-- | 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 ()
-- | The real heart of a propagator network is the cell-level interaction,
-- but it doesn't come with a particularly pleasant API. The solution is
-- the Prop abstraction, which hides away some of the more
-- gruesome internals.
--
-- This module exposes a set of functions to construct propagator
-- networks with a "focal point", which we can intuit as being the
-- "output" of the functions we're used to writing.
--
-- The important thing to note is that most of these functions allow for
-- multi-directional information flow. While (.&&)
-- might look like (&&), it allows the inputs to be
-- computed from the outputs, so it's a lot more capable. Think of these
-- functions as a way to build equations that we can re-arrange as need
-- be.
module Data.Propagator
-- | A propagator network with a "focus" on a particular cell. The focus is
-- the cell that typically holds the result we're trying to compute.
data Prop (m :: Type -> Type) (content :: Type)
-- | Lift a cell into a propagator network. Mostly for internal library
-- use.
up :: Applicative m => Cell m x -> Prop m x
-- | Lower a propagator network's focal point down to a cell. Mostly for
-- internal library use.
down :: (MonadCell m, Monoid x) => Prop m x -> m (Cell m x)
lift :: forall f m c x. (MonadCell m, c x) => Lifting f c => x -> Prop m (f x)
-- | Lift a regular function into a propagator network. The function is
-- lifted into a relationship with one-way information flow.
over :: (Merge x, Merge y) => (x -> y) -> Prop m x -> Prop m y
-- | Lift a regular binary function into a propagator network. The function
-- is lifted into a relationship between three variables where
-- information only flows in one direction.
lift2 :: (Merge x, Merge y, Merge z) => (x -> y -> z) -> Prop m x -> Prop m y -> Prop m z
-- | Lift a unary relationship into a propagator network. Unlike
-- over, this allows information to travel in both directions.
unary :: (Merge x, Merge y) => ((x, y) -> (x, y)) -> Prop m x -> Prop m y
-- | Lift a binary relationship into a propagator network. This allows
-- three-way information flow.
binary :: (Merge x, Merge y, Merge z) => ((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
-- | Different parameter types come with different representations for
-- Bool. This function takes two propagator networks focusing on
-- boolean values, and produces a new network in which the focus is the
-- conjunction of the two values.
--
-- It's a lot of words, but the intuition is, "(&&) over
-- propagators".
(.&&) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
infixr 3 .&&
-- | Run a predicate on all values in a list, producing a list of
-- propagator networks focusing on boolean values. Then, produce a new
-- network with a focus on the conjunction of all these values.
--
-- In other words, "all over propagators".
all' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | The same as the all' function, but with access to the index of
-- the element within the array. Typically, this is useful when trying to
-- relate each element to other elements within the array.
--
-- For example, cells "surrounding" the current cell in a conceptual
-- "board".
allWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | Given a list of propagator networks with a focus on boolean values,
-- create a new network with a focus on the conjugation of all these
-- values.
--
-- In other words, "and over propagators".
and' :: (BooleanR f, MonadCell m) => [Prop m (f Bool)] -> Prop m (f Bool)
-- | Calculate the disjunction of two boolean propagator network values.
(.||) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
infixr 2 .||
-- | Run a predicate on all values in a list, producing a list of
-- propagator networks focusing on boolean values. Then, produce a new
-- network with a focus on the disjunction of all these values.
--
-- In other words, "any over propagators".
any' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | The same as the any' function, but with access to the index of
-- the element within the array. Typically, this is useful when trying to
-- relate each element to other elements within the array.
--
-- For example, cells "surrounding" the current cell in a conceptual
-- "board".
anyWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | Given a list of propagator networks with a focus on boolean values,
-- create a new network with a focus on the disjunction of all these
-- values.
--
-- In other words, "or over propagators".
or' :: (BooleanR f, MonadCell m) => [Prop m (f Bool)] -> Prop m (f Bool)
-- | Different parameter types come with different representations for
-- Bool. This value is a propagator network with a focus on a
-- polymorphic "falsey" value.
false :: (BooleanR f, MonadCell m) => Prop m (f Bool)
-- | Given a propagator network with a focus on a boolean value, produce a
-- network with a focus on its negation.
--
-- ... It's "not over propagators".
not' :: (BooleanR f, MonadCell m) => Prop m (f Bool) -> Prop m (f Bool)
-- | Different parameter types come with different representations for
-- Bool. This value is a propagator network with a focus on a
-- polymorphic "truthy" value.
true :: (BooleanR f, MonadCell m) => Prop m (f Bool)
-- | Asserts that exactly n of the elements must match the given predicate.
exactly :: (BooleanR f, MonadCell m) => Int -> (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | Utility function that calculates all possible ways to pick k values
-- out of n. It returns a list of picks, where each pick contains a
-- boolean indicating whether that value was picked
choose :: Int -> Int -> [[Bool]]
-- | Given two propagator networks, produce a new propagator network with
-- the result of testing the two for equality.
--
-- In other words, "it's (==) for propagators".
(.==) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .==
-- | Given two propagator networks, produce a new propagator network with
-- the result of testing the two for inequality.
--
-- In other words, "it's (/=) for propagators".
(./=) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 ./=
-- | Given a list of networks, produce the conjunction of (./=)
-- applied to every possible pair. The resulting network's focus is the
-- answer to whether every propagator network's focus is different to the
-- others.
--
-- Are all the values in this list distinct?
distinct :: (EqR f, EqC f x, MonadCell m) => [Prop m (f x)] -> Prop m (f Bool)
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be greater than the second.
--
-- In other words, "it's (>) for propagators".
(.>) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .>
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be greater than or equal to the
-- second.
--
-- In other words, "it's (>=) for propagators".
(.>=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .>=
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be less than the second.
--
-- In other words, "it's (<) for propagators".
(.<) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .<
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be less than or equal to the second.
--
-- In other words, "it's (<=) for propagators".
(.<=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .<=
-- | Given two propagator networks, produce a new network that focuses on
-- the sum of the two given networks' foci.
--
-- ... It's (+) lifted over propagator networks.
(.+) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 6 .+
-- | Given two propagator networks, produce a new network that focuses on
-- the difference between the two given networks' foci.
--
-- ... It's (-) lifted over propagator networks.
(.-) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 6 .-
-- | Produce a network that focuses on the negation of another
-- network's focus.
--
-- ... It's negate lifted over propagator networks.
negate' :: (Num x, SumR x, MonadCell m) => Prop m x -> Prop m x
-- | Given two propagator networks, produce a new network that focuses on
-- the product between the two given networks' integral foci.
--
-- ... It's (*) lifted over propagator networks. Crucially,
-- the reverse information flow uses integral division, which
-- should work the same way as div.
(.*.) :: (Num x, IntegralR x) => Prop m x -> Prop m x -> Prop m x
infixl 7 .*.
-- | Given two propagator networks, produce a new network that focuses on
-- the division of the two given networks' integral foci.
--
-- ... It's div lifted over propagator networks.
(./.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 ./.
-- | Given two propagator networks, produce a new network that focuses on
-- the modulo of the two given networks' integral foci.
--
-- ... It's mod lifted over propagator networks.
(.%.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 .%.
-- | Given two propagator networks, produce a new network that focuses on
-- the product of the two given networks' foci.
--
-- ... It's (*) lifted over propagator networks. The
-- reverse information flow is fractional division, (/).
(.*) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 .*
-- | Given two propagator networks, produce a new network that focuses on
-- the division of the two given networks' foci.
--
-- ... It's (/) lifted over propagator networks.
(./) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 ./
-- | Produce a network that focuses on the reciprocal of another
-- network's focus.
--
-- ... It's recip lifted over propagator networks.
recip' :: (Num x, FractionalR x, MonadCell m) => Prop m x -> Prop m x
-- | Produce a network that focuses on the absolute value of another
-- network's focus.
--
-- ... It's abs lifted over propagator networks.
abs' :: (AbsR x, MonadCell m) => Prop m x -> Prop m x
-- | Lift a regular function over a propagator network and its
-- parameter type. Unlike over, this function abstracts away the
-- specific behaviour of the parameter type (such as Defined).
(.$) :: (Mapping f c, c x, c y) => (x -> y) -> Prop m (f x) -> Prop m (f y)
-- | Lift a three-way relationship over two propagator networks' foci to
-- produce a third propagator network with a focus on the third value in
-- the relationship.
--
-- ... It's liftA2 for propagators.
zipWith' :: (Zipping f c, c x, c y, c z) => (x -> y -> z) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
-- | Produce a network in which the raw values of a given network are used
-- to produce new parameter types. See the "wave function collapse" demo
-- for an example usage.
(.>>=) :: (FlatMapping f c, c x, c y) => Prop m (f x) -> (x -> f y) -> Prop m (f y)
instance (Data.JoinSemilattice.Class.Abs.AbsR x, Data.JoinSemilattice.Class.Sum.SumR x, GHC.Num.Num x, Control.Monad.Cell.Class.MonadCell m) => GHC.Num.Num (Data.Propagator.Prop m x)
instance (Data.JoinSemilattice.Class.Abs.AbsR x, GHC.Real.Fractional x, Data.JoinSemilattice.Class.Fractional.FractionalR x, GHC.Num.Num x, Control.Monad.Cell.Class.MonadCell m) => GHC.Real.Fractional (Data.Propagator.Prop m x)
-- | MoriarT is a monad transformer implementing the
-- MonadCell class with provenance and backtracking search. In
-- other words, it can search large parameter spaces using different
-- parameter configurations, looking for contradicting sets of parameters
-- to prune out parts of the search tree. It does this by keeping track
-- of which cells influence which results, and considering any
-- influencers on a failure to be contradictory.
--
-- In other words: if a write to cell A fails, and the write was
-- based on values from cells B and C, any search
-- branch in which B and C have these current values
-- will be pruned from the search, and we won't try them.
--
-- (In practice, this isn't strictly true: we just abort any branch that
-- ever produces any cell with any provenance that contains those values
-- for B and C. This is a "lazier" strategy, and
-- doesn't involve evaluating the search space up front).
module Control.Monad.MoriarT
-- | The constraint-solving monad transformer. We implement the current
-- computation context with MonadReader, and the current "no
-- goods" list with MonadState.
--
-- This transformer exposes its internals through the MonadReader,
-- MonadState, MonadLogic, and MonadIO interfaces,
-- and should therefore not be used directly. The reason is simply
-- that misuse of any of these will break the computation, so the library
-- provides Control.Monad.Holmes and Control.Monad.Watson,
-- who do their best to thwart MoriarT.
newtype MoriarT (m :: Type -> Type) (x :: Type)
MoriarT :: ReaderT Rule (LogicT (StateT Group m)) x -> MoriarT (m :: Type -> Type) (x :: Type)
[unMoriarT] :: MoriarT (m :: Type -> Type) (x :: Type) -> ReaderT Rule (LogicT (StateT Group m)) x
-- | Run a MoriarT computation and return the list of all
-- valid branches' results, in the order in which they were discovered.
runAll :: Monad m => MoriarT m x -> m [x]
-- | Run a MoriarT computation and return the first valid
-- branch's result.
runOne :: Monad m => MoriarT m x -> m (Maybe x)
-- | Given an input configuration, and a predicate on those input
-- variables, compute the configurations that satisfy the predicate. This
-- result (or these results) can be extracted using runOne or
-- runAll.
solve :: (PrimMonad m, EqR f, Merge (f x), Typeable x) => Config (MoriarT m) (f x) -> (forall m'. MonadCell m' => [Prop m' (f x)] -> Prop m' (f Bool)) -> MoriarT m [f x]
-- | Unsafely read from a cell. This operation is unsafe because it doesn't
-- factor this cell into the provenance of any subsequent writes. If this
-- value ends up causing a contradiction, we may end up removing branches
-- of the search tree that are totally valid! This operation is safe as
-- long as it is the very last thing you do in a computation, and
-- its value is never used to influence any writes in any way.
unsafeRead :: PrimMonad m => Cell (MoriarT m) x -> MoriarT m x
instance GHC.Base.Monoid x => GHC.Base.Monoid (Control.Monad.MoriarT.MoriarT m x)
instance GHC.Base.Semigroup x => GHC.Base.Semigroup (Control.Monad.MoriarT.MoriarT m x)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState Data.CDCL.Group (Control.Monad.MoriarT.MoriarT m)
instance Control.Monad.Reader.Class.MonadReader Data.CDCL.Rule (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.MonadPlus (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.Monad m => Control.Monad.Logic.Class.MonadLogic (Control.Monad.MoriarT.MoriarT m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.Monad (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.Alternative (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.Applicative (Control.Monad.MoriarT.MoriarT m)
instance GHC.Base.Functor (Control.Monad.MoriarT.MoriarT m)
instance Control.Monad.Trans.Class.MonadTrans Control.Monad.MoriarT.MoriarT
instance Control.Monad.Primitive.PrimMonad m => Control.Monad.Primitive.PrimMonad (Control.Monad.MoriarT.MoriarT m)
instance Control.Monad.Primitive.PrimMonad m => Control.Monad.Cell.Class.MonadCell (Control.Monad.MoriarT.MoriarT m)
-- | Watson works in a near-identical way to Holmes, but with one
-- distinction: its base type is ST rather than IO, so the
-- API calculates the results with "observably pure" functions. There are
-- downsides: for example, Watson can't perform random restart
-- with operations like shuffle. However, this is often an
-- acceptable compromise to avoid IO entirely!
module Control.Monad.Watson
-- | A monad capable of solving constraint problems using ST as the
-- evaluation type. Cells are represented using STRef references,
-- and provenance is tracked to optimise backtracking search
-- across multiple branches.
data Watson (h :: Type) (x :: Type)
-- | 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 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 (STRef, IORef, or
-- similar), but the implementation may attach further metadata to the
-- individual cells.
data family 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 :: MonadCell m => 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 :: MonadCell m => 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 :: MonadCell m => 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 :: MonadCell m => Cell m x -> (x -> m ()) -> m ()
-- | Write an update to a cell. This update should be merged into
-- the current value using the (<<-) 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 :: (MonadCell m, Merge x) => Cell m x -> x -> m ()
-- | Run a function between propagators "backwards", writing the given
-- value as the output and then trying to push information backwards to
-- the input cell.
backward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> y -> Maybe x
-- | Run a function between propagators with a raw value, writing the given
-- value to the "input" cell and reading the result from the "output"
-- cell.
forward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> x -> Maybe y
-- | Interpret a Watson program, returning a list of all successful
-- branches' outputs. It's unlikely that you want to call this directly,
-- though; typically, satisfying or whenever are more
-- likely the things you want.
runAll :: (forall h. Watson h x) -> [x]
-- | Interpret a Watson program, returning the first successful
-- branch's result if any branch succeeds. It's unlikely that you
-- want to call this directly, though; typically, satisfying or
-- whenever are more likely the things you want.
runOne :: (forall h. Watson h x) -> Maybe x
-- | Given an input configuration, and a predicate on those input
-- variables, return the first configuration that satisfies the
-- predicate.
satisfying :: (EqC f x, EqR f, Typeable x) => (forall h. Config (Watson h) (f x)) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> Maybe [f x]
-- | Unsafely read from a cell. This operation is unsafe because it doesn't
-- factor this cell into the provenance of any subsequent writes. If this
-- value ends up causing a contradiction, we may end up removing branches
-- of the search tree that are totally valid! This operation is safe as
-- long as it is the very last thing you do in a computation, and
-- its value is never used to influence any writes in any way.
unsafeRead :: Cell (Watson h) x -> Watson h x
-- | Given an input configuration, and a predicate on those input
-- variables, return all configurations that satisfy the
-- predicate. It should be noted that there's nothing lazy about this; if
-- your problem has a lot of solutions, or your search space is very big,
-- you'll be waiting a long time!
whenever :: (EqC f x, EqR f, Typeable x) => (forall h. Config (Watson h) (f x)) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> [[f x]]
instance GHC.Base.Monad (Control.Monad.Watson.Watson h)
instance GHC.Base.Applicative (Control.Monad.Watson.Watson h)
instance GHC.Base.Functor (Control.Monad.Watson.Watson h)
instance Control.Monad.Fail.MonadFail (Control.Monad.Watson.Watson h)
instance Control.Monad.Cell.Class.MonadCell (Control.Monad.Watson.Watson h)
-- | Holmes is a type for solving constraint problems. These
-- computations are executed with IO, which allows for extra
-- features such as the ability to shuffle the input
-- configuration.
--
-- If this isn't a feature you require, you may prefer to use the
-- Control.Monad.Watson interface, which offers a pure version of
-- the API thanks to its use of ST. The internal code is shared
-- between the two, so results between the two are consistent.
module Control.Monad.Holmes
-- | A monad capable of solving constraint problems using IO as the
-- evaluation type. Cells are represented using IORef references,
-- and provenance is tracked to optimise backtracking search
-- across multiple branches.
data Holmes (x :: Type)
-- | 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 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)
-- | Run a function between propagators "backwards", writing the given
-- value as the output and then trying to push information backwards to
-- the input cell.
backward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> y -> IO (Maybe x)
-- | Run a function between propagators with a raw value, writing the given
-- value to the "input" cell and reading the result from the "output"
-- cell.
forward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> x -> IO (Maybe y)
-- | Interpret a Holmes program into IO, returning a list of
-- all successful branches' outputs. It's unlikely that you want to call
-- this directly, though; typically, satisfying or whenever
-- are more likely the things you want.
runAll :: Holmes x -> IO [x]
-- | Interpret a Holmes program into IO, returning the first
-- successful branch's result if any branch succeeds. It's
-- unlikely that you want to call this directly, though; typically,
-- satisfying or whenever are more likely the things you
-- want.
runOne :: Holmes x -> IO (Maybe x)
-- | Given an input configuration, and a predicate on those input
-- variables, return the first configuration that satisfies the
-- predicate.
satisfying :: (EqC f x, EqR f, Typeable x) => Config Holmes (f x) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> IO (Maybe [f x])
-- | Shuffle the refinements in a configuration. If we make a configuration
-- like 100 from [1 .. 10], the first configuration
-- will be one hundred 1 values. Sometimes, we might find we get
-- to a first solution faster by randomising the order in which
-- refinements are given. This is similar to the "random restart"
-- strategy in hill-climbing problems.
--
-- Another nice use for this function is procedural generation: often,
-- your results will look more "natural" if you introduce an element of
-- randomness.
shuffle :: Config Holmes x -> Config Holmes x
-- | Unsafely read from a cell. This operation is unsafe because it doesn't
-- factor this cell into the provenance of any subsequent writes. If this
-- value ends up causing a contradiction, we may end up removing branches
-- of the search tree that are totally valid! This operation is safe as
-- long as it is the very last thing you do in a computation, and
-- its value is never used to influence any writes in any way.
unsafeRead :: Cell Holmes x -> Holmes x
-- | Given an input configuration, and a predicate on those input
-- variables, return all configurations that satisfy the
-- predicate. It should be noted that there's nothing lazy about this; if
-- your problem has a lot of solutions, or your search space is very big,
-- you'll be waiting a long time!
whenever :: (EqC f x, EqR f, Typeable x) => Config Holmes (f x) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> IO [[f x]]
instance GHC.Base.Monad Control.Monad.Holmes.Holmes
instance GHC.Base.Applicative Control.Monad.Holmes.Holmes
instance GHC.Base.Functor Control.Monad.Holmes.Holmes
instance Control.Monad.Fail.MonadFail Control.Monad.Holmes.Holmes
instance Control.Monad.Cell.Class.MonadCell Control.Monad.Holmes.Holmes
-- | This module includes almost everything you'd need to build a
-- constraint-solving computation. The module uses the Holmes
-- solver, but you may want to use the functions in the
-- Control.Monad.Watson module to avoid executing your code in
-- IO.
module Data.Holmes
-- | A monad capable of solving constraint problems using IO as the
-- evaluation type. Cells are represented using IORef references,
-- and provenance is tracked to optimise backtracking search
-- across multiple branches.
data Holmes (x :: Type)
-- | 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 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)
-- | Run a function between propagators with a raw value, writing the given
-- value to the "input" cell and reading the result from the "output"
-- cell.
forward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> x -> Maybe y
-- | Run a function between propagators "backwards", writing the given
-- value as the output and then trying to push information backwards to
-- the input cell.
backward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> y -> Maybe x
-- | Given an input configuration, and a predicate on those input
-- variables, return the first configuration that satisfies the
-- predicate.
satisfying :: (EqC f x, EqR f, Typeable x) => Config Holmes (f x) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> IO (Maybe [f x])
-- | Shuffle the refinements in a configuration. If we make a configuration
-- like 100 from [1 .. 10], the first configuration
-- will be one hundred 1 values. Sometimes, we might find we get
-- to a first solution faster by randomising the order in which
-- refinements are given. This is similar to the "random restart"
-- strategy in hill-climbing problems.
--
-- Another nice use for this function is procedural generation: often,
-- your results will look more "natural" if you introduce an element of
-- randomness.
shuffle :: Config Holmes x -> Config Holmes x
-- | Given an input configuration, and a predicate on those input
-- variables, return all configurations that satisfy the
-- predicate. It should be noted that there's nothing lazy about this; if
-- your problem has a lot of solutions, or your search space is very big,
-- you'll be waiting a long time!
whenever :: (EqC f x, EqR f, Typeable x) => Config Holmes (f x) -> (forall m. MonadCell m => [Prop m (f x)] -> Prop m (f Bool)) -> IO [[f x]]
-- | An input configuration.
--
-- This stores both an initial configuration of input parameters,
-- as well as a function that can look for ways to refine an
-- input. In other words, if the initial value is an
-- Data.JoinSemilattice.Intersect of [1 .. 5], the
-- refinements might be singleton values of every remaining
-- possibility.
data Config (m :: Type -> Type) (x :: Type)
Config :: [x] -> (x -> m [x]) -> Config (m :: Type -> Type) (x :: Type)
[initial] :: Config (m :: Type -> Type) (x :: Type) -> [x]
[refine] :: Config (m :: Type -> Type) (x :: Type) -> x -> m [x]
-- | The simplest way of generating an input configuration is to say that a
-- problem has m variables that will all be one of n
-- possible values. For example, a sudoku board is 81 variables
-- of 9 possible values. This class allows us to generate these
-- simple input configurations like a game of countdown: "81
-- from 1 .. 9, please, Carol!"
class Input (x :: Type) where {
-- | Different parameter types will have different representations for
-- their values. The Raw type means that I can say 81
-- from [1 .. 9], and have the parameter type determine how
-- it will represent 1, for example. It's a little bit of
-- syntactic sugar for the benefit of the user, so they don't need to
-- know as much about how the parameter types work to use the library.
type family Raw x :: Type;
}
-- | Generate m variables who are one of n values. 81
-- from [1 .. 9], 5 from [ True, False ], and
-- so on.
from :: (Input x, Applicative m) => Int -> [Raw x] -> Config m x
-- | For debugging purposes, produce a HashSet of all possible
-- refinements that a Config might produce for a given problem.
-- This set could potentially be very large!
permute :: (Applicative m, Eq x, Hashable x) => Config m x -> m (HashSet [x])
-- | Unlike the abs we know, which is a function from a value
-- to its absolute value, absR is a relationship between a
-- value and its absolute.
--
-- For some types, while we can't truly reverse the abs function,
-- we can say that there are two possible inputs to consider, and
-- so we can push some information in the reverse direction.
class Merge x => AbsR (x :: Type)
-- | Given a value and its absolute, try to learn something in either
-- direction.
absR :: AbsR x => (x, x) -> (x, x)
-- | Given a value and its absolute, try to learn something in either
-- direction.
absR :: (AbsR x, Num x) => (x, x) -> (x, x)
-- | Rather than the not, and, and or functions we
-- know and love, the BooleanR class presents relationships
-- that are analogous to these. The main difference is that relationships
-- are not one-way. For example, if I tell you that the output of
-- x && y is True, you can tell me what the
-- inputs are, even if your computer can't. The implementations of
-- BooleanR should be such that all directions of inference are
-- considered.
class Merge (f Bool) => BooleanR (f :: Type -> Type)
-- | An overloaded False value.
falseR :: BooleanR f => f Bool
-- | An overloaded True value.
trueR :: BooleanR f => f Bool
-- | A relationship between a boolean value and its opposite.
notR :: BooleanR f => (f Bool, f Bool) -> (f Bool, f Bool)
-- | A relationship between two boolean values and their conjunction.
andR :: BooleanR f => (f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
-- | A relationship between two boolean values and their disjunction.
orR :: BooleanR f => (f Bool, f Bool, f Bool) -> (f Bool, f Bool, f Bool)
-- | Equality between two variables as a relationship between them and
-- their result. The hope here is that, if we learn the output before the
-- inputs, we can often "work backwards" to learn something about them.
-- If we know the result is exactly true, for example, we can
-- effectively then unify the two input cells, as we know that
-- their values will always be the same.
--
-- The class constraints are a bit ugly here, and it's something I'm
-- hoping I can tidy up down the line. The idea is that, previously, our
-- class was defined as:
--
--
-- class EqR (x :: Type) (b :: Type) | x -> b where
-- eqR :: (x -> x -> b) -> (x -> x -> b)
--
--
-- The problem here was that, if we said x .== x :: Prop m (Defined
-- Bool), we couldn't even infer that the type of x was
-- Defined-wrapped, which made the overloaded literals, for
-- example, largely pointless.
--
-- To fix it, the class was rewritten to parameterise the wrapper type,
-- which means we can always make this inference. However, the
-- constraints got a bit grizzly when I hacked it together.
class (forall x. EqC' f x => Merge (f x), BooleanR f) => EqR (f :: Type -> Type) where {
type family EqC f :: Type -> Constraint;
}
eqR :: (EqR f, EqC' f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | A relationship between two variables and the result of a not-equals
-- comparison between them.
neR :: (EqR f, EqC' f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | Some types, such as Intersect, contain multiple "candidate
-- values". This function allows us to take each candidate, apply
-- a function, and then union all the results. Perhaps fanOut
-- would have been a better name for this function, but we use
-- (>>=) to lend an intuition when we lift this into
-- Prop via (.>>=).
--
-- There's not normally much reverse-flow information here, sadly, as it
-- typically requires us to have a way to generate an "empty candidate" a
-- la mempty. It's quite hard to articulate this in a succinct
-- way, but try implementing the reverse flow for Defined or
-- Intersect, and see what happens.
class Zipping f c => FlatMapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c
flatMapR :: (FlatMapping f c, c x, c y) => (Maybe (x -> f y), Maybe (f y -> x)) -> (f x, f y) -> (f x, f y)
-- | Reversible (fractional or floating-point) multiplication as a
-- three-value relationship between two values and their product.
class SumR x => FractionalR (x :: Type)
multiplyR :: FractionalR x => (x, x, x) -> (x, x, x)
multiplyR :: (FractionalR x, Fractional x) => (x, x, x) -> (x, x, x)
-- | A four-way divMod relationship between two values, the result
-- of integral division, and the result of the first modulo the second.
class SumR x => IntegralR (x :: Type)
divModR :: IntegralR x => (x, x, x, x) -> (x, x, x, x)
-- | Embed a regular value inside a parameter type.
class Lifting (f :: Type -> Type) (c :: Type -> Constraint) | f -> c
lift' :: (Lifting f c, c x) => x -> f x
-- | Lift a relationship between two values over some type constructor.
-- Typically, this type constructor will be the parameter type.
class (forall x. c x => Merge (f x)) => Mapping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c
mapR :: (Mapping f c, c x, c y) => (Maybe (x -> y), Maybe (y -> x)) -> (f x, f y) -> (f x, f y)
-- | Comparison relationships between two values and their comparison
-- result. See EqR for more information on the design of this
-- class, and a full apology for the constraints involved.
class (EqR f, forall x. OrdC f x => EqC' f x) => OrdR (f :: Type -> Type) where {
type family OrdC f :: Type -> Constraint;
type OrdC f = EqC f;
}
-- | A relationship between two values and whether the left is less than or
-- equal to the right.
lteR :: (OrdR f, OrdC f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | Comparison between two values and their (<) result.
ltR :: (OrdR f, OrdC f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | Comparison between two values and their (>) result.
gtR :: (OrdR f, OrdC f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | Comparison between two values and their (>=) result.
gteR :: (OrdR f, OrdC f x) => (f x, f x, f Bool) -> (f x, f x, f Bool)
-- | A relationship between two values and their sum.
class Merge x => SumR (x :: Type)
addR :: SumR x => (x, x, x) -> (x, x, x)
addR :: (SumR x, Num x) => (x, x, x) -> (x, x, x)
-- | A relationship between a value and its negation.
negateR :: (Num x, SumR x) => (x, x) -> (x, x)
-- | A relationship between two values and their difference.
subR :: SumR x => (x, x, x) -> (x, x, x)
-- | Lift a relationship between three values over some f (usually
-- a parameter type).
class Mapping f c => Zipping (f :: Type -> Type) (c :: Type -> Constraint) | f -> c
zipWithR :: (Zipping f c, c x, c y, c z) => (Maybe ((x, y) -> z), Maybe ((x, z) -> y), Maybe ((y, z) -> x)) -> (f x, f y, f z) -> (f x, f y, f z)
-- | Join semilattice (<>) specialised for propagator network
-- needs. Allows types to implement the notion of "knowledge
-- combination".
class Monoid x => Merge (x :: Type)
-- | Merge the news (right) into the current value (left), returning an
-- instruction on how to update the network.
(<<-) :: Merge x => x -> x -> Result x
-- | The result of merging some news into a cell's current knowledge.
data Result (x :: Type)
-- | We've learnt nothing; no updates elsewhere are needed.
Unchanged :: Result (x :: Type)
-- | We've learnt something; fire the propagators!
Changed :: x -> Result (x :: Type)
-- | We've hit a failure state; discard the computation.
Failure :: Result (x :: Type)
-- | Defines simple "levels of knowledge" about a value.
data Defined (x :: Type)
-- | Nothing has told me what this value is.
Unknown :: Defined (x :: Type)
-- | Everyone who has told me this value agrees.
Exactly :: x -> Defined (x :: Type)
-- | Two sources disagree on what this value should be.
Conflict :: Defined (x :: Type)
-- | A set type with intersection as the (<>) operation.
newtype Intersect (x :: Type)
Intersect :: HashSet x -> Intersect (x :: Type)
[toHashSet] :: Intersect (x :: Type) -> HashSet x
-- | Produce a Config with the given initial value, where the
-- refine function just tries each remaining candidate as a
-- singleton.
using :: (Applicative m, Intersectable x) => [Intersect x] -> Config m (Intersect x)
-- | A propagator network with a "focus" on a particular cell. The focus is
-- the cell that typically holds the result we're trying to compute.
data Prop (m :: Type -> Type) (content :: Type)
-- | Lift a cell into a propagator network. Mostly for internal library
-- use.
up :: Applicative m => Cell m x -> Prop m x
-- | Lower a propagator network's focal point down to a cell. Mostly for
-- internal library use.
down :: (MonadCell m, Monoid x) => Prop m x -> m (Cell m x)
lift :: forall f m c x. (MonadCell m, c x) => Lifting f c => x -> Prop m (f x)
-- | Lift a regular function into a propagator network. The function is
-- lifted into a relationship with one-way information flow.
over :: (Merge x, Merge y) => (x -> y) -> Prop m x -> Prop m y
-- | Lift a unary relationship into a propagator network. Unlike
-- over, this allows information to travel in both directions.
unary :: (Merge x, Merge y) => ((x, y) -> (x, y)) -> Prop m x -> Prop m y
-- | Lift a binary relationship into a propagator network. This allows
-- three-way information flow.
binary :: (Merge x, Merge y, Merge z) => ((x, y, z) -> (x, y, z)) -> Prop m x -> Prop m y -> Prop m z
-- | Lift a regular function over a propagator network and its
-- parameter type. Unlike over, this function abstracts away the
-- specific behaviour of the parameter type (such as Defined).
(.$) :: (Mapping f c, c x, c y) => (x -> y) -> Prop m (f x) -> Prop m (f y)
-- | Produce a network in which the raw values of a given network are used
-- to produce new parameter types. See the "wave function collapse" demo
-- for an example usage.
(.>>=) :: (FlatMapping f c, c x, c y) => Prop m (f x) -> (x -> f y) -> Prop m (f y)
-- | Lift a three-way relationship over two propagator networks' foci to
-- produce a third propagator network with a focus on the third value in
-- the relationship.
--
-- ... It's liftA2 for propagators.
zipWith' :: (Zipping f c, c x, c y, c z) => (x -> y -> z) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)
-- | Different parameter types come with different representations for
-- Bool. This function takes two propagator networks focusing on
-- boolean values, and produces a new network in which the focus is the
-- conjunction of the two values.
--
-- It's a lot of words, but the intuition is, "(&&) over
-- propagators".
(.&&) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
infixr 3 .&&
-- | Run a predicate on all values in a list, producing a list of
-- propagator networks focusing on boolean values. Then, produce a new
-- network with a focus on the conjunction of all these values.
--
-- In other words, "all over propagators".
all' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | The same as the all' function, but with access to the index of
-- the element within the array. Typically, this is useful when trying to
-- relate each element to other elements within the array.
--
-- For example, cells "surrounding" the current cell in a conceptual
-- "board".
allWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | Given a list of propagator networks with a focus on boolean values,
-- create a new network with a focus on the conjugation of all these
-- values.
--
-- In other words, "and over propagators".
and' :: (BooleanR f, MonadCell m) => [Prop m (f Bool)] -> Prop m (f Bool)
-- | Calculate the disjunction of two boolean propagator network values.
(.||) :: BooleanR f => Prop m (f Bool) -> Prop m (f Bool) -> Prop m (f Bool)
infixr 2 .||
-- | Run a predicate on all values in a list, producing a list of
-- propagator networks focusing on boolean values. Then, produce a new
-- network with a focus on the disjunction of all these values.
--
-- In other words, "any over propagators".
any' :: (BooleanR f, MonadCell m) => (x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | The same as the any' function, but with access to the index of
-- the element within the array. Typically, this is useful when trying to
-- relate each element to other elements within the array.
--
-- For example, cells "surrounding" the current cell in a conceptual
-- "board".
anyWithIndex' :: (BooleanR f, MonadCell m) => (Int -> x -> Prop m (f Bool)) -> [x] -> Prop m (f Bool)
-- | Given a list of propagator networks with a focus on boolean values,
-- create a new network with a focus on the disjunction of all these
-- values.
--
-- In other words, "or over propagators".
or' :: (BooleanR f, MonadCell m) => [Prop m (f Bool)] -> Prop m (f Bool)
-- | Given a propagator network with a focus on a boolean value, produce a
-- network with a focus on its negation.
--
-- ... It's "not over propagators".
not' :: (BooleanR f, MonadCell m) => Prop m (f Bool) -> Prop m (f Bool)
-- | Different parameter types come with different representations for
-- Bool. This value is a propagator network with a focus on a
-- polymorphic "falsey" value.
false :: (BooleanR f, MonadCell m) => Prop m (f Bool)
-- | Different parameter types come with different representations for
-- Bool. This value is a propagator network with a focus on a
-- polymorphic "truthy" value.
true :: (BooleanR f, MonadCell m) => Prop m (f Bool)
-- | Given two propagator networks, produce a new network that focuses on
-- the product of the two given networks' foci.
--
-- ... It's (*) lifted over propagator networks. The
-- reverse information flow is fractional division, (/).
(.*) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 .*
-- | Given two propagator networks, produce a new network that focuses on
-- the division of the two given networks' foci.
--
-- ... It's (/) lifted over propagator networks.
(./) :: (FractionalR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 ./
-- | Given two propagator networks, produce a new network that focuses on
-- the sum of the two given networks' foci.
--
-- ... It's (+) lifted over propagator networks.
(.+) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 6 .+
-- | Given two propagator networks, produce a new network that focuses on
-- the difference between the two given networks' foci.
--
-- ... It's (-) lifted over propagator networks.
(.-) :: (SumR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 6 .-
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be less than the second.
--
-- In other words, "it's (<) for propagators".
(.<) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .<
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be less than or equal to the second.
--
-- In other words, "it's (<=) for propagators".
(.<=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .<=
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be greater than the second.
--
-- In other words, "it's (>) for propagators".
(.>) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .>
-- | Given two propagator networks, produce a new network that calculates
-- whether the first network's focus be greater than or equal to the
-- second.
--
-- In other words, "it's (>=) for propagators".
(.>=) :: (OrdR f, OrdC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .>=
-- | Given two propagator networks, produce a new propagator network with
-- the result of testing the two for equality.
--
-- In other words, "it's (==) for propagators".
(.==) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 .==
-- | Given two propagator networks, produce a new propagator network with
-- the result of testing the two for inequality.
--
-- In other words, "it's (/=) for propagators".
(./=) :: (EqR f, EqC f x, MonadCell m) => Prop m (f x) -> Prop m (f x) -> Prop m (f Bool)
infix 4 ./=
-- | Given a list of networks, produce the conjunction of (./=)
-- applied to every possible pair. The resulting network's focus is the
-- answer to whether every propagator network's focus is different to the
-- others.
--
-- Are all the values in this list distinct?
distinct :: (EqR f, EqC f x, MonadCell m) => [Prop m (f x)] -> Prop m (f Bool)
-- | Given two propagator networks, produce a new network that focuses on
-- the modulo of the two given networks' integral foci.
--
-- ... It's mod lifted over propagator networks.
(.%.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 .%.
-- | Given two propagator networks, produce a new network that focuses on
-- the product between the two given networks' integral foci.
--
-- ... It's (*) lifted over propagator networks. Crucially,
-- the reverse information flow uses integral division, which
-- should work the same way as div.
(.*.) :: (Num x, IntegralR x) => Prop m x -> Prop m x -> Prop m x
infixl 7 .*.
-- | Given two propagator networks, produce a new network that focuses on
-- the division of the two given networks' integral foci.
--
-- ... It's div lifted over propagator networks.
(./.) :: (IntegralR x, MonadCell m) => Prop m x -> Prop m x -> Prop m x
infixl 7 ./.
-- | Produce a network that focuses on the absolute value of another
-- network's focus.
--
-- ... It's abs lifted over propagator networks.
abs' :: (AbsR x, MonadCell m) => Prop m x -> Prop m x
-- | Produce a network that focuses on the negation of another
-- network's focus.
--
-- ... It's negate lifted over propagator networks.
negate' :: (Num x, SumR x, MonadCell m) => Prop m x -> Prop m x
-- | Produce a network that focuses on the reciprocal of another
-- network's focus.
--
-- ... It's recip lifted over propagator networks.
recip' :: (Num x, FractionalR x, MonadCell m) => Prop m x -> Prop m x