diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.lhs b/README.lhs new file mode 100644 --- /dev/null +++ b/README.lhs @@ -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. + + + +## πŸ‘Ÿ 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**!_ + + + +## πŸš‚ 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._ diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. + + + +## πŸ‘Ÿ 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**!_ + + + +## πŸš‚ 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._ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Futoshiki.hs b/examples/Futoshiki.hs new file mode 100644 --- /dev/null +++ b/examples/Futoshiki.hs @@ -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 + ] diff --git a/examples/Main.hs b/examples/Main.hs new file mode 100644 --- /dev/null +++ b/examples/Main.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-} diff --git a/examples/WaveFunctionCollapse.hs b/examples/WaveFunctionCollapse.hs new file mode 100644 --- /dev/null +++ b/examples/WaveFunctionCollapse.hs @@ -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 diff --git a/holmes.cabal b/holmes.cabal new file mode 100644 --- /dev/null +++ b/holmes.cabal @@ -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 diff --git a/src/Control/Monad/Cell/Class.hs b/src/Control/Monad/Cell/Class.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Cell/Class.hs @@ -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 diff --git a/src/Control/Monad/Holmes.hs b/src/Control/Monad/Holmes.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Holmes.hs @@ -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) diff --git a/src/Control/Monad/MoriarT.hs b/src/Control/Monad/MoriarT.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/MoriarT.hs @@ -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 diff --git a/src/Control/Monad/Watson.hs b/src/Control/Monad/Watson.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Watson.hs @@ -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)) diff --git a/src/Data/CDCL.hs b/src/Data/CDCL.hs new file mode 100644 --- /dev/null +++ b/src/Data/CDCL.hs @@ -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 diff --git a/src/Data/Holmes.hs b/src/Data/Holmes.hs new file mode 100644 --- /dev/null +++ b/src/Data/Holmes.hs @@ -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 diff --git a/src/Data/Input/Config.hs b/src/Data/Input/Config.hs new file mode 100644 --- /dev/null +++ b/src/Data/Input/Config.hs @@ -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) diff --git a/src/Data/JoinSemilattice/Class/Abs.hs b/src/Data/JoinSemilattice/Class/Abs.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Abs.hs @@ -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 ) diff --git a/src/Data/JoinSemilattice/Class/Boolean.hs b/src/Data/JoinSemilattice/Class/Boolean.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Boolean.hs @@ -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 + ) diff --git a/src/Data/JoinSemilattice/Class/Eq.hs b/src/Data/JoinSemilattice/Class/Eq.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Eq.hs @@ -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 + ) diff --git a/src/Data/JoinSemilattice/Class/FlatMapping.hs b/src/Data/JoinSemilattice/Class/FlatMapping.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/FlatMapping.hs @@ -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) + ) diff --git a/src/Data/JoinSemilattice/Class/Fractional.hs b/src/Data/JoinSemilattice/Class/Fractional.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Fractional.hs @@ -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) diff --git a/src/Data/JoinSemilattice/Class/Integral.hs b/src/Data/JoinSemilattice/Class/Integral.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Integral.hs @@ -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) + ) diff --git a/src/Data/JoinSemilattice/Class/Mapping.hs b/src/Data/JoinSemilattice/Class/Mapping.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Mapping.hs @@ -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' ) diff --git a/src/Data/JoinSemilattice/Class/Merge.hs b/src/Data/JoinSemilattice/Class/Merge.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Merge.hs @@ -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 + diff --git a/src/Data/JoinSemilattice/Class/Ord.hs b/src/Data/JoinSemilattice/Class/Ord.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Ord.hs @@ -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 + ) diff --git a/src/Data/JoinSemilattice/Class/Sum.hs b/src/Data/JoinSemilattice/Class/Sum.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Sum.hs @@ -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) diff --git a/src/Data/JoinSemilattice/Class/Zipping.hs b/src/Data/JoinSemilattice/Class/Zipping.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Class/Zipping.hs @@ -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 + ) diff --git a/src/Data/JoinSemilattice/Defined.hs b/src/Data/JoinSemilattice/Defined.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Defined.hs @@ -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 ] diff --git a/src/Data/JoinSemilattice/Intersect.hs b/src/Data/JoinSemilattice/Intersect.hs new file mode 100644 --- /dev/null +++ b/src/Data/JoinSemilattice/Intersect.hs @@ -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) diff --git a/src/Data/Propagator.hs b/src/Data/Propagator.hs new file mode 100644 --- /dev/null +++ b/src/Data/Propagator.hs @@ -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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}