ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
63 stars 15 forks source link

make it easier to write types #42

Closed jwaldmann closed 5 years ago

jwaldmann commented 5 years ago

After import Ersatz, I can define

c =  do p <- exists ; q <- exists ; assert $ xor p q ; return [p,q]

but the type of c is

c :: (mtl-2.2.2:Control.Monad.State.Class.MonadState s m,
      HasSAT s) =>
     m [Bit]

I find this

I understand the motivation for being polymorphic in the monad (e.g., I can use runSAT' c to see the clauses)

I guess I am suggesting that we re-export MonadState? or invent some type synonym?

glguy commented 5 years ago

I agree that this is annoying. When I use ersatz in my own projects I typically define

type MonadSAT s m = (HasSAT s, MonadState s m)

Let's just put this in ersatz?

jwaldmann commented 5 years ago

Yes this would improve things greatly.

It still leaks the s?

glguy commented 5 years ago

Yes, the s is necessarily visible. In addition to being unavoidable this means you can also have: (MonadSAT s m, HasQSAT s) for the cases when your doing qsat stuff.

jwaldmann commented 5 years ago

Very good, thanks for handling this, it will certainly be useful.