ekmett/ersatz

make it easier to write types

Closed this issue · 4 comments

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

  • somewhat complicated mentally (it leaks an implementation detail - why should I care about MonadState)
  • super inconvenient: Just to write the type, I have to import an extra module,
    and add an extra package (mtl) in the cabal file.

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

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?

Yes this would improve things greatly.

It still leaks the s?

glguy commented

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.

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