content: # 🕵️‍♂️ 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.
  
  Now available on [Hackage](https://hackage.haskell.org/package/holmes)!
  
  <!--
  
  ```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 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._
  