i-am-tom / holmes Goto Github PK

Hi there, thanks for this lovely library! I have grand plans to (eventually) incorporate procedural generation via wavefunction collapse into https://github.com/swarm-game/swarm/ (it currently has procedural generation but only based on Perlin noise) . However, I was reading the documentation today, and it seems like I want something in between Holmes and Watson:

• I do want to generate "natural-looking" procedurally generated things, so I definitely want the random shuffling that the Holmes monad does. Besides just generating more natural-looking things, I also don't want to get the same solution every time.
• However, because I am generating infinite worlds and only dynamically generating/loading the parts of the world that are actually explored, the generation needs to be deterministic (based on a seed value), like Minecraft. I also just really don't want to introduce IO.

So I would really like a monad that (1) is built over ST, but (2) does random shuffling based on a seeded PRNG. This seems like it should be totally possible in theory --- from what I can tell Holmes is implemented in terms of shuffle from hedgehog, which has type MonadGen m => [a] -> m [a] and does not itself depend on IO in any way --- the IO only comes in from the use of sample :: MonadIO m => Gen a -> m a, which is one convenient way to run a MonadGen computation but not the only way.

Curious to hear what you think about the possibility of exposing a slightly different API which allows this. I'd be very happy to try to submit a PR if you think it seems reasonable. I saw elsewhere that you mentioned working on a rewrite of this library, so I'm not quite sure what the status is.

Hello, big fan of your library and it seems very cool. I'm trying it out with this years advent of code, and ran into this while doing the first problem. Boiled down, basically:

test :: IO (Maybe [ Defined Int ])
test = do
  let guesses = 2 `from` [1, 3]

  guesses `satisfying` \[a, b] -> and'
    [ (a .+ b) .== 5 ]

returns Just [Exactly 1,Exactly 4], where as I would've expected it to fail without a match.

I'm guessing I'm using something wrong but was surprised. Thanks again for your library!

First off, thanks for your work on this library and for providing such extensive docs. It was super easy for me to get started!

I'm currently experimenting with a constellation where the order of the elements in the solution doesn't matter. I'm pretty sure I'm missing something here, so maybe you can help me out.

data M = A | B | C | D deriving (Bounded, Eq, Enum, Ord, Generic, Hashable, Show)

solve :: IO [[Defined M]]
solve = do
  let guesses = 3 `from` [A .. D]
  guesses `whenever` \solution -> and' [distinct solution]

run :: IO ()
run = solve >>= traverse_ print . take 3

This will print

[Exactly A,Exactly B,Exactly C]
[Exactly A,Exactly B,Exactly D]
[Exactly A,Exactly C,Exactly B]

However, I'd like to add a constraint that makes the solver treat the first and the third solution as equal solutions (and therefore delete one of them from the set of possible solutions).
I could map over the solution afterwards, but this doesn't help in making the computation run faster. That's why I want to include it in the constraints.

Is there a way to do that?

TLDR: I can use pure to get a value to test against into Defined, and singleton for Intersect, but there's nothing polymorphic. Would be nice to have something.

The story behind it:

I wrote a solver for a puzzle type using Defined, which worked out fine but turned out pretty slow. So I thought I'd try out Intersect to see if that improved things. In what may have been a mistaked I tried to generalize the constraints to be able to use both Defined and Intersect.

I ran into a couple issues there:

• I had used over (fmap f) (because (.$) was broken when I started with this), which worked fine due to the Functor instance on Defined, but Intersect doesn't have that. Switching to (.$) turned out to work at the expense of having to specify terrifying type signatures. I suppose Intersect doesn't naturally admit a Functor instance? Otherwise that would be nice to have.
• I used some equality checks against given values with x .== lift (pure v), which caused an Applicative constraint which again works for Defined but not Intersect. That's this ticket.

I'll have to disclaim this report by being very much unsure what I'm doing here -- I'm plugging things together getting them to work rather than really understanding how this stuff should function, so there's a good chance I'm asking for things that don't make sense.

See https://github.com/olivierdeckers/holmes/blob/aquarium-example/examples/Aquarium.hs for an example

when running solve example4, it sometimes returns the solution, and sometimes returns Nothing.

In order to produce lift, the following class was created:

class Lifting (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
  lift' :: c x => x -> f x

Now, if we say lift 3 .== lift 4 :: Prop m (Defined Bool), we run into a problem: we can't infer a type of Defined Int (specifically the Defined part) for the 3 and 4, because there's no reversing functional dependency on the EqR class to get us from Defined Bool back to Defined Int. This makes sense - the instances are of the shape EqR (Defined x) (Defined Bool), so you couldn't have a functional dependency in the other direction even if you wanted one.

The type inference could be fixed if we restructured the EqR and OrdR classes to be of the same shape:

class EqR (f :: Type -> Type) (c :: Type -> Constraint) | f -> c where
  eqR :: c x => (f x, f x, f Bool) -> (f x, f x, f Bool)

Now, we've guaranteed that the parameter type of the input and bool result match. This means that with lift 3 .== lift 4 :: Prop m (Defined Bool), it is clear that the type of 3 must be (Num x => Defined x), which is what we're after.

This is not a lot of work, but it might be a good first issue if someone fancies getting involved in the library!

Tried to install holmes from Cabal and got this error:

src/Control/Monad/Watson.hs:55:10: error:
    Not in scope: type constructor or class ‘MonadFail’
   |
55 | instance MonadFail (Watson h) where
   |          ^^^^^^^^^

I'm using GHC version 8.6.5, it seems to be failing on Hackage CI as well.

Chances are I'm doing something wrong here, but since I'm at a point where I'm likely to shelve this toy project, thought I should report my problem just in case it's an issue with Holmes.

Concretely, my puzzle solver runs fine and slow with Defined, and typechecks but doesn't run at all with Intersect. (Doesn't run at all means: stack overflow in GHCI, non-termination in compiled executable.)

The offending function seems to be:

-- given a list of values at indexes, count how many of these occur
countEqual ::
  (Eq x, Mapping f c, c x, c v, Num v, Num (f v), SumR (f v), MonadCell m) =>
  [(Int, x)] ->
  [Prop m (f x)] ->
  Prop m (f v)
countEqual vals cells = foldr (.+) (lift 0) (map f vals)
  where
    isEqual v w = if w == v then 1 else 0
    f (i, v) = isEqual v .$ (cells !! i)

With this (and a bounded integer type Val4 with range 0..4), I see:

> let cfg = 1 `from` [1] :: Config Holmes (Defined Int)
> let prop = (\cells -> countEqual [(0, 3::Int)] cells .>= lift (pure (0::Int))) :: MonadCell m => [ Prop m (Defined Int)] -> Prop m (Defined Bool)
> cfg `satisfying` prop
Just [Exactly 1]
> let cfg = 1 `from` [1] :: Config Holmes (Intersect Val4)
> let prop cells = countEqual [(0, 3::Val4)] cells .>= lift (singleton (0::Val4))
> cfg `satisfying` prop
*** Exception: stack overflow

(Chances are there's a better way to do what I'm doing. The thing I'm trying to encode is that some values on a Sudoku-like board count certain other cells in the board according to their values and relative position.)

Thanks for making Holmes by the way! Certainly had fun figuring things out this far.