packages feed

holmes (empty) → 0.1.0.0

raw patch · 30 files changed

+3608/−0 lines, 30 filesdep +basedep +containersdep +hashablesetup-changed

Dependencies added: base, containers, hashable, hedgehog, holmes, hspec, logict, mtl, primitive, relude, split, tasty, tasty-discover, tasty-hedgehog, tasty-hspec, transformers, unordered-containers

Files

+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2019 Tom Harding++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ README.lhs view
@@ -0,0 +1,504 @@+# 🕵️‍♂️ Holmes++**Holmes** is a library for computing **constraint-solving** problems. Under+the hood, it uses **propagator networks** and **conflict-directed clause+learning** to optimise the search over the parameter space.++<!--++```haskell+{-# OPTIONS_GHC -Wno-missing-methods -Wno-unused-top-binds #-}++{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE RankNTypes #-}++import Data.List (transpose)+import GHC.Generics (Generic)+import Data.Hashable (Hashable)+import Test.Hspec (describe, hspec, it, shouldBe)+```++-->++## 👟 Example++[Dinesman's+problem](https://rosettacode.org/wiki/Dinesman%27s_multiple-dwelling_problem)+is a nice first example of a constraint problem. In this problem, we imagine+**five** people — Baker, Cooper, Fletcher, Miller, and Smith —  living in a+five-story apartment block, and we must figure out the floor on which each+person lives. Here's how we state the problem with `Holmes`:++```haskell+import Data.Holmes++dinesman :: IO (Maybe [ Defined Int ])+dinesman = do+  let guesses = 5 `from` [1 .. 5]++  guesses `satisfying` \[ baker, cooper, fletcher, miller, smith ] -> and'+    [ distinct [ baker, cooper, fletcher, miller, smith ]+    , baker ./= 5+    , cooper ./= 1+    , fletcher ./= 1 .&& fletcher ./= 5+    , miller .> cooper+    , abs' (smith .- fletcher) ./= 1+    , abs' (fletcher .- cooper) ./= 1+    ]+```++## 👣 Step-by-step problem-solving++Now we've written the poster example, how do we go about **stating** and+**solving** our own constraint problems?++### ⚖️ 0. Pick a parameter type++Right now, there are **two** parameter type constructors: `Defined` and+`Intersect`. The choice of type determines the **strategy** by which we solve+the problem:++- `Defined` only permits two levels of knowledge about a value: **nothing** and+  **everything**. In other words, it doesn't support a notion of _partial_+  information; we either know a value, or we don't. This is fine for small+  problem spaces, particularly when few branches are likely to fail, but+  we can usually achieve faster results using another type.++- `Intersect` stores a set of "possible answers", and attempts to eliminate+  possibilities as the computation progresses. For problems with many+  constraints, this will produce **significantly faster** results than+  `Defined` as we can hopefully discover failures much earlier.++It would seem that `Intersect` would be the best choice in most cases, but+beware: it will only work for **small** enum types. An `Intersect Int` for+which we have no knowledge will contain every possible `Int`, and will+therefore take an **intractable** time to compute. `Defined` has no such+restrictions.++### 🗺 1. State the parameter space++Next, we need to produce a `Config` stating the search space we want to explore+when looking for satisfactory inputs. The simplest way to do this is with the+`from` function:++```hs+from :: Int -> [ x ] -> Config Holmes (Defined x)+```++```hs+from :: Int -> [ x ] -> Config Holmes (Intersect x)+```++If, for example, we wanted to solve a Sudoku problem, we might say something+like this:++```haskell+definedConfig :: Config Holmes (Defined Int)+definedConfig = 81 `from` [ 1 .. 9 ]+```++We read this as, "`81` variables whose values must all be numbers between `1`+and `9`". At this point, we place no constraints (such as uniqueness of rows or+columns); we're just stating the possible range of values that could exist in+each parameter.++We could do the same for `Intersect`, but we'd first need to produce some+**enum** type to represent our parameter space:++```haskell+data Value = V1 | V2 | V3 | V4 | V5 | V6 | V7 | V8 | V9+  deriving stock (Eq, Ord, Show, Enum, Bounded, Generic)+  deriving anyclass (Hashable)++instance Num Value where -- Syntactic sugar for numeric literals.+  fromInteger = toEnum . pred . fromInteger+```++_Now_, we can produce an `Intersect` parameter space. Because we can now work+with a type who has only `9` values, rather than all possible `Int` values,+producing the initial possibilities list becomes tractable:++```haskell+intersectConfig :: Config Holmes (Intersect Value)+intersectConfig = 81 `from` [ 1 .. 9 ]+```++There's one more function that lets us do slightly better with an `Intersect`+strategy, and that's `using`:++```hs+using :: [ Intersect Value ] -> Config Holmes (Intersect Value)+```++With `using`, we can give a precise "initial state" for all the `Intersect`+variables in our system. This, it turns out, is very convenient when we're+trying to state sudoku problems:++```haskell+squares :: Config Holmes (Intersect Value)+squares = let x = mempty in using+    [ x, 5, 6,   x, x, 3,   x, x, x+    , 8, 1, x,   x, x, x,   x, x, x+    , x, x, x,   5, 4, x,   x, x, x++    , x, x, 4,   x, x, x,   x, 8, 2+    , 6, x, 8,   2, x, 4,   3, x, 7+    , 7, 2, x,   x, x, x,   4, x, x++    , x, x, x,   x, 7, 8,   x, x, x+    , x, x, x,   x, x, x,   x, 9, 3+    , x, x, x,   3, x, x,   8, 2, x+    ]+```++Now, let's write some **constraints**!++### 📯 2. Declare your constraints++Typically, your constraints should be stated as a **predicate** on the input+**parameters**, with a type that, when specialised to your problem, should look+something like `[Prop Holmes (Defined Int)] -> Prop Holmes (Defined Bool)`.+Now, what's this `Prop` type?++#### 🕸 Propagators++If this library has done its job properly, this predicate shouldn't look too+dissimilar to regular predicates. However, behind the scenes, the `Prop` type+is wiring up a lot of **relationships**.++As an example, consider the `(+)` function. This has two inputs and one output,+and the output is the sum of the two inputs. This is totally fixed, and there's+nothing we can do about it. This is fine when we write normal programs, because+we only have **one-way information flow**: input flows to output, and it's as+simple as that.++When we come to constraint problems, however, we have **multi-way information+flow**: we might know the output before we know the inputs! Ideally, it'd be+nice in these situations if we could "work backwards" to the information we're+missing.++When we say `x .+ y .== z`, we actually wire up **multiple** relationships:+`x + y = z`, `z - y = x`, and `z - x = y`. That way, as soon as we learn+**two** of the three values involved in addition, we can infer the other!++The operators provided by this library aim to **maximise** information flow+around a propagator network by automatically wiring up all the different+**identities** for all the different operators. We'll see later that this+allows us to write seemingly-magical functions like `backwards`: given a+function and an **output**, we can produce the function's input!++#### 🛠 The problem-solving toolkit++With all this in mind, the following functions are available to us for+multi-directional information flow. We'll leave the type signatures to Haddock,+and instead just run through the functions and either their analogous regular+functions _or_ a brief explanation of what they do:++##### 🎚 Boolean functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.&&)` | `(&&)` |+| `all'` | `all` |+| `allWithIndex'` | `all'`, but the predicate _also_ receives the list index |+| `and'` | `and` |+| `(.\|\|)` | `(\|\|)` |+| `any'` | `any` |+| `anyWithIndex'` | `any'`, but the predicate _also_ receives the list index |+| `or'` | `or` |+| `not'` | `not` |+| `false` | `False` |+| `true` | `True` |++##### 🏳️‍🌈 Equality functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.==)` | `(==)` |+| `(./=)` | `(/=)` |+| `distinct` | Are all list elements _different_ (according to `(./=)`)? |++##### 🥈 Comparison functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.<)` | `(<)` |+| `(.<=)` | `(<=)` |+| `(.>)` | `(>)` |+| `(.>=)` | `(>=)` |++##### 🎓 Arithmetic functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.*)` | `(*)` |+| `(./)` | `(/)` |+| `(.+)` | `(+)` |+| `(.-)` | `(-)` |+| `(.%.)` | `mod` |+| `(.*.)` | `(*)` for _integral_ functions |+| `(./.)` | `div` |+| `abs'` | `abs` |+| `negate'` | `negate` |+| `recip'` | `recip` |++##### 🌱 Information-generating functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.$)` | Apply a function to the value _within_ the parameter type.+| `zipWith'` | Similar to `liftA2`; generate results from the parameters. |+| `(.>>=)` | Turn each value within the parameter type into the parameter type. |++The analogy gets stretched a bit here, unfortunately. It's perhaps helpful to+think of these functions in terms of `Intersect`:++- `(.$)` maps over the remaining candidates in an `Intersect`.++- `zipWith'` creates an `Intersect` of the **cartesian product** of the two+  given `Intersect`s, with the pairs applied to the given function.++- `(.>>=)` takes every remaining candidate, applies the given function, then+  **unions** the results to produce an `Intersect` of all possible results.++---++Using the above toolkit, we could express the constraints of our **sudoku**+example. After we establish some less interesting functions for splitting up+our `81` inputs into helpful chunks...++```haskell+rows :: [ x ] -> [[ x ]]+rows [] = []+rows xs = take 9 xs : rows (drop 9 xs)++columns :: [ x ] -> [[ x ]]+columns = transpose . rows++subsquares :: [ x ] -> [[ x ]]+subsquares xs = do+  x <- [ 0 .. 2 ]+  y <- [ 0 .. 2 ]++  let subrows = take 3 (drop (y * 3) (rows xs))+      values  = foldMap (take 3 . drop (x * 3)) subrows++  pure values+```++... we can use the **propagator toolkit** to specify our constraints in a+delightfully straightforward way:++```haskell+constraints :: forall m. MonadCell m => [ Prop m (Intersect Value) ] -> Prop m (Intersect Bool)+constraints board = and'+  [ all' distinct (columns    board)+  , all' distinct (rows       board)+  , all' distinct (subsquares board)+  ]+```++> _The type signature looks a little bit **ugly** here, but the polymorphism is+to guarantee that predicate computations are totally generic propagator+networks that can be run in any interpretation strategy. As we'll see later,+`Holmes` isn't the only one capable of solving a mystery!_+>+> _Typically, we write the constraint predicate inline (as we did for the+> Dinesman example above), so we never usually write this signature anyway!)_++We've explained all the rules and **constraints** of the sudoku puzzle, and+designed a propagator network to solve it! Now, why don't we get ourselves a+**solution**?++### 💡 3. Solving the puzzle++Currently, `Holmes` only exposes two strategies for solving constraint+problems:++- `satisfying`, which returns the **first** valid configuration that is found,+  **if one exists**. As soon as this result has been found, computation will+  cease, and this program will return the result.++- `whenever`, which returns **all** valid configurations in the search space.+  This function could potentially run for a long time, depending on the size of+  the search space, so you might find better results by sticking to+  `satisfying` and simply adding more constraints to eliminate the results you+  don't want!++These functions are named to be written as **infix** functions, which hopefully+makes our programs a lot easier to read:++```haskell+sudoku :: IO (Maybe [ Intersect Value ])+sudoku = squares `satisfying` constraints+```++At last, we combine the three steps to solve our problem. This README is a+**literate Haskell file** containing a **complete sudoku solver**, so feel free+to run `cabal new-test readme` and see for yourself!++## 🎁 Bonus surprises++We've now covered almost the **full API** of the library. However, there are a+couple extra little surprises in there for the curious few:++### 📖 `Control.Monad.Watson`++`Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike+`Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is+thus is a much purer soul.++Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and+`whenever` functions to return results _without_ the `IO` wrapper, thus making+these computations **observably pure**! For most computations — certainly those+outlined in this README — `Watson` is more than capable of deducing results.++### 🎲 Random restart with `shuffle`++`Watson` isn't quite as capable as `Holmes`, however. Consider a typical+`Config`:++```haskell+example :: Config Holmes (Defined Int)+example = 1 `from` [1 .. 10]+```++With this `Config`, a program will run with a single parameter. For the _first_+run, that parameter will be set to `Exactly 1`. For the _second_ run, it will+be set to `Exactly 2`. In other words, it tries each value **in order**.++For many problems, however, we can get to results faster — or produce more+desirable results — by applying some **randomness** to this order. This is+especially useful in problems such as **procedural generation**, where+randomness tends to lead to more **natural**-seeming outputs. See the+`WaveFunctionCollapse` example for more details!++### ♻️ Running functions forwards _and_ backwards++With `satisfying` and `whenever`, we build a **predicate** on the input+parameters we supply. However, we can use propagators to create normal+functions, too! Consider the following function:++```haskell+celsius2fahrenheit :: MonadCell m => Prop m (Defined Double) -> Prop m (Defined Double)+celsius2fahrenheit c = c .* (9 ./ 5) .+ 32+```++This function converts a temperature written in **celsius** to **fahrenheit**.+The _interesting_ part of this, however, is that this is a function over+**propagator networks**. This means that, while we can use it as a _regular_+function...++```haskell+fahrenheit :: Maybe (Defined Double)+fahrenheit = forward celsius2fahrenheit 40.0 -- Just 104.0+```++... the "input" and "output" labels are meaningless! In fact, we can just as+easily pass a value to the function as the **output** and get back the+**input**!++```haskell+celsius :: Maybe (Defined Double)+celsius = backward celsius2fahrenheit 104.0 -- Just 40.0+```++> _Because neither `forward` nor `backward` require any parameter search, they+> are both computed by `Watson`, so the results are **pure**!_++<!--++```haskell+main :: IO ()+main = hspec do+  describe "Dinesman's Multiple Dwellings problem" do+    it "should be solved successfully" do+      dinesman >>= \result ->+        result `shouldBe` Just [ 3, 2, 4, 5, 1 ]++  describe "Sudoku" do+    it "should be solved successfully" do+      sudoku >>= \result ->+        result `shouldBe` Just solution++  describe "forward / backward" do+    it "works forwards"  do fahrenheit `shouldBe` Just 104.0+    it "works backwards" do celsius    `shouldBe` Just  40.0++solution :: [Intersect Value]+solution+  = [ 4, 5, 6,   1, 8, 3,   2, 7, 9+    , 8, 1, 2,   6, 9, 7,   5, 3, 4+    , 3, 7, 9,   5, 4, 2,   6, 1, 8++    , 1, 3, 4,   7, 6, 5,   9, 8, 2+    , 6, 9, 8,   2, 1, 4,   3, 5, 7+    , 7, 2, 5,   8, 3, 9,   4, 6, 1++    , 2, 6, 3,   9, 7, 8,   1, 4, 5+    , 5, 8, 1,   4, 2, 6,   7, 9, 3+    , 9, 4, 7,   3, 5, 1,   8, 2, 6+    ]+```++-->++## 🚂 Exploring the code++Now we've covered the **what**, maybe you're interested in the **how**! If+you're new to the **code** and want to get a feel for how the library works:++- The best place to start is probably in `Data/JoinSemilattice/Class/*`+  (we can ignore `Merge` until the next step). These will give you an idea of+  how we represent **relationships** (as opposed to **functions**) in `Holmes`.++- After that, `Control/Monad/Cell/Class.hs` gives an overview of the+  primitives for building a propagator network. In particular, see `unary` and+  `binary` for an idea of how we lift our **relationships** into a network.+  Here's where `src/Data/JoinSemilattice/Class/Merge` gets used, too, so the+  `write` primitive should give you an idea of why it's useful.++- `src/Data/Propagator.hs` introduces the high-level user-facing abstraction+  for stating constraints. Most of these functions are just wrapped calls to+  the aforementioned `unary` or `binary`, and really just add some syntactic+  sugar.++- Finally, `Control/Monad/MoriarT.hs` is a full implementation of the interface+  including support for **provenance** and **backtracking**. It also uses the+  functions in `Data/CDCL.hs` to optimise the parameter search. This is the+  base transformer on top of which we build `Control/Monad/Holmes.hs` _and_+  `Control/Monad/Watson.hs`.++Thus concludes our **whistle-stop tour** of my favourite sights in the+repository!++## ☎️ Questions?++If anything isn't clear, feel free to open an issue, or just message [me on+Twitter](https://twitter.com/am_i_tom); it's where you'll most likely get a+reply! I want this project to be an accessible way to approach the fields of+**propagators**, **constraint-solving**, and **CDCL**. If there's anything I+can do to improve this repository towards that goal, please **let me know**!++## 💐 Acknowledgements++- [Edward Kmett](https://twitter.com/kmett), whose+  [propagators repository](https://github.com/ekmett/propagators)\* gave us the+  `Prop` abstraction. I spent several months looking for alternative ways to+  represent computations, and never came close to something as neat.++- [Marco Sampellegrini](https://twitter.com/_alpacaaa), [Alex+  Peitsinis](https://twitter.com/alexpeits), [Irene+  Papakonstantinou](https://twitter.com/futumorphism), and plenty others who+  have helped me figure out how to present this library in a+  maximally-accessible way.++\* _This repository also approaches propagator network computations using Andy+Gill's [observable sharing](http://hackage.haskell.org/package/data-reify)+methods, which may be of interest! Neither `Holmes` nor `Watson` implement+this, as it requires some small breaks to purity and referential transparency,+of which users must be aware. We sacrifice some performance gains for ease of+use._
+ README.md view
@@ -0,0 +1,504 @@+# 🕵️‍♂️ Holmes++**Holmes** is a library for computing **constraint-solving** problems. Under+the hood, it uses **propagator networks** and **conflict-directed clause+learning** to optimise the search over the parameter space.++<!--++```haskell+{-# OPTIONS_GHC -Wno-missing-methods -Wno-unused-top-binds #-}++{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE RankNTypes #-}++import Data.List (transpose)+import GHC.Generics (Generic)+import Data.Hashable (Hashable)+import Test.Hspec (describe, hspec, it, shouldBe)+```++-->++## 👟 Example++[Dinesman's+problem](https://rosettacode.org/wiki/Dinesman%27s_multiple-dwelling_problem)+is a nice first example of a constraint problem. In this problem, we imagine+**five** people — Baker, Cooper, Fletcher, Miller, and Smith —  living in a+five-story apartment block, and we must figure out the floor on which each+person lives. Here's how we state the problem with `Holmes`:++```haskell+import Data.Holmes++dinesman :: IO (Maybe [ Defined Int ])+dinesman = do+  let guesses = 5 `from` [1 .. 5]++  guesses `satisfying` \[ baker, cooper, fletcher, miller, smith ] -> and'+    [ distinct [ baker, cooper, fletcher, miller, smith ]+    , baker ./= 5+    , cooper ./= 1+    , fletcher ./= 1 .&& fletcher ./= 5+    , miller .> cooper+    , abs' (smith .- fletcher) ./= 1+    , abs' (fletcher .- cooper) ./= 1+    ]+```++## 👣 Step-by-step problem-solving++Now we've written the poster example, how do we go about **stating** and+**solving** our own constraint problems?++### ⚖️ 0. Pick a parameter type++Right now, there are **two** parameter type constructors: `Defined` and+`Intersect`. The choice of type determines the **strategy** by which we solve+the problem:++- `Defined` only permits two levels of knowledge about a value: **nothing** and+  **everything**. In other words, it doesn't support a notion of _partial_+  information; we either know a value, or we don't. This is fine for small+  problem spaces, particularly when few branches are likely to fail, but+  we can usually achieve faster results using another type.++- `Intersect` stores a set of "possible answers", and attempts to eliminate+  possibilities as the computation progresses. For problems with many+  constraints, this will produce **significantly faster** results than+  `Defined` as we can hopefully discover failures much earlier.++It would seem that `Intersect` would be the best choice in most cases, but+beware: it will only work for **small** enum types. An `Intersect Int` for+which we have no knowledge will contain every possible `Int`, and will+therefore take an **intractable** time to compute. `Defined` has no such+restrictions.++### 🗺 1. State the parameter space++Next, we need to produce a `Config` stating the search space we want to explore+when looking for satisfactory inputs. The simplest way to do this is with the+`from` function:++```hs+from :: Int -> [ x ] -> Config Holmes (Defined x)+```++```hs+from :: Int -> [ x ] -> Config Holmes (Intersect x)+```++If, for example, we wanted to solve a Sudoku problem, we might say something+like this:++```haskell+definedConfig :: Config Holmes (Defined Int)+definedConfig = 81 `from` [ 1 .. 9 ]+```++We read this as, "`81` variables whose values must all be numbers between `1`+and `9`". At this point, we place no constraints (such as uniqueness of rows or+columns); we're just stating the possible range of values that could exist in+each parameter.++We could do the same for `Intersect`, but we'd first need to produce some+**enum** type to represent our parameter space:++```haskell+data Value = V1 | V2 | V3 | V4 | V5 | V6 | V7 | V8 | V9+  deriving stock (Eq, Ord, Show, Enum, Bounded, Generic)+  deriving anyclass (Hashable)++instance Num Value where -- Syntactic sugar for numeric literals.+  fromInteger = toEnum . pred . fromInteger+```++_Now_, we can produce an `Intersect` parameter space. Because we can now work+with a type who has only `9` values, rather than all possible `Int` values,+producing the initial possibilities list becomes tractable:++```haskell+intersectConfig :: Config Holmes (Intersect Value)+intersectConfig = 81 `from` [ 1 .. 9 ]+```++There's one more function that lets us do slightly better with an `Intersect`+strategy, and that's `using`:++```hs+using :: [ Intersect Value ] -> Config Holmes (Intersect Value)+```++With `using`, we can give a precise "initial state" for all the `Intersect`+variables in our system. This, it turns out, is very convenient when we're+trying to state sudoku problems:++```haskell+squares :: Config Holmes (Intersect Value)+squares = let x = mempty in using+    [ x, 5, 6,   x, x, 3,   x, x, x+    , 8, 1, x,   x, x, x,   x, x, x+    , x, x, x,   5, 4, x,   x, x, x++    , x, x, 4,   x, x, x,   x, 8, 2+    , 6, x, 8,   2, x, 4,   3, x, 7+    , 7, 2, x,   x, x, x,   4, x, x++    , x, x, x,   x, 7, 8,   x, x, x+    , x, x, x,   x, x, x,   x, 9, 3+    , x, x, x,   3, x, x,   8, 2, x+    ]+```++Now, let's write some **constraints**!++### 📯 2. Declare your constraints++Typically, your constraints should be stated as a **predicate** on the input+**parameters**, with a type that, when specialised to your problem, should look+something like `[Prop Holmes (Defined Int)] -> Prop Holmes (Defined Bool)`.+Now, what's this `Prop` type?++#### 🕸 Propagators++If this library has done its job properly, this predicate shouldn't look too+dissimilar to regular predicates. However, behind the scenes, the `Prop` type+is wiring up a lot of **relationships**.++As an example, consider the `(+)` function. This has two inputs and one output,+and the output is the sum of the two inputs. This is totally fixed, and there's+nothing we can do about it. This is fine when we write normal programs, because+we only have **one-way information flow**: input flows to output, and it's as+simple as that.++When we come to constraint problems, however, we have **multi-way information+flow**: we might know the output before we know the inputs! Ideally, it'd be+nice in these situations if we could "work backwards" to the information we're+missing.++When we say `x .+ y .== z`, we actually wire up **multiple** relationships:+`x + y = z`, `z - y = x`, and `z - x = y`. That way, as soon as we learn+**two** of the three values involved in addition, we can infer the other!++The operators provided by this library aim to **maximise** information flow+around a propagator network by automatically wiring up all the different+**identities** for all the different operators. We'll see later that this+allows us to write seemingly-magical functions like `backwards`: given a+function and an **output**, we can produce the function's input!++#### 🛠 The problem-solving toolkit++With all this in mind, the following functions are available to us for+multi-directional information flow. We'll leave the type signatures to Haddock,+and instead just run through the functions and either their analogous regular+functions _or_ a brief explanation of what they do:++##### 🎚 Boolean functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.&&)` | `(&&)` |+| `all'` | `all` |+| `allWithIndex'` | `all'`, but the predicate _also_ receives the list index |+| `and'` | `and` |+| `(.\|\|)` | `(\|\|)` |+| `any'` | `any` |+| `anyWithIndex'` | `any'`, but the predicate _also_ receives the list index |+| `or'` | `or` |+| `not'` | `not` |+| `false` | `False` |+| `true` | `True` |++##### 🏳️‍🌈 Equality functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.==)` | `(==)` |+| `(./=)` | `(/=)` |+| `distinct` | Are all list elements _different_ (according to `(./=)`)? |++##### 🥈 Comparison functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.<)` | `(<)` |+| `(.<=)` | `(<=)` |+| `(.>)` | `(>)` |+| `(.>=)` | `(>=)` |++##### 🎓 Arithmetic functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.*)` | `(*)` |+| `(./)` | `(/)` |+| `(.+)` | `(+)` |+| `(.-)` | `(-)` |+| `(.%.)` | `mod` |+| `(.*.)` | `(*)` for _integral_ functions |+| `(./.)` | `div` |+| `abs'` | `abs` |+| `negate'` | `negate` |+| `recip'` | `recip` |++##### 🌱 Information-generating functions++| Function | Analogous function / notes |+| --:|:-- |+| `(.$)` | Apply a function to the value _within_ the parameter type.+| `zipWith'` | Similar to `liftA2`; generate results from the parameters. |+| `(.>>=)` | Turn each value within the parameter type into the parameter type. |++The analogy gets stretched a bit here, unfortunately. It's perhaps helpful to+think of these functions in terms of `Intersect`:++- `(.$)` maps over the remaining candidates in an `Intersect`.++- `zipWith'` creates an `Intersect` of the **cartesian product** of the two+  given `Intersect`s, with the pairs applied to the given function.++- `(.>>=)` takes every remaining candidate, applies the given function, then+  **unions** the results to produce an `Intersect` of all possible results.++---++Using the above toolkit, we could express the constraints of our **sudoku**+example. After we establish some less interesting functions for splitting up+our `81` inputs into helpful chunks...++```haskell+rows :: [ x ] -> [[ x ]]+rows [] = []+rows xs = take 9 xs : rows (drop 9 xs)++columns :: [ x ] -> [[ x ]]+columns = transpose . rows++subsquares :: [ x ] -> [[ x ]]+subsquares xs = do+  x <- [ 0 .. 2 ]+  y <- [ 0 .. 2 ]++  let subrows = take 3 (drop (y * 3) (rows xs))+      values  = foldMap (take 3 . drop (x * 3)) subrows++  pure values+```++... we can use the **propagator toolkit** to specify our constraints in a+delightfully straightforward way:++```haskell+constraints :: forall m. MonadCell m => [ Prop m (Intersect Value) ] -> Prop m (Intersect Bool)+constraints board = and'+  [ all' distinct (columns    board)+  , all' distinct (rows       board)+  , all' distinct (subsquares board)+  ]+```++> _The type signature looks a little bit **ugly** here, but the polymorphism is+to guarantee that predicate computations are totally generic propagator+networks that can be run in any interpretation strategy. As we'll see later,+`Holmes` isn't the only one capable of solving a mystery!_+>+> _Typically, we write the constraint predicate inline (as we did for the+> Dinesman example above), so we never usually write this signature anyway!)_++We've explained all the rules and **constraints** of the sudoku puzzle, and+designed a propagator network to solve it! Now, why don't we get ourselves a+**solution**?++### 💡 3. Solving the puzzle++Currently, `Holmes` only exposes two strategies for solving constraint+problems:++- `satisfying`, which returns the **first** valid configuration that is found,+  **if one exists**. As soon as this result has been found, computation will+  cease, and this program will return the result.++- `whenever`, which returns **all** valid configurations in the search space.+  This function could potentially run for a long time, depending on the size of+  the search space, so you might find better results by sticking to+  `satisfying` and simply adding more constraints to eliminate the results you+  don't want!++These functions are named to be written as **infix** functions, which hopefully+makes our programs a lot easier to read:++```haskell+sudoku :: IO (Maybe [ Intersect Value ])+sudoku = squares `satisfying` constraints+```++At last, we combine the three steps to solve our problem. This README is a+**literate Haskell file** containing a **complete sudoku solver**, so feel free+to run `cabal new-test readme` and see for yourself!++## 🎁 Bonus surprises++We've now covered almost the **full API** of the library. However, there are a+couple extra little surprises in there for the curious few:++### 📖 `Control.Monad.Watson`++`Watson` knows `Holmes`' methods, and can apply them to compute results. Unlike+`Holmes`, however, `Watson` is built on top of `ST` rather than `IO`, and is+thus is a much purer soul.++Users can import `Control.Monad.Watson` and use the equivalent `satisfying` and+`whenever` functions to return results _without_ the `IO` wrapper, thus making+these computations **observably pure**! For most computations — certainly those+outlined in this README — `Watson` is more than capable of deducing results.++### 🎲 Random restart with `shuffle`++`Watson` isn't quite as capable as `Holmes`, however. Consider a typical+`Config`:++```haskell+example :: Config Holmes (Defined Int)+example = 1 `from` [1 .. 10]+```++With this `Config`, a program will run with a single parameter. For the _first_+run, that parameter will be set to `Exactly 1`. For the _second_ run, it will+be set to `Exactly 2`. In other words, it tries each value **in order**.++For many problems, however, we can get to results faster — or produce more+desirable results — by applying some **randomness** to this order. This is+especially useful in problems such as **procedural generation**, where+randomness tends to lead to more **natural**-seeming outputs. See the+`WaveFunctionCollapse` example for more details!++### ♻️ Running functions forwards _and_ backwards++With `satisfying` and `whenever`, we build a **predicate** on the input+parameters we supply. However, we can use propagators to create normal+functions, too! Consider the following function:++```haskell+celsius2fahrenheit :: MonadCell m => Prop m (Defined Double) -> Prop m (Defined Double)+celsius2fahrenheit c = c .* (9 ./ 5) .+ 32+```++This function converts a temperature written in **celsius** to **fahrenheit**.+The _interesting_ part of this, however, is that this is a function over+**propagator networks**. This means that, while we can use it as a _regular_+function...++```haskell+fahrenheit :: Maybe (Defined Double)+fahrenheit = forward celsius2fahrenheit 40.0 -- Just 104.0+```++... the "input" and "output" labels are meaningless! In fact, we can just as+easily pass a value to the function as the **output** and get back the+**input**!++```haskell+celsius :: Maybe (Defined Double)+celsius = backward celsius2fahrenheit 104.0 -- Just 40.0+```++> _Because neither `forward` nor `backward` require any parameter search, they+> are both computed by `Watson`, so the results are **pure**!_++<!--++```haskell+main :: IO ()+main = hspec do+  describe "Dinesman's Multiple Dwellings problem" do+    it "should be solved successfully" do+      dinesman >>= \result ->+        result `shouldBe` Just [ 3, 2, 4, 5, 1 ]++  describe "Sudoku" do+    it "should be solved successfully" do+      sudoku >>= \result ->+        result `shouldBe` Just solution++  describe "forward / backward" do+    it "works forwards"  do fahrenheit `shouldBe` Just 104.0+    it "works backwards" do celsius    `shouldBe` Just  40.0++solution :: [Intersect Value]+solution+  = [ 4, 5, 6,   1, 8, 3,   2, 7, 9+    , 8, 1, 2,   6, 9, 7,   5, 3, 4+    , 3, 7, 9,   5, 4, 2,   6, 1, 8++    , 1, 3, 4,   7, 6, 5,   9, 8, 2+    , 6, 9, 8,   2, 1, 4,   3, 5, 7+    , 7, 2, 5,   8, 3, 9,   4, 6, 1++    , 2, 6, 3,   9, 7, 8,   1, 4, 5+    , 5, 8, 1,   4, 2, 6,   7, 9, 3+    , 9, 4, 7,   3, 5, 1,   8, 2, 6+    ]+```++-->++## 🚂 Exploring the code++Now we've covered the **what**, maybe you're interested in the **how**! If+you're new to the **code** and want to get a feel for how the library works:++- The best place to start is probably in `Data/JoinSemilattice/Class/*`+  (we can ignore `Merge` until the next step). These will give you an idea of+  how we represent **relationships** (as opposed to **functions**) in `Holmes`.++- After that, `Control/Monad/Cell/Class.hs` gives an overview of the+  primitives for building a propagator network. In particular, see `unary` and+  `binary` for an idea of how we lift our **relationships** into a network.+  Here's where `src/Data/JoinSemilattice/Class/Merge` gets used, too, so the+  `write` primitive should give you an idea of why it's useful.++- `src/Data/Propagator.hs` introduces the high-level user-facing abstraction+  for stating constraints. Most of these functions are just wrapped calls to+  the aforementioned `unary` or `binary`, and really just add some syntactic+  sugar.++- Finally, `Control/Monad/MoriarT.hs` is a full implementation of the interface+  including support for **provenance** and **backtracking**. It also uses the+  functions in `Data/CDCL.hs` to optimise the parameter search. This is the+  base transformer on top of which we build `Control/Monad/Holmes.hs` _and_+  `Control/Monad/Watson.hs`.++Thus concludes our **whistle-stop tour** of my favourite sights in the+repository!++## ☎️ Questions?++If anything isn't clear, feel free to open an issue, or just message [me on+Twitter](https://twitter.com/am_i_tom); it's where you'll most likely get a+reply! I want this project to be an accessible way to approach the fields of+**propagators**, **constraint-solving**, and **CDCL**. If there's anything I+can do to improve this repository towards that goal, please **let me know**!++## 💐 Acknowledgements++- [Edward Kmett](https://twitter.com/kmett), whose+  [propagators repository](https://github.com/ekmett/propagators)\* gave us the+  `Prop` abstraction. I spent several months looking for alternative ways to+  represent computations, and never came close to something as neat.++- [Marco Sampellegrini](https://twitter.com/_alpacaaa), [Alex+  Peitsinis](https://twitter.com/alexpeits), [Irene+  Papakonstantinou](https://twitter.com/futumorphism), and plenty others who+  have helped me figure out how to present this library in a+  maximally-accessible way.++\* _This repository also approaches propagator network computations using Andy+Gill's [observable sharing](http://hackage.haskell.org/package/data-reify)+methods, which may be of interest! Neither `Holmes` nor `Watson` implement+this, as it requires some small breaks to purity and referential transparency,+of which users must be aware. We sacrifice some performance gains for ease of+use._
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/Futoshiki.hs view
@@ -0,0 +1,90 @@+{-# OPTIONS_GHC -Wno-missing-methods #-}++{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}++-- Futoshiki is one of my favourite number games. If you're unfamiliar with the+-- rules, we'll use the following configuration for this example:+--+-- ┌───┐   ┌───┐   ┌───┐   ┌───┐+-- │   │   │   │ < │   │ < │   │+-- └───┘   └───┘   └───┘   └───┘+--   ^+-- ┌───┐   ┌───┐   ┌───┐   ┌───┐+-- │   │   │   │   │   │   │ 3 │+-- └───┘   └───┘   └───┘   └───┘+--           v+-- ┌───┐   ┌───┐   ┌───┐   ┌───┐+-- │   │   │   │   │   │   │   │+-- └───┘   └───┘   └───┘   └───┘+--                           ^+-- ┌───┐   ┌───┐   ┌───┐   ┌───┐+-- │   │   │   │   │   │   │   │+-- └───┘   └───┘   └───┘   └───┘+--+-- The goal is to fill a four-by-four board with numbers `[1 .. 4]` such that+-- every number is __unique__ in its __row__ and __column__. As well as that,+-- if a @<@ symbol appears between two cells, the right cell must be **greater+-- than** the left. This "greater than" symbol can appear between any two+-- adjacent cells, though, so we represent it using the @<@, @>@, @^@, and @v@+-- symbols, depending on its direction.+module Futoshiki where++import Data.Hashable (Hashable)+import Control.Monad.Watson (satisfying)+import Data.Holmes hiding (satisfying)+import Data.List (transpose)+import Data.List.Split (chunksOf)+import GHC.Generics (Generic)+import Test.Hspec++-- We'll be using @Intersect@ for this one, so we need to establish our enum+-- type for the parameter space.+data Choice = V1 | V2 | V3 | V4+  deriving stock (Eq, Ord, Show, Bounded, Enum, Generic)+  deriving anyclass (Hashable)++instance Num Choice where+  fromInteger = toEnum . pred . fromInteger++-- Here's the translation of the board shown above, with the constraints+-- expressed as a `Prop` predicate:+solution :: Maybe [ Intersect Choice ]+solution = do++  -- For this example, the board is a @4 × 4@ grid with each cell being a+  -- number between @1@ and @4@.+  (16 `from` [1 .. 4]) `satisfying` \board -> do+    let rows    = chunksOf 4 board+        columns = transpose rows++    and'+      [ -- First up, the rules of the game:+        all' distinct rows+      , all' distinct columns++        -- Then, the constraints on this particular board:+      , (rows !! 0 !! 1) .< (rows !! 0 !! 2)+      , (rows !! 0 !! 2) .< (rows !! 0 !! 3)+      , (rows !! 0 !! 0) .< (rows !! 1 !! 0)+      , (rows !! 1 !! 3) .== 3                +      , (rows !! 2 !! 1) .< (rows !! 1 !! 1)+      , (rows !! 2 !! 3) .< (rows !! 3 !! 3)+      ]++-- All being well, this should be the result! Use `cabal new-test examples` to+-- run these tests and check for correct solutions.++spec_futoshiki+  = it "computes the solution" do+      solution `shouldBe` Just+        [   1,   2,   3,   4++        ,   2,   4,   1,   3++        ,   4,   3,   2,   1++        ,   3,   1,   4,   2+        ]
+ examples/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}
+ examples/WaveFunctionCollapse.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ViewPatterns #-}+module WaveFunctionCollapse where++import Data.Function ((&))+import Data.Hashable (Hashable)+import Data.Holmes+import Data.JoinSemilattice.Intersect (fromList, singleton, toList)+import Data.List (transpose)+import Data.List.Split (chunksOf)+import Data.Maybe (isJust, mapMaybe)+import Data.Propagator (lift)+import GHC.Generics (Generic)+import Relude ((!!?))+import Test.Hspec (Spec, it, shouldBe)++-- Wave function collapse* is an algorithm that works by placing constraints+-- between each cell and their neighbours. A cell is randomly specialised to a+-- particular value, and the effects ripple out via the constraints. Then,+-- another cell is specialised, and the process repeats until all cells are+-- specialised.+--+-- It turns out that this is actually just a special case of the propagator+-- idea, and specifically the `Intersect` strategy. While we're not going to+-- implement the full algorithm here, we'll demonstrate the idea with a+-- simplified version in order to draw some desert island maps!+--+-- * https://github.com/mxgmn/WaveFunctionCollapse++--------------------------------------------------++-- First, we'll start with a type to specify the possible terrain types in our+-- map:+data Tile = Water | Sand | Grass | Tree+  deriving stock (Eq, Ord, Bounded, Enum, Generic)+  deriving anyclass (Hashable)++instance Show Tile where+  show = \case+    Water -> "💦"+    Sand  -> "🔅"+    Grass -> "🍀"+    Tree  -> "🌲"++-- Now, we'll specify some constraints on our neighbours. Again, this is a very+-- simplified version of the WaveFunctionCollapse concept - typically, we'd+-- have far more "tiles", and neighbours would be chosen by properties attached+-- to each edge of each tile.++surroundings :: Tile -> Intersect Tile+surroundings = fromList . \case++  -- A tree must be entirely surrounded by grass. Two trees cannot touch, and+  -- trees cannot be on beaches or in water.+  Tree -> [ Grass ]++  -- The only thing that can neighbour water is more water or sand. This means+  -- that every island has a beach, and we might even get some small islands+  -- out in water, too!+  Water -> [ Sand, Water ]++  -- Sand must sit between water and grass. Note that this simple system+  -- doesn't prevent random sand tiles amid grass; we'd need to specify the+  -- constraints in a more comprehensive way to mitigate this.+  Sand -> [ Sand, Water, Grass ]++  -- Grass can neighbour sand, more grass, or trees!+  Grass -> [ Sand, Tree, Grass ]++-- Get the neighbours of a cell at a given index.+neighbours :: Int -> [ x ] -> [ x ]+neighbours index board = mapMaybe (board !!?)+  [ index - 21, index - 20, index - 19+  , index -  1, {- HOME! -} index +  1+  , index + 19, index + 20, index + 21+  ]++-- The 20 × 20 board makes up 400 tiles.+tiles :: Config Holmes (Intersect Tile)+tiles = shuffle (400 `from` [ Water, Sand, Grass, Tree ])++--------------------------------------------------++maps :: IO (Maybe [ Intersect Tile ])+maps = do+  tiles `satisfying` \board@(chunksOf 20 -> rows) -> do+    let columns = transpose rows++    and'+      [ -- As we're trying to draw an island, we'll surround the whole map with+        -- water:+        all' (.== lift (singleton Water)) (head rows)+      , all' (.== lift (singleton Water)) (last rows)++      , all' (.== lift (singleton Water)) (head columns)+      , all' (.== lift (singleton Water)) (last columns)++        -- To generate more interesting maps, we'll require that every valid+        -- map contains at least one tree (and thus has at least one 5 × 5+        -- island).+      , any' (.== lift (singleton Tree)) board++        -- For each tile, find the valid surrounding tiles, then constraint its+        -- neighbours to those possibilities.+      , board & allWithIndex' \index tile -> do+          let candidates = tile .>>= surroundings+          all' (.== candidates) (neighbours index board)+      ]++-- If you want to see some of the generated maps, run `cabal new-repl examples`+-- and use the following function to print out a result:+--+-- > import WaveFunctionCollapse+-- > Just example <- maps+-- > printMap example++printMap :: [ Intersect Tile ] -> IO ()+printMap (chunksOf 20 -> rows) = mapM_ printRow rows+  where printRow = putStrLn . foldMap (show . head . toList)++-- Use `cabal new-test examples` to run these tests and check for correct+-- solutions.++spec_wfc :: Spec+spec_wfc = it "generates a map" do+  maps >>= \result -> isJust result `shouldBe` True
+ holmes.cabal view
@@ -0,0 +1,114 @@+cabal-version:       2.4++author:             Tom Harding+build-type:         Simple+category:           Data+extra-source-files: README.md+homepage:           https://github.com/i-am-tom/holmes/+license-file:       LICENSE+license:            MIT+maintainer:         i.am.tom.harding@gmail.com+name:               holmes+description:        A reference library for constraint-solving with propagators and CDCL.+synopsis:           Tools and combinators for solving constraint problems.+version:            0.1.0.0++library+  exposed-modules: Control.Monad.Cell.Class+                 , Control.Monad.Holmes+                 , Control.Monad.Watson+                 , Data.Input.Config+                 , Data.JoinSemilattice.Defined+                 , Data.JoinSemilattice.Intersect+                 , Data.Propagator+                 , Data.Holmes++  other-modules: Control.Monad.MoriarT+               , Data.JoinSemilattice.Class.Abs+               , Data.JoinSemilattice.Class.Boolean+               , Data.JoinSemilattice.Class.Eq+               , Data.JoinSemilattice.Class.FlatMapping+               , Data.JoinSemilattice.Class.Fractional+               , Data.JoinSemilattice.Class.Integral+               , Data.JoinSemilattice.Class.Mapping+               , Data.JoinSemilattice.Class.Merge+               , Data.JoinSemilattice.Class.Ord+               , Data.JoinSemilattice.Class.Sum+               , Data.JoinSemilattice.Class.Zipping+               , Data.CDCL++  build-depends: base >=4.13 && < 4.14+               , hashable >= 1.3 && < 1.4+               , hedgehog >= 1.0 && < 1.1+               , logict >= 0.7 && < 0.8+               , mtl >= 2.2 && < 2.3+               , primitive >= 0.7 && < 0.8+               , transformers >= 0.5 && < 0.6+               , unordered-containers >= 0.2 && < 0.3++  ghc-options: -Wall -Wextra+  hs-source-dirs: src+  default-language: Haskell2010++--------------------------------------------------+-- EXAMPLE PROJECTS++test-suite examples+  type:     exitcode-stdio-1.0+  main-is:  Main.hs++  build-depends: base+               , hashable >= 1.3 && < 1.4+               , holmes+               , hspec >= 2.7 && < 2.8+               , split >= 0.2 && < 0.3+               , unordered-containers >= 0.2 && < 0.3+               , relude >= 0.6 && < 0.7+               , tasty >= 1.2 && < 1.3+               , tasty-discover+               , tasty-hspec++  other-modules: Futoshiki+               , WaveFunctionCollapse++  ghc-options: -Wall -Wextra -threaded+  hs-source-dirs: examples+  default-language: Haskell2010++--------------------------------------------------+-- UNIT TESTS++test-suite test+  type:     exitcode-stdio-1.0+  main-is:  Main.hs++  build-depends: base+               , containers >= 0.6 && < 0.7+               , hashable >= 1.3 && < 1.4+               , hedgehog >= 1.0 && < 1.1+               , holmes+               , primitive >= 0.7 && < 0.8+               , transformers >= 0.5 && < 0.6+               , tasty >= 1.2 && < 1.3+               , tasty-discover+               , tasty-hedgehog+               , tasty-hspec++  ghc-options: -Wall -Wextra -threaded+  hs-source-dirs: test+  build-tool-depends: markdown-unlit:markdown-unlit+  default-language: Haskell2010++--------------------------------------------------+-- LITERATE HASKELL README / HSPEC RUNNER++test-suite readme+  build-depends: base+               , hashable >= 1.3 && < 1.4+               , holmes+               , hspec >= 2.7 && < 2.8+  main-is:             README.lhs+  type:                exitcode-stdio-1.0+  default-language:    Haskell2010+  ghc-options:         -pgmL markdown-unlit -Wall+  build-tool-depends:  markdown-unlit:markdown-unlit
+ src/Control/Monad/Cell/Class.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Control.Monad.Cell.Class+Description : An interface for the primitive cell operations in a propagator network.+Copyright   : (c) Tom Harding, 2020+License     : MIT++/Are you just trying to use the library?/ If so, the contents of this module+shouldn't matter to you, so feel free to head straight over to the main+"Data.Holmes" module instead!++A __cell__ is the unit of storage in a propagator network. We can think of it+as "a description of a value", which is /refined/ over the course of a+computation.  Because we're functional programmers, the /described/ value is+__referentially transparent__ and __pure__: a cell's description must always be+of the /same/ value, and it can't change during the course of a computation.++Instead of __functions__ from one cell to another, we should try to think about+__relationships__ between cells. Addition, for example, could be seen as a+/function/ with two inputs, but it could also be seen as a /relationship/+between three values: the two components and their sum. The reason why this+helps us is that we might very well, for whatever reason, learn the sum+/before/ we learn both of the inputs. In these cases, it's useful to allow+information to flow in __multiple direcitons__. Why restrict ourselves to the+one-way flow of input-to-output when we can happily re-arrange equations on+paper?++Once we've built up our vocabulary for relationships, we just need a way to+lift them over cells. Intuitively, we should think of all relationships as+__invariants__. As cells' values are refined, these relationships are+constantly re-evaluated, and any new information can be spread around the+network to trigger, we hope, /more/ learnings that bring us closer to a+solution.++The 'Control.Monad.MoriarT.MoriarT' type provides a good reference+implementation for this interface, so head over there to see how we can use the+class to implement ideas like __provenance__ and __backtracking__.+-}+module Control.Monad.Cell.Class where++import Data.JoinSemilattice.Class.Merge (Merge)+import Data.Kind (Type)+import Data.Tuple (swap)+import Prelude++-- | The DSL for network construction primitives. The following interface+-- provides the building blocks upon which the rest of the library is+-- constructed.+--+-- If you are looking to implement the class yourself, you should note the lack+-- of functionality for ambiguity/searching. This is deliberate: for+-- backtracking search (as opposed to truth maintenance-based approaches), the+-- ability to create computation branches dynamically makes it much harder to+-- establish a reliable mechanism for tracking the effects of these choices.+--+-- For example: the approach used in the 'Control.Monad.MoriarT.MoriarT'+-- implementation is to separate the introduction of ambiguity into one+-- definite, explicit step, and all parameters must be declared ahead of time+-- so that they can be assigned indices. Other implementations should feel free+-- to take other approaches, but these will be implementation-specific.+class Monad m => MonadCell (m :: Type -> Type) where++  -- | The type of cells for this particular implementation. Typically, it's+  -- some sort of mutable reference ('Data.STRef.STRef', 'Data.IORef.IORef', or+  -- similar), but the implementation may attach further metadata to the+  -- individual cells.+  data Cell m :: Type -> Type++  -- | Mark the current computation as __failed__. For more advanced+  -- implementations that utilise backtracking and branching, this is an+  -- indication that we should begin a different branch of the search.+  -- Otherwise, the computation should simply fail without a result.+  discard :: m x++  -- | Create a new cell with the given value. Although this value's type has+  -- no constraints, it will be immutable unless it also implements 'Merge',+  -- which exists to enforce __monotonic__ updates.+  fill :: x -> m (Cell m x)++  -- | Create a callback that is fired whenever the value in a given cell is+  -- updated. Typically, this callback will involve potential writes to /other/+  -- cells based on the current value of the given cell. If such a write+  -- occurs, we say that we have __propagated__ information from the first cell+  -- to the next.+  watch :: Cell m x -> (x -> m ()) -> m ()++  -- | Execute a callback with the current value of a cell. Unlike 'watch',+  -- this will only fire once, and subsequent changes to the cell should /not/+  -- re-trigger this callback. This callback should therefore not be+  -- "registered" on any cell.+  with :: Cell m x -> (x -> m ()) -> m ()++  -- | Write an __update__ to a cell. This update should be merged into the+  -- current value using the '(Data.JoinSemilattice.Merge.<<-)' operation,+  -- which should behave the same way as '(<>)' for commutative and idempotent+  -- monoids. This therefore preserves the monotonic behaviour: updates can+  -- only __refine__ a value. The result of a 'write' must be /more refined/+  -- than the value before, with no exception.+  write :: Merge x => Cell m x -> x -> m ()++-- | In our regular Haskell coding, a binary function usually looks something+-- like @x -> y -> z@. When we view it as a /relationship/, we see that it's+-- actually a relationship between __three__ values: @x@, @y@, and @z@.+--+-- Given a function that takes everything we /currently/ know about these three+-- values, and returns three "updates" based on what each can learn from the+-- others, we can lift our three-way relationship (which, again, we can intuit+-- as a multi-directional binary function) into a network as a three-way+-- __propagator__. As an illustrative example, we might convert the '(+)'+-- function into something like:+--+-- @+-- addR :: (Int, Int, Int) -> (Int, Int, Int)+-- addR ( a, b, c ) = ( c - b, c - a, a + b )+-- @+--+-- In /practice/, these values must be 'Merge' values (unlike 'Int'), and so+-- any of them /could/ be 'mempty', or less-than-well-defined. This function+-- will take the three results as __updates__, and 'Merge' it into the cell,+-- so they will only make a difference /if/ we've learnt something new.+binary :: (MonadCell m, Merge x, Merge y, Merge z) => ((x, y, z) -> (x, y, z)) -> Cell m x -> Cell m y -> Cell m z -> m ()+binary f xs ys zs = do+  let update x y z = do+        let ( x', y', z' ) = f ( x, y, z )++        write xs x'+        write ys y'+        write zs z'++  watch xs \x -> with ys \y -> with zs \z -> update x y z+  watch ys \y -> with xs \x -> with zs \z -> update x y z+  watch zs \z -> with ys \y -> with xs \x -> update x y z++-- | Create a cell with "no information", which we represent as 'mempty'. When+-- we evaluate propagator computations written with the 'Data.Propagator.Prop'+-- abstraction, this function is used to create the result cells at each node+-- of the computation.+--+-- It's therefore important that your 'mempty' value is reasonably efficient to+-- compute, as larger computations may involve producing many of these values+-- as intermediaries. An 'Data.JoinSemilattice.Intersect.Intersect' of all+-- 'Int' values, for example, is going to make things run /very/ slowly.+make :: (MonadCell m, Monoid x) => m (Cell m x) +make = fill mempty++-- | This function takes two cells, and establishes propagators between them in+-- both directions. These propagators simply copy across any updates that+-- either cell receives, which means that the two cells end up holding exactly+-- the same value at all times.+--+-- After calling this function, the two cells are entirely indistinguishable,+-- as they will always be equivalent. We can intuit this function as "merging+-- two cells into one".+unify :: (MonadCell m, Merge x) => Cell m x -> Cell m x -> m ()+unify = unary swap++-- | A standard unary function goes from an input value to an output value.+-- However, in the world of propagators, it is more powerful to rethink this as+-- a /relationship/ between two values.+--+-- A good example is the 'negate' function. It doesn't matter whether you know+-- the input or the output; it's always possible to figure out the one you're+-- missing. Why, then, should our program only run in one direction? We could+-- rephrase 'negate' from 'Int -> Int' to something more like:+--+-- @+-- negateR :: ( Maybe Int, Maybe Int ) -> ( Maybe Int, Maybe Int )+-- negateR ( x, y ) = ( x <|> fmap negate y, y <|> fmap negate x )+-- @+--+-- Now, if we're missing /one/ of the values, we can calculate it using the+-- other! This, and the 'binary' function's description above, give us an idea+-- of how functions and relationships differ. The 'unary' function simply lifts+-- one of these expressions into a two-way propagator between two cells.+--+-- The 'Merge' constraint means that we can use 'mempty' to represent "knowing+-- nothing" rather than the 'Maybe' in the above example, which makes this+-- function a little more generalised.+unary :: (MonadCell m, Merge x, Merge y) => ((x, y) -> (x, y)) -> Cell m x -> Cell m y -> m ()+unary f xs ys = do+  let update x y = do+        let ( x', y' ) = f ( x, y )+        write xs x' *> write ys y'++  watch xs \x -> with ys \y -> update x y+  watch ys \y -> with xs \x -> update x y
+ src/Control/Monad/Holmes.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Control.Monad.Holmes+Description : A monad for constructing constraint-solving computations, and executing them inside 'IO'.+Copyright   : (c) Tom Harding, 2020+License     : MIT++'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 'Control.Monad.ST'. The internal code is shared between the two,+so results between the two are consistent.+-}+module Control.Monad.Holmes+  ( Holmes+  , MonadCell++  , unsafeRead+  , backward+  , forward+  , runAll+  , runOne+  , satisfying+  , shuffle+  , whenever+  ) where++import Control.Monad.Cell.Class (MonadCell (..))+import Control.Monad.IO.Class (MonadIO (..))+import qualified Control.Monad.Cell.Class as Cell+import Control.Monad.MoriarT (MoriarT (..))+import qualified Control.Monad.MoriarT as MoriarT+import Data.Coerce (coerce)+import Data.Input.Config (Config (..))+import Data.JoinSemilattice.Class.Eq (EqR)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.Kind (Type)+import Data.Propagator (Prop)+import qualified Data.Propagator as Prop+import qualified Hedgehog.Gen as Gen+import Type.Reflection (Typeable)++-- | A monad capable of solving constraint problems using 'IO' as the+-- evaluation type. Cells are represented using 'Data.IORef.IORef' references,+-- and __provenance__ is tracked to optimise backtracking search across+-- multiple branches.+newtype Holmes (x :: Type)+  = Holmes { runHolmes :: MoriarT IO x }+  deriving (Functor, Applicative, Monad)++instance MonadCell Holmes where+  newtype Cell Holmes x = Cell { unwrap :: Cell (MoriarT IO) x }++  discard = coerce (discard @(MoriarT IO))+  fill = fmap Cell . coerce (fill @(MoriarT IO))++  watch (Cell cell) = coerce (watch @(MoriarT IO) cell)+  with  (Cell cell) = coerce (with  @(MoriarT IO) cell)+  write (Cell cell) = coerce (write @(MoriarT IO) cell)++-- | 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+unsafeRead = coerce . MoriarT.unsafeRead . unwrap++-- | 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)+backward f y = MoriarT.runOne $ runHolmes do+  input  <- Cell.make+  output <- Prop.down (f (Prop.up input))++  Cell.write output y+  unsafeRead input++-- | 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)+forward f x = MoriarT.runOne $ runHolmes do+  input  <- Cell.make+  output <- Prop.down (f (Prop.up input))++  Cell.write input x+  unsafeRead output++-- | 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 ]+runAll = coerce (MoriarT.runAll @IO)++-- | 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)+runOne = coerce (MoriarT.runOne @IO)++-- | Given an input configuration, and a predicate on those input variables,+-- return the __first__ configuration that satisfies the predicate.+satisfying :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO (Maybe [ x ])+satisfying (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runOne (MoriarT.solve config f)++-- | 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+shuffle Config{..} = Config initial \x -> do+  let shuffle' = liftIO . Gen.sample . Gen.shuffle+  Holmes (runHolmes (refine x) >>= shuffle')++-- | 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 :: (EqR x b, Typeable x) => Config Holmes x -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> IO [[ x ]]+whenever (coerce -> config :: Config (MoriarT IO) x) f = MoriarT.runAll (MoriarT.solve config f)
+ src/Control/Monad/MoriarT.hs view
@@ -0,0 +1,204 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Data.Input.Config+Description : My horror at his crimes was lost in my admiration at his skill.+Copyright   : (c) Tom Harding, 2020+License     : MIT++'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+  ( MoriarT (..)++  , runAll+  , runOne+  , solve+  , unsafeRead+  ) where++import Control.Applicative (Alternative (..))+import Control.Monad (MonadPlus, guard)+import Control.Monad.Cell.Class (MonadCell (..))+import qualified Control.Monad.Cell.Class as Cell+import Control.Monad.IO.Class (MonadIO (..))+import Control.Monad.Logic (MonadLogic, LogicT (..))+import qualified Control.Monad.Logic as LogicT+import Control.Monad.Primitive (PrimMonad (..))+import Control.Monad.Reader.Class (MonadReader (..))+import qualified Control.Monad.Reader.Class as Reader+import Control.Monad.State.Class (MonadState (..))+import qualified Control.Monad.State.Class as State+import Control.Monad.Trans.Class (MonadTrans (..))+import Control.Monad.Trans.Reader (ReaderT (..))+import Control.Monad.Trans.State (StateT (..))+import qualified Control.Monad.Trans.State as StateT+import qualified Data.CDCL as CDCL+import Data.Foldable (asum)+import Data.Function ((&))+import Data.Functor ((<&>))+import Data.Input.Config (Config (..))+import Data.JoinSemilattice.Class.Boolean (BooleanR (..))+import Data.JoinSemilattice.Class.Eq (EqR (..))+import Data.JoinSemilattice.Class.Merge (Merge (..), Result (..))+import Data.Kind (Type)+import Data.Maybe (listToMaybe)+import Data.Monoid (Ap (..))+import Data.Primitive.MutVar (MutVar)+import qualified Data.Primitive.MutVar as MutVar+import Data.Propagator (Prop)+import qualified Data.Propagator as Prop+import Type.Reflection (Typeable)++-- | 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+      { unMoriarT :: ReaderT CDCL.Rule (LogicT (StateT CDCL.Group m)) x+      }+   deriving newtype+    ( Functor+    , Applicative+    , Alternative+    , Monad+    , MonadIO+    , MonadLogic+    , MonadPlus+    , MonadReader CDCL.Rule+    , MonadState CDCL.Group+    )+  deriving (Semigroup, Monoid)+    via (Ap (MoriarT m) x)++instance MonadTrans MoriarT where+  lift = MoriarT . lift . lift . lift++instance PrimMonad m => PrimMonad (MoriarT m) where+  type PrimState (MoriarT m) = PrimState m++  primitive = lift . primitive++instance PrimMonad m => MonadCell (MoriarT m) where+  newtype Cell (MoriarT m) (content :: Type)+    = Cell (MutVar (PrimState m) (CDCL.Rule, content, MoriarT m ()))++  discard = do+    context <- Reader.ask+    State.modify (CDCL.resolve context) -- Add this context to the "no goods" list.+    +    empty++  fill content = do+    context <- Reader.ask+    mutVar  <- MutVar.newMutVar (context, content, mempty)+    pure (Cell mutVar)++  watch cell@(Cell mutVar) propagator = do+    let next = with cell propagator++    before@(provenance, content, callbacks)+      <- MutVar.readMutVar mutVar++    MutVar.writeMutVar mutVar (provenance, content, callbacks *> next) *> next+      <|> MutVar.writeMutVar mutVar before *> empty -- Undo the action for the next branch.++  with (Cell mutVar) callback = do+    (provenance, content, _) <- MutVar.readMutVar mutVar+    Reader.local (<> provenance) (callback content)++  write (Cell mutVar) news = do+    context <- Reader.ask+    nogoods <- State.get++    before@(provenance, content, callbacks)+      <- MutVar.readMutVar mutVar++    let provenance' = context <> provenance+        content'    = content <<- news++    -- Skip this branch if the provenance is no good.+    guard (not (nogoods `CDCL.implies` provenance'))++    case content' of+      Changed update -> do+        MutVar.writeMutVar mutVar (provenance', update, callbacks) *> callbacks+          <|> MutVar.writeMutVar mutVar before *> empty++      Failure   -> Reader.local (<> context) discard+      Unchanged -> pure ()++-- | 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+unsafeRead (Cell mutVar) = do+  (_, content, _) <- MutVar.readMutVar mutVar++  pure content++-- | 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 ]+runAll+  = flip StateT.evalStateT mempty+  . LogicT.observeAllT+  . flip runReaderT mempty+  . unMoriarT++-- | Run a 'MoriarT' computation and return the /first/ valid branch's result.+runOne :: Monad m => MoriarT m x -> m (Maybe x)+runOne+  = fmap listToMaybe+  . flip StateT.evalStateT mempty+  . LogicT.observeManyT 1+  . flip runReaderT mempty+  . unMoriarT++-- | 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 x b, Merge x, Typeable x) => Config (MoriarT m) x -> (forall f. MonadCell f => [ Prop f x ] -> Prop f b) -> MoriarT m [ x ]+solve Config{..} predicate = do+  inputs <- traverse Cell.fill initial+  output <- Prop.down (predicate (map Prop.up inputs))+  Cell.write output trueR++  _ <- zip [0 ..] inputs & traverse \(major, cell) -> do+    current     <- unsafeRead cell+    refinements <- refine current++    input <- asum $ CDCL.index major refinements <&> \(rule, content) ->+      fmap Cell (MutVar.newMutVar (rule, content, mempty))++    Cell.unify cell input++  traverse unsafeRead inputs
+ src/Control/Monad/Watson.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Control.Monad.Watson+Description : A much purer soul than Holmes.+Copyright   : (c) Tom Harding, 2020+License     : MIT++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 'Control.Monad.Holmes.shuffle'.+However, this is often an acceptable compromise to avoid 'IO' entirely!+-}+module Control.Monad.Watson+  ( Watson+  , MonadCell (..)++  , unsafeRead+  , backward+  , forward+  , runAll+  , runOne+  , satisfying+  , whenever+  ) where++import Control.Monad.ST (ST, runST)+import Control.Monad.Cell.Class (MonadCell (..))+import qualified Control.Monad.Cell.Class as Cell+import Control.Monad.MoriarT (MoriarT (..))+import qualified Control.Monad.MoriarT as MoriarT+import Data.Coerce (coerce)+import Data.Input.Config (Config (..))+import Data.JoinSemilattice.Class.Eq (EqR)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.Kind (Type)+import Data.Propagator (Prop)+import qualified Data.Propagator as Prop+import Type.Reflection (Typeable)++-- | A monad capable of solving constraint problems using 'ST' as the+-- evaluation type. Cells are represented using 'Data.STRef.STRef' references,+-- and __provenance__ is tracked to optimise backtracking search across+-- multiple branches.+newtype Watson (h :: Type) (x :: Type)+  = Watson { runWatson :: MoriarT (ST h) x }+  deriving (Functor, Applicative, Monad)++instance MonadCell (Watson h) where+  newtype Cell (Watson h) x = Cell { unwrap :: Cell (MoriarT (ST h)) x }++  discard = coerce (discard @(MoriarT (ST h)))+  fill = fmap Cell . coerce (fill @(MoriarT (ST h)))++  watch (Cell cell) = coerce (watch @(MoriarT (ST h)) cell)+  with  (Cell cell) = coerce (with  @(MoriarT (ST h)) cell)+  write (Cell cell) = coerce (write @(MoriarT (ST h)) cell)++-- | 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+unsafeRead = coerce . MoriarT.unsafeRead . unwrap++-- | 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+backward f y = runST $ MoriarT.runOne $ runWatson do+  input  <- Cell.make+  output <- Prop.down (f (Prop.up input))++  Cell.write output y+  unsafeRead input++-- | 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+forward f x = runST $ MoriarT.runOne $ runWatson do+  input  <- Cell.make+  output <- Prop.down (f (Prop.up input))++  Cell.write input x+  unsafeRead output++-- | 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 ]+runAll xs = runST (MoriarT.runAll (runWatson xs))++-- | 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+runOne xs = runST (MoriarT.runOne (runWatson xs))++-- | Given an input configuration, and a predicate on those input variables,+-- return the __first__ configuration that satisfies the predicate.+satisfying :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> Maybe [ x ]+satisfying config f = runST (MoriarT.runOne (MoriarT.solve (coerce config) f))++-- | 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 :: (EqR x b, Typeable x) => (forall h. Config (Watson h) x) -> (forall m. MonadCell m => [ Prop m x ] -> Prop m b) -> [[ x ]]+whenever config f = runST (MoriarT.runAll (MoriarT.solve (coerce config) f))
+ src/Data/CDCL.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Data.CDCL+Description : Conflict-directed clause learning utilities.+Copyright   : (c) Tom Harding, 2020+License     : MIT++Each parameter in a computation has a unique identifier, which we refer to as+its 'Major' index. Each possible /value/ of a parameter is also assigned a+unique identifier, which we refer to as its 'Minor' index.++When a conflict arises in a computation, the cause of the conflict can be+identified by a set of @('Major', 'Minor')@ pairs. Then, every branch that+involves those parameters set to /those/ values can be eliminated, as we know+they'll eventually result in a conflict.*++This module takes the conflicts we encounter, and tries to generalise them to+eliminate as many redundant branches as possible.++* In practice, we don't do this exactly. Instead, we run every branch until we+spot a cell with a previously-identified "no good" provenance. This means we+don't have to enumerate all the possible branches up front, which could end up+costing us a lot of time for no reason.+-}+module Data.CDCL where++import Control.Monad (guard)+import Data.Bifunctor (first)+import Data.Function ((&))+import Data.Functor (($>))+import Data.Hashable (Hashable)+import Data.HashMap.Strict (HashMap)+import Data.Maybe (mapMaybe)+import qualified Data.HashMap.Strict as HashMap+import Data.HashSet (HashSet)+import qualified Data.HashSet as HashSet++-- | The index of a parameter in our computation.+type Major = Int++-- | The index of the chosen /value/ of a parameter in our computation.+type Minor = Int++-- | A set of value identifiers and their settings.+newtype Rule+  = Rule { toHashMap :: HashMap (Major, Minor) Bool }+  deriving newtype (Hashable, Monoid, Semigroup)+  deriving stock (Eq, Show)++-- | Generate unique rules for a set of possible values for a given parameter.+-- For example, if we assign parameter @#1@ possible values @[1 .. 4]@, this+-- function might generate something like:+--+-- @+-- [ ( -(1, 0) && -(1, 1), 1 )+-- , ( -(1, 0) &&  (1, 1), 2 )+-- , (  (1, 1) && -(1, 1), 3 )+-- , (  (1, 1) &&  (1, 1), 4 )+-- ]+-- @+index :: Major -> [ x ] -> [( Rule, x )]+index major items = map (first rulify) (go items)+  where+    rulify = Rule . HashMap.fromList . zipWith zipper [0 ..]+    zipper minor value = ((major, minor), value)++    go :: [ x ] -> [( [Bool], x )]+    go = \case+      [ ] -> []+      [x] -> pure (mempty, x)++      xs@(length -> count) -> do+        let (go -> true, go -> false) = splitAt (count `div` 2) xs+        map (first (True :)) true <> map (first (False :)) false++-- | List all the @(Major, Minor)@ pairs in a 'Rule'.+variables :: Rule -> [(Major, Minor)]+variables = HashMap.keys . toHashMap++-- | Toggle the boolean switch of a @(Major, Minor)@ pair.+invert :: (Major, Minor) -> Rule -> Rule+invert key = Rule . HashMap.update (Just . not) key . toHashMap++-- | Remove a @(Major, Minor)@ pair from a 'Rule'.+remove :: (Major, Minor) -> Rule -> Rule+remove key = Rule . HashMap.delete key . toHashMap++-- | A set of rules. We use this to represent our global list of "no good"+-- configurations. If any cell's provenance ever contains one of the rules in+-- our global set, we know this computation will eventually end in failure.+newtype Group+  = Group { toSet :: HashSet Rule }+  deriving newtype (Monoid)++instance Semigroup Group where+  Group these <> Group those+    = foldr resolve mempty (these <> those)++-- | If a group implies @(A && B)@ /and/ @(A && -B)@ then the @B@ seems to be+-- irrelevant, so we can refine the 'Rule' to @A@. This hopefully means we can+-- eliminate /more/ branches, and get to an answer faster!+refinements :: Rule -> Group -> [Rule]+refinements rule group = variables rule & mapMaybe \key ->+  guard (group `implies` invert key rule) $> remove key rule++-- | Does any 'Rule' in this 'Group' subsume the given 'Rule'?+implies :: Group -> Rule -> Bool+implies (Group group) candidate = any (`subsumes` candidate) group++-- | If @x@ 'subsumes' @y@, then the set of switches in @x@ is a strict+-- __subset__ of the switches in @y@. In other words, the @x@ 'Rule' will match+-- /everything/ that @y@ will.+subsumes :: Rule -> Rule -> Bool+subsumes (Rule these) (Rule those) = HashMap.foldrWithKey check True these+  where check key value acc = HashMap.lookup key those == Just value && acc++-- | Add a new 'Rule' to a 'Group'. Attempt to calculate any 'refinements' of+-- the rule, and generalise the 'Group' as far as possible.+resolve :: Rule -> Group -> Group+resolve rule group | group `implies` rule = group+resolve rule@(Rule config) group@(Group rules)+  = case refinements rule group of+      [] -> Group case HashMap.toList config of+        [ (key, value) ] -> do -- Unit propagation+          HashSet.insert rule $ rules & HashSet.map \(Rule current) -> do+            if HashMap.lookup key current /= Just value+              then Rule (HashMap.delete key current)+              else rule++        _ -> rules & HashSet.filter (not . (rule `subsumes`))+                   & HashSet.insert rule++      better -> foldr resolve group better
+ src/Data/Holmes.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Data.Holmes+Description : The public API for the @holmes@ library.+Copyright   : (c) Tom Harding, 2020+License     : MIT++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+  ( Holmes+  , MonadCell++  , forward+  , backward+  , satisfying+  , shuffle+  , whenever++  , Config (..)+  , Input (..)+  , permute++  , AbsR (..)+  , BooleanR (..)+  , EqR (..), neR+  , FlatMapping (..)+  , FractionalR (..)+  , IntegralR (..)+  , Mapping (..)+  , OrdR (..), ltR, gtR, gteR+  , SumR (..), negateR, subR+  , Zipping (..)++  , Merge (..)+  , Result (..)++  , Defined (..)+  , Intersect (..)+  , using++  , Prop++  , (Prop..$), (Prop..>>=), Prop.zipWith'++  , (Prop..&&), Prop.all', Prop.allWithIndex', Prop.and'+  , (Prop..||), Prop.any', Prop.anyWithIndex', Prop.or'++  , Prop.not'+  , Prop.false, Prop.true++  , (Prop..*), (Prop../)+  , (Prop..+), (Prop..-)+  , (Prop..<), (Prop..<=), (Prop..>), (Prop..>=)+  , (Prop..==), (Prop../=), Prop.distinct+  , (Prop..%.), (Prop..*.), (Prop../.)++  , Prop.abs'+  , Prop.negate'+  , Prop.recip'+  ) where++import Control.Monad.Cell.Class (MonadCell)+import Control.Monad.Holmes (Holmes, satisfying, shuffle, whenever)+import Control.Monad.Watson (forward, backward)+import Data.Input.Config (Config (..), Input (..), permute)+import Data.JoinSemilattice.Class.Abs (AbsR (..))+import Data.JoinSemilattice.Class.Boolean (BooleanR (..))+import Data.JoinSemilattice.Class.Eq (EqR (..), neR)+import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..))+import Data.JoinSemilattice.Class.Fractional (FractionalR (..))+import Data.JoinSemilattice.Class.Integral (IntegralR (..))+import Data.JoinSemilattice.Class.Mapping (Mapping (..))+import Data.JoinSemilattice.Class.Merge (Merge (..), Result (..))+import Data.JoinSemilattice.Class.Ord (OrdR (..), ltR, gtR, gteR)+import Data.JoinSemilattice.Class.Sum (SumR (..), negateR, subR)+import Data.JoinSemilattice.Class.Zipping (Zipping (..))+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..), using)+import Data.Propagator (Prop)+import qualified Data.Propagator as Prop
+ src/Data/Input/Config.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Data.Input.Config+Description : Configuration for input parameters.+Copyright   : (c) Tom Harding, 2020+License     : MIT++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+'Data.JoinSemilattice.Defined.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 where++import Control.Applicative (liftA2)+import Data.HashSet (HashSet)+import qualified Data.HashSet as HashSet+import Data.Hashable (Hashable)+import Data.Kind (Type)++-- | 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 'Data.JoinSemilattice.Intersect.singleton' values of+-- every remaining possibility.+data Config (m :: Type -> Type) (x :: Type)+  = Config { initial :: [ x ], refine  :: 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 Raw x :: Type++  -- | Generate @m@ variables who are one of @n@ values. @81 `from` [1 .. 9]@,+  -- @5 `from` [ True, False ]@, and so on.+  from :: 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 ])+permute Config{..} = fmap HashSet.fromList (go initial)+  where go [      ] = pure [ [] ]+        go (i : is) = liftA2 (liftA2 (:)) (refine i) (go is)
+ src/Data/JoinSemilattice/Class/Abs.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.Abs+Description : Relationships between values and their absolutes.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Abs where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Defined (Defined)+import Data.JoinSemilattice.Intersect (Intersect)+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Type)++-- | 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) where++  -- | Given a value and its absolute, try to learn something in either+  -- direction.+  absR :: ( x, x ) -> ( x, x )++  -- | By default, this relationship is one-way.+  default absR :: Num x => ( x, x ) -> ( x, x )+  absR ( x, _ ) = ( mempty, abs x )++instance (Eq x, Num x) => AbsR (Defined x)++instance (Bounded x, Enum x, Eq x, Hashable x, Num x)+    => AbsR (Intersect x) where+  absR ( x, y ) = ( Intersect.union y (negate y), abs x )
+ src/Data/JoinSemilattice/Class/Boolean.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiWayIf #-}++{-|+Module      : Data.JoinSemilattice.Class.Boolean+Description : Relationships between boolean variables.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Boolean where++import Control.Applicative (liftA2)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..))+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Type)++-- | 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 x => BooleanR (x :: Type) where+  -- | An overloaded 'False' value.+  falseR :: x++  -- | An overloaded 'True' value.+  trueR :: x++  -- | A relationship between a boolean value and its opposite.+  notR :: ( x, x ) -> ( x, x )++  -- | A relationship between two boolean values and their conjunction.+  andR :: ( x, x, x ) -> ( x, x, x )++  -- | A relationship between two boolean values and their disjunction.+  orR :: ( x, x, x ) -> ( x, x, x )++instance BooleanR (Defined Bool) where+  falseR = Exactly False+  trueR  = Exactly True++  notR (x, y) = ( fmap not y, fmap not x )++  andR (x, y, z)+    = ( if | z == trueR                -> trueR+           | z == falseR && y == trueR -> falseR+           | otherwise                 -> mempty++      , if | z == trueR                -> trueR+           | z == falseR && x == trueR -> falseR+           | otherwise                 -> mempty++      , liftA2 (&&) x y+      )++  orR (x, y, z)+    = ( if | z == falseR               -> falseR+           | z == trueR && y == falseR -> trueR+           | otherwise                 -> mempty++      , if | z == falseR               -> falseR+           | z == trueR && x == falseR -> trueR+           | otherwise                 -> mempty++      , liftA2 (||) x y+      )++instance BooleanR (Intersect Bool) where+  falseR = Intersect.singleton False+  trueR  = Intersect.singleton True++  notR (x, y) = ( Intersect.map not y, Intersect.map not x )++  andR (x, y, z)+    = ( if | z == trueR                -> trueR+           | z == falseR && y == trueR -> falseR+           | otherwise                 -> mempty++      , if | z == trueR                -> trueR+           | z == falseR && x == trueR -> falseR+           | otherwise                 -> mempty++      , Intersect.lift2 (&&) x y+      )++  orR (x, y, z)+    = ( if | z == falseR               -> falseR+           | z == trueR && y == falseR -> trueR+           | otherwise                 -> mempty++      , if | z == falseR               -> falseR+           | z == trueR && x == falseR -> trueR+           | otherwise                 -> mempty++      , Intersect.lift2 (||) x y+      )
+ src/Data/JoinSemilattice/Class/Eq.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiWayIf #-}++{-|+Module      : Data.JoinSemilattice.Class.Eq+Description : Equality relationships.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Eq where++import Control.Applicative (liftA2)+import Data.Hashable (Hashable)+import Data.JoinSemilattice.Class.Boolean (BooleanR (..))+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..))+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Type)++-- | 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+-- 'Control.Monad.Cell.Class.unify' the two input cells, as we know that their+-- values will always be the same.+class (BooleanR b, Merge x) => EqR (x :: Type) (b :: Type) | x -> b where+  eqR :: ( x, x, b ) -> ( x, x, b )++-- | A relationship between two variables and the result of a not-equals+-- comparison between them.+neR :: EqR x b => ( x, x, b ) -> ( x, x, b )+neR ( x, y, z )+  = let ( notZ', _ ) = notR ( mempty, z )+        ( x', y', notZR ) = eqR ( x, y, notZ' )+        ( _, z' ) = notR ( notZR, mempty )++    in ( x', y', z' )++instance Eq x => EqR (Defined x) (Defined Bool) where+  eqR ( x, y, z )+    = ( if z == trueR then y else mempty+      , if z == trueR then x else mempty+      , liftA2 (==) x y+      )++instance (Bounded x, Enum x, Eq x, Hashable x)+    => EqR (Intersect x) (Intersect Bool) where+  eqR ( x, y, z )+    = ( if | z == trueR                           -> y+           | z == falseR && Intersect.size y == 1 -> Intersect.except y+           | otherwise                            -> mempty++      , if | z == trueR                           -> x+           | z == falseR && Intersect.size x == 1 -> Intersect.except x+           | otherwise                            -> mempty++      , Intersect.lift2 (==) x y+      )
+ src/Data/JoinSemilattice/Class/FlatMapping.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.FlatMapping+Description : Refine parameters using their raw values.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.FlatMapping where++import Data.JoinSemilattice.Class.Zipping (Zipping)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..), Intersectable)+import Data.Kind (Constraint, Type)+import Prelude hiding (unzip)++-- | 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 `(Data.Propagator..>>=)`.+--+-- 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 where+  flatMapR :: (c x, c y) => ((x, f y) -> (x, f y)) -> ((f x, f y) -> (f x, f y))++instance FlatMapping Defined Eq where+  flatMapR f ( xs, _ )+    = ( mempty -- Unless you have 'Monoid x'+      , case xs of Exactly x -> let ( _, ys' ) = f (x, mempty) in ys'+                   _         -> mempty+      )++instance FlatMapping Intersect Intersectable where+  flatMapR f ( Intersect xs, _ )+    = ( mempty -- Unless you have 'Monoid x'+        +        -- Take the union of all generated 'Intersect' values.+      , Intersect (foldMap (\x -> let (_, Intersect ys') = f (x, mempty) in ys') xs)+      )
+ src/Data/JoinSemilattice/Class/Fractional.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.Fractional+Description : Relationships between values and their (floating/fractional) product.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Fractional where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Defined (Defined)+import Data.JoinSemilattice.Intersect (Intersect)+import Data.JoinSemilattice.Class.Sum (SumR)+import Data.Kind (Type)++-- | Reversible (fractional or floating-point) multiplication as a three-value+-- relationship between two values and their product.+class SumR x => FractionalR (x :: Type) where+  multiplyR :: ( x, x, x ) -> ( x, x, x )++  default multiplyR :: Fractional x => ( x, x, x ) -> ( x, x, x )+  multiplyR ( x, y, z ) = ( z / y, z / x, x * y )++-- | A three-way division relationships implemented as a flipped multiplication+-- relationship.+divideR :: FractionalR x => ( x, x, x ) -> ( x, x, x )+divideR ( x, y, z ) = let ( z', y', x' ) = multiplyR ( z, y, x ) in ( x', y', z' )++-- | A two-way relationship between a value and its reciprocal, implemented+-- with a multiplication relationship in which the third value is fixed to be+-- @1@.+recipR :: (FractionalR x, Num x) => ( x, x ) -> ( x, x )+recipR ( x, y ) = let ( x', y', _ ) = multiplyR ( x, y, 1 ) in ( x', y' )++instance (Eq x, Fractional x) => FractionalR (Defined x)++instance (Bounded x, Enum x, Eq x, Fractional x, Hashable x)+  => FractionalR (Intersect x)
+ src/Data/JoinSemilattice/Class/Integral.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.Integral+Description : Relationships between values and their (integral) division results.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Integral where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect)+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.JoinSemilattice.Class.Sum (SumR)+import Data.Kind (Type)++-- | 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) where+  divModR :: ( x, x, x, x ) -> ( x, x, x, x )++-- | Integral multiplication implemented as a 'divModR' relationship in which+-- the remainder is fixed to be @0@.+timesR :: (IntegralR x, Num x) => ( x, x, x ) -> ( x, x, x )+timesR ( x, y, z ) = let ( z', y', x', _ ) = divModR ( z, y, x, 0 ) in ( x', y', z' )++-- | Integal division as a three-value relationship.+divR :: IntegralR x => ( x, x, x ) -> ( x, x, x )+divR ( x, y, z ) = let ( x', y', z', _ ) = divModR ( x, y, z, mempty ) in ( x', y', z' )++-- | Modulo operator implemented as a three-value relationship.+modR :: IntegralR x => ( x, x, x ) -> ( x, x, x )+modR ( x, y, z ) = let ( x', y', _, z' ) = divModR ( x, y, mempty, z ) in ( x', y', z' )++instance (Eq x, Integral x) => IntegralR (Defined x) where+  divModR ( x, y, z, w )+    = (  y * z + w+      , (x - w) `div` z+      , (x - w) `div` y+      ,  x - (y * z)+      )++instance (Bounded x, Enum x, Eq x, Hashable x, Integral x)+    => IntegralR (Intersect x) where+  divModR ( x, y, z, w )+    = ( y * z + w+      , Intersect.lift2 div (x - w) z+      , Intersect.lift2 div (x - w) y+      , x - (y * z)+      )
+ src/Data/JoinSemilattice/Class/Mapping.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Data.JoinSemilattice.Class.Mapping+Description : Lift "regular functions" over parameter types.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Mapping where++import Control.Applicative (liftA2)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Defined (Defined)+import Data.JoinSemilattice.Intersect (Intersect, Intersectable)+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Constraint, Type)+import Data.List.NonEmpty (unzip)+import Prelude hiding (unzip)++-- | 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 where+  mapR :: (c x, c y) => ((x, y) -> (x, y)) -> ((f x, f y) -> (f x, f y))++  default mapR :: Applicative f => ((x, y) -> (x, y)) -> ((f x, f y) -> (f x, f y))+  mapR f (xs, ys) = unzip (liftA2 (curry f) xs ys)++instance Mapping Defined Eq++instance Mapping Intersect Intersectable where+  mapR f (Intersect.toList -> xs, Intersect.toList -> ys) = do+    let ( xs', ys' ) = unzip (liftA2 (curry f) xs ys)++    ( Intersect.fromList xs', Intersect.fromList ys' )
+ src/Data/JoinSemilattice/Class/Merge.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Control.Monad.Watson+Description : Performant join semilattice-based knowledge-merging.+Copyright   : (c) Tom Harding, 2020+License     : MIT++= Join semilattices++A __join semilattice__ is a 'Monoid' with two extra laws:++prop> x <> y === y <> x -- Commutativity+prop> x <> x === x      -- Idempotence++Within every cell, we store a join semilattice, and all writes are added into+the cell using '(<>)'. Adding the above laws introduces enough structure to+ensure that all functions between cells are __monotonic__. In other words, if+we assume that @x@ "implies" @y@ if @x <> y === x@, the value /after/ a write+will always imply the value /before/.++We can therefore see each value as "moving up" some chain towards the final+answer. More interestingly, the final answer implies /every value/ that has+ever been in the cell. I like to use the intuition of __knowledge__ for join+semilattices:++- 'mempty' represents "knowing nothing" about a value.+- '(<>)' is a function that /combines/ two knowledge bases into one.+- @x@ implies @y@ if @y@ tells us nothing that @x@ doesn't already tell us.++When we think about pure functions and referential transparency, we tend to say+that "the value of a variable never changes". In the language of propagator+networks, we can tweak this a little to say, "the value /being described/ by a+cell's knowledge never changes".++= Merging++In a naïve system, we could simply define the join semilattice class as+follows:++@+class Monoid x => JoinSemilattice (x :: Type)+@++(It would need no methods as it's really just some extra assertions on '(<>)').+This would be fine, but there are a few shortcomings when we come to implement+our 'Control.Monad.Cell.Class.write' operation:++- We don't want to trigger propagators if we don't need to, so we'd want to+  check whether the result is different to the value that was there before.+  We'd most likely do this with a standard '(==)' comparison, but this could be+  quite expensive!++- We don't have a notion of "failure state", so we don't know when we can+  discard branches. If we don't know when to /discard/ branches, we either have+  to implement assertions elsewhere (which puts more work onto the user) /or/+  discard nothing (which makes many problems intractably slow to compute).++The cleanest solution I could find to this is expressed in the 'Result' type,+which allows the type simultaneously to compute the merge result /and/ the+resulting effect on the cell or network. In theory, it should respect the+'(<>)' operation's behaviour, but with the added 'Failure' state. Not every+type /needs/ to have a 'Failure' state, but it means that the user needn't+write their own assertion boilerplate for the usual suspects (such as the+'Data.JoinSemilattice.Defined.Conflict' constructor).++-}+module Data.JoinSemilattice.Class.Merge where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..))+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Type)++-- | The result of merging some news into a cell's current knowledge.+data Result (x :: Type)+  = Unchanged -- ^ We've learnt nothing; no updates elsewhere are needed.+  | Changed x -- ^ We've learnt something; fire the propagators!+  | Failure   -- ^ We've hit a failure state; discard the computation.+  deriving stock (Eq, Functor, Ord, Show)++instance Semigroup x => Semigroup (Result x) where+  Changed x <> Changed y = Changed (x <> y)++  Failure <> _ = Failure+  _ <> Failure = Failure++  Unchanged <> y = y+  x <> Unchanged = x++instance Semigroup x => Monoid (Result x) where+  mempty = Unchanged++-- | 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, Eq 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+
+ src/Data/JoinSemilattice/Class/Ord.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiWayIf #-}++{-|+Module      : Data.JoinSemilattice.Class.Ord+Description : Relationships between values and their comparison results.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Ord where++import Control.Applicative (liftA2)+import Data.Hashable (Hashable)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect (..))+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.JoinSemilattice.Class.Boolean (BooleanR (..))+import Data.JoinSemilattice.Class.Eq (EqR)+import Data.Kind (Type)++-- | Comparison relationships between two values and their comparison result.+class EqR x b => OrdR (x :: Type) (b :: Type) | x -> b where++  -- | A relationship between two values and whether the left is less than or+  -- equal to the right.+  lteR :: ( x, x, b ) -> ( x, x, b )++-- | Comparison between two values and their '(>)' result.+gtR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+gtR ( x, y, z ) = let ( y', x', z' ) = ltR ( y, x, z ) in ( x', y', z' )++-- | Comparison between two values and their '(>=)' result.+gteR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+gteR ( x, y, z ) = let ( y', x', z' ) = lteR ( y, x, z ) in ( x', y', z' )++-- | Comparison between two values and their '(<)' result.+ltR :: OrdR x b => ( x, x, b ) -> ( x, x, b )+ltR ( x, y, z )+  = let ( notZ', _ ) = notR ( mempty, z )+        ( x', y', notZR ) = gteR ( x, y, notZ' )+        ( _, z' ) = notR ( notZR, mempty )++    in ( x', y', z' )++instance Ord x => OrdR (Defined x) (Defined Bool) where+  lteR ( x, y, _ ) = ( mempty, mempty, liftA2 (<=) x y )++instance (Bounded x, Enum x, Hashable x, Ord x)+    => OrdR (Intersect x) (Intersect Bool) where+  lteR ( x, y, z )+    = ( if | z == trueR  -> Intersect.filter (<= maximum y) x+           | z == falseR -> Intersect.filter ( > minimum y) x+           | otherwise   -> mempty++      , if | z == trueR  -> Intersect.filter (>= minimum x) y+           | z == falseR -> Intersect.filter ( < maximum x) y+           | otherwise   -> mempty++      , Intersect.lift2 (<=) x y+      )
+ src/Data/JoinSemilattice/Class/Sum.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE KindSignatures #-}++{-|+Module      : Data.JoinSemilattice.Class.Sum+Description : Relationships between values and their sums.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Sum where++import Data.Hashable (Hashable)+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Defined (Defined (..))+import Data.JoinSemilattice.Intersect (Intersect)+import Data.Kind (Type)++-- | A relationship between two values and their sum.+class Merge x => SumR (x :: Type) where+  addR :: ( x, x, x ) -> ( x, x, x )++  default addR :: Num x => ( x, x, x ) -> ( x, x, x )+  addR ( x, y, z ) = ( z - y, z - x, x + y )++-- | A relationship between two values and their difference.+subR :: SumR x => ( x, x, x ) -> ( x, x, x )+subR ( x, y, z ) = let ( z', y', x' ) = addR ( z, y, x ) in ( x', y', z' )++-- | A relationship between a value and its negation.+negateR :: (Num x, SumR x) => ( x, x ) -> ( x, x )+negateR ( x, y ) = let ( x', y', _ ) = addR ( x, y, 0 ) in ( x', y' )++instance (Eq x, Num x) => SumR (Defined x)+instance (Bounded x, Enum x, Eq x, Hashable x, Num x) => SumR (Intersect x)
+ src/Data/JoinSemilattice/Class/Zipping.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Data.JoinSemilattice.Class.Zipping+Description : Computing knowledge from multiple parameters.+Copyright   : (c) Tom Harding, 2020+License     : MIT+-}+module Data.JoinSemilattice.Class.Zipping (Zipping (..)) where++import Control.Applicative (liftA3)+import Data.Function ((&))+import Data.JoinSemilattice.Class.Mapping (Mapping)+import Data.JoinSemilattice.Defined (Defined)+import Data.JoinSemilattice.Intersect (Intersect, Intersectable)+import qualified Data.JoinSemilattice.Intersect as Intersect+import Data.Kind (Constraint, Type)+import Prelude hiding (unzip3)++-- | 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 where+  zipWithR :: (c x, c y, c z) => ((x, y, z) -> (x, y, z)) -> ((f x, f y, f z) -> (f x, f y, f z))++  default zipWithR :: Applicative f => ((x, y, z) -> (x, y, z)) -> ((f x, f y, f z) -> (f x, f y, f z))+  zipWithR f (xs, ys, zs) = unzip3 (liftA3 (\x y z -> f (x, y, z)) xs ys zs)++instance Zipping Defined Eq++instance Zipping Intersect Intersectable where+  zipWithR f (Intersect.toList -> xs, Intersect.toList -> ys, Intersect.toList -> zs) = do+    let ( xs', ys', zs' ) = unzip3 (liftA3 (\x y z -> f (x, y, z)) xs ys zs)+    ( Intersect.fromList xs', Intersect.fromList ys', Intersect.fromList zs' )++unzip3 :: Functor f => f (x, y, z) -> (f x, f y, f z)+unzip3 xyz+  = ( xyz & fmap \(x, _, _) -> x+    , xyz & fmap \(_, y, _) -> y+    , xyz & fmap \(_, _, z) -> z+    )
+ src/Data/JoinSemilattice/Defined.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeFamilies #-}++{-|+Module      : Data.JoinSemilattice.Defined+Description : Values with differing levels of "definedness".+Copyright   : (c) Tom Harding, 2020+License     : MIT++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 where++import Control.Applicative (liftA2)+import Data.Hashable (Hashable)+import Data.Input.Config (Config (..), Input (..))+import Data.Kind (Type)+import Data.List.NonEmpty (unzip)+import Data.Monoid (Ap (..))+import GHC.Generics (Generic)+import Prelude hiding (unzip)++-- | Defines simple "levels of knowledge" about a value.+data Defined (x :: Type)+  = Unknown   -- ^ Nothing has told me what this value is.+  | Exactly x -- ^ Everyone who has told me this value agrees.+  | Conflict  -- ^ Two sources disagree on what this value should be.+  deriving stock (Eq, Ord, Show, Functor, Generic)+  deriving anyclass (Hashable)+  deriving (Bounded, Num) via (Ap Defined x)++instance Enum content => Enum (Defined content) where+  fromEnum = \case+    Exactly this -> fromEnum this+    _            -> error "fromEnum is undefined for non-exact values."++  toEnum = pure . toEnum++instance Applicative Defined where+  pure = Exactly++  Conflict <*> _ = Conflict+  _ <*> Conflict = Conflict++  Unknown <*> _ = Unknown+  _ <*> Unknown = Unknown++  Exactly f <*> Exactly x+    = Exactly (f x)++instance Eq content => Semigroup (Defined content) where+  Conflict <> _ = Conflict+  _ <> Conflict = Conflict++  this <> Unknown = this+  Unknown <> that = that++  Exactly this <> Exactly that+    | this == that = Exactly this+    | otherwise    = Conflict++instance Eq content => Monoid (Defined content) where+  mempty = Unknown++instance Real content => Real (Defined content) where+  toRational = \case+    Exactly this -> toRational this+    _            -> error "toRational is undefined for non-exact values."++instance Integral content => Integral (Defined content) where+  quotRem this that = unzip (liftA2 quotRem this that)++  toInteger = \case+    Exactly this -> toInteger this+    _            -> error "toInteger is undefined for non-exact values."++instance Fractional x => Fractional (Defined x) where+  (/) = liftA2 (/)++  fromRational = pure . fromRational+  recip        = fmap recip++instance Input (Defined content) where+  type Raw (Defined content) = content++  from count options = Config (replicate count Unknown) do+    pure . \case+      Unknown -> map Exactly options+      decided -> [ decided ]
+ src/Data/JoinSemilattice/Intersect.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralisedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++{-|+Module      : Data.JoinSemilattice.Intersect+Description : Solving problems by reducing lists of candidates.+Copyright   : (c) Tom Harding, 2020+License     : MIT++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 where++import Control.Applicative (liftA2)+import Data.Coerce (coerce)+import Data.HashSet (HashSet)+import qualified Data.HashSet as HashSet+import Data.Hashable (Hashable)+import Data.Input.Config (Config (..), Input (..))+import Data.Kind (Type)+import Prelude hiding (filter, map, unzip)++-- | A set type with intersection as the '(<>)' operation.+newtype Intersect (x :: Type)+  = Intersect { toHashSet :: HashSet x }+  deriving stock (Eq, Ord, Show, Foldable)+  deriving newtype (Hashable)++class (Bounded content, Enum content, Eq content, Hashable content)+  => Intersectable content++instance (Bounded content, Enum content, Eq content, Hashable content)+  => Intersectable content++instance (Eq content, Hashable content) => Semigroup (Intersect content) where+  (<>) = coerce HashSet.intersection++instance Intersectable content => Monoid (Intersect content) where+  mempty = fromList [ minBound .. maxBound ]++lift2+  :: ( Intersectable this+     , Intersectable that+     , Intersectable result+     )+  => (this -> that -> result)+  -> Intersect this+  -> Intersect that+  -> Intersect result++lift2 f these those = fromList do+  liftA2 f (toList these) (toList those)++instance (Intersectable content, Num content)+    => Num (Intersect content) where+  (+) = lift2 (+)+  (*) = lift2 (*)+  (-) = lift2 (-)++  abs         = map abs+  fromInteger = singleton . fromInteger+  negate      = map negate+  signum      = map signum++instance (Intersectable x, Fractional x) => Fractional (Intersect x) where+  (/) = lift2 (/)++  fromRational = singleton . fromRational+  recip = map recip++-- | Create an 'Intersect' from a list of candidates.+fromList :: (Eq x, Hashable x) => [ x ] -> Intersect x+fromList = coerce HashSet.fromList++-- | Return a list of candidates stored within an 'Intersect'.+toList :: (Bounded x, Enum x, Eq x) => Intersect x -> [ x ]+toList = coerce HashSet.toList++-- | Run an action /only if/ a single candidate remains.+decided :: (Applicative m, Intersectable x) => (x -> m ()) -> Intersect x -> m ()+decided f = \case+  (toList -> [ x ]) -> f x+  _                 -> pure ()++-- | Delete a candidate from an 'Intersect'.+delete :: Intersectable x => x -> Intersect x -> Intersect x+delete = coerce HashSet.delete++-- | 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+except = foldr delete mempty++-- | Filter an 'Intersect' with a predicate.+filter :: (x -> Bool) -> Intersect x -> Intersect x+filter = coerce HashSet.filter++-- | Map over an 'Intersect' with a given function.+map :: (Eq y, Hashable y) => (x -> y) -> Intersect x -> Intersect y+map = coerce HashSet.map++-- | Create a singleton 'Intersect'.+singleton :: Hashable x => x -> Intersect x+singleton = coerce HashSet.singleton++-- | Count the candidates in an 'Intersect'.+size :: Intersectable x => Intersect x -> Int+size = coerce HashSet.size++-- | Merge two 'Intersect' values with set __union__.+union :: Intersectable x => Intersect x -> Intersect x -> Intersect x +union = coerce ((<>) @(HashSet _))++instance Intersectable x => Input (Intersect x) where+  type Raw (Intersect x) = x++  from count = using . replicate count . fromList++-- | 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)+using xs = Config xs (pure . fmap singleton . toList)
+ src/Data/Propagator.hs view
@@ -0,0 +1,412 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}++{-|+Module      : Data.Propagator+Description : The high-level propagator abstraction.+Copyright   : (c) Tom Harding, 2020+License     : MIT++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+  ( Prop, up, down, lift, over, lift2, unary, binary++  , (.&&), all', allWithIndex', and'+  , (.||), any', anyWithIndex', or'+  , false, not', true++  , (.==), (./=), distinct++  , (.>), (.>=), (.<), (.<=)++  , (.+), (.-), negate'+  , (.*.), (./.), (.%.)+  , (.*), (./), recip'+  , abs'++  , (.$)+  , zipWith'+  , (.>>=)+  ) where++import Control.Monad.Cell.Class (MonadCell (..))+import qualified Control.Monad.Cell.Class as Cell+import Data.JoinSemilattice.Class.Abs (AbsR (..))+import Data.JoinSemilattice.Class.Boolean (BooleanR (..))+import Data.JoinSemilattice.Class.Eq (EqR (..), neR)+import Data.JoinSemilattice.Class.FlatMapping (FlatMapping (..))+import Data.JoinSemilattice.Class.Fractional (FractionalR (..), divideR, multiplyR, recipR)+import Data.JoinSemilattice.Class.Integral (IntegralR (..), divR, modR, timesR)+import Data.JoinSemilattice.Class.Mapping (Mapping (..))+import Data.JoinSemilattice.Class.Merge (Merge)+import Data.JoinSemilattice.Class.Ord (OrdR (..), gtR, gteR, ltR)+import Data.JoinSemilattice.Class.Sum (SumR (..), negateR, subR)+import Data.JoinSemilattice.Class.Zipping (Zipping (..))+import Data.Kind (Type)++-- | 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) where++  Nullary+    :: m (Cell m x)+    -> Prop m x++  Unary+    :: Merge x+    => (forall f. MonadCell f => Cell f x -> Cell f y -> f ())+    -> Prop m x+    -> Prop m y++  Binary+    :: ( Merge x+       , Merge y+       )+    => (forall f. MonadCell f => Cell f x -> Cell f y -> Cell f z -> f ())+    -> Prop m x+    -> Prop m y+    -> Prop m z++instance (AbsR x, SumR x, Num x, MonadCell m)+    => Num (Prop m x) where+  (+) = Binary (Cell.binary addR)+  (-) = Binary (Cell.binary subR)++  abs    = Unary (Cell.unary absR)+  negate = Unary (Cell.unary negateR)++  (*) = Binary \these those total ->+    -- Division isn't in 'Num', so we can't invert!+    Cell.watch these \this -> Cell.with those \that ->+      Cell.write total (this * that)++  fromInteger = Nullary . Cell.fill . Prelude.fromInteger+  signum = Unary \these those -> Cell.watch these (Cell.write those . signum)++instance (AbsR x, Fractional x, FractionalR x, Num x, MonadCell m)+    => Fractional (Prop m x) where+  (/) = Binary (Cell.binary divideR)++  fromRational = Nullary . Cell.fill . Prelude.fromRational+  recip = Unary (Cell.unary recipR)++-- | Lift a cell into a propagator network. Mostly for internal library use.+up :: Applicative m => Cell m x -> Prop m x+up = Nullary . pure++-- | 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)+down = \case+  Nullary x -> x++  Unary f a -> do+    x <- down a+    y <- Cell.make+    +    f x y+    pure y++  Binary f a b -> do+    x <- down a+    y <- down b+    z <- Cell.make++    f x y z+    pure z++-- | Lift a regular value into a propagator network. This is analogous to+-- 'pure' for some 'Applicative' type.+lift :: MonadCell m => x -> Prop m x+lift = Nullary . Cell.fill++-- | 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+over f = Unary \x y -> Cell.watch x (Cell.write y . f)++-- | 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+unary f = Unary (Cell.unary f)++-- | 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+binary f = Binary (Cell.binary f)++-- | 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+lift2 f = binary \(x, y, _) -> (mempty, mempty, f x y)++-- | 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 b => Prop m b -> Prop m b -> Prop m b+(.&&) = Binary (Cell.binary andR)++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 b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b+all' f = and' . map f++-- | 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 b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b+allWithIndex' f = all' (uncurry f) . zip [0 ..]++-- | 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 b, MonadCell m) => [ Prop m b ] -> Prop m b+and' = foldr (.&&) true++-- | 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 b, MonadCell m) => (x -> Prop m b) -> [ x ] -> Prop m b+any' f = or' . map f++-- | 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 b, MonadCell m) => (Int -> x -> Prop m b) -> [ x ] -> Prop m b+anyWithIndex' f = any' (uncurry f) . zip [0 ..]++-- | 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 b, MonadCell m) => Prop m b+false = Nullary (Cell.fill falseR)++-- | 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 b, MonadCell m) => Prop m b -> Prop m b +not' = Unary (Cell.unary notR)++-- | 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 b, MonadCell m) => [ Prop m b ] -> Prop m b +or' = foldr (.||) false++-- | 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 b, MonadCell m) => Prop m b+true = Nullary (Cell.fill trueR)++-- | Calculate the disjunction of two boolean propagator network values.+(.||) :: BooleanR b => Prop m b -> Prop m b -> Prop m b+(.||) = Binary (Cell.binary orR)++infixr 2 .||++-- | 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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.==) = Binary (Cell.binary eqR)++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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(./=) = Binary (Cell.binary neR)++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 x b, MonadCell m) => [ Prop m x ] -> Prop m b+distinct = \case+  x : xs -> all' (./= x) xs .&& distinct xs+  [    ] -> Nullary (Cell.fill trueR)++-- | 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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.>) = Binary (Cell.binary gtR)++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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.>=) = Binary (Cell.binary gteR)++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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.<) = Binary (Cell.binary ltR)++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 x b, MonadCell m) => Prop m x -> Prop m x -> Prop m b+(.<=) = Binary (Cell.binary lteR)++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+(.+) = Binary (Cell.binary addR)++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+negate' = Unary (Cell.unary negateR)++-- | 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+(.-) = Binary (Cell.binary subR)++infixl 6 .-++-- | 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+(.*.) = Binary (Cell.binary timesR)++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+(./.) = Binary (Cell.binary divR)++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+(.%.) = Binary (Cell.binary modR)++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+(.*) = Binary (Cell.binary multiplyR)++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+(./) = Binary (Cell.binary divideR)++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+recip' = Unary (Cell.unary recipR)++-- | 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+abs' = Unary (Cell.unary absR)++-- | 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 'Data.JoinSemilattice.Defined.Defined').+(.$) :: (Mapping f c, c x, c y) => (x -> y) -> Prop m (f x) -> Prop m (f y)+(.$) f = Unary (Cell.unary (mapR \( x, _ ) -> ( x, f x )))++-- | 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 'Control.Applicative.liftA2' for propagators./+zipWith' :: (Zipping f c, c x, c y, c z) => ((x, y, z) -> (x, y, z)) -> Prop m (f x) -> Prop m (f y) -> Prop m (f z)+zipWith' f = Binary (Cell.binary (zipWithR f))++-- | 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)+(.>>=) xs f = Unary (Cell.unary (flatMapR \( x, _ ) -> ( x, f x ))) xs
+ test/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}