how to notate types for expressions

[jwaldmann]

I adapted a very simple example from smtlib2 version 0.3.1 to 1.0, see https://gitlab.imn.htwk-leipzig.de/waldmann/cp-ws16/commit/d53f037fc7c9a71a63dd6de70369aea9459ec69b

This is all more or less straightforward, but one thing appears really inconvenient to me: types for expressions. Consider this definition:

decimal xs =  foldl (\x y -> cint 10 .*. x .+. y) (cint 0) xs

in 0.3.1. it had type

decimal :: [  SMTExpr Integer ] -> SMTExpr Integer

but now ghci tells me

*Main> :t decimal
decimal
  :: (Language.SMTLib2.Internals.Interface.MonadResult b
      ~
      e 'IntType,
      Language.SMTLib2.Internals.Interface.HasMonad b, Embed m e,
      Foldable t, Language.SMTLib2.Internals.Interface.MatchMonad b m) =>
     t b -> m (e 'IntType)

What!? Is there a shorter notation, perhap some typedefs?

[hgoes]

I agree that the infered type for the expression is a bit overwhelming. Let's break it down:

1. The Foldable context isn't my fault, it comes from the new Prelude which generalizes foldl. So we can specialize it to: (MonadResult b ~ e 'IntType, HasMonad b, Embed m e, MatchMonad b m) => [b] -> m (e 'IntType)
2. The "HasMonad" context means that the "b" type can either be an SMT expression, or a monadic action producing an SMT expression. This is useful because now (x .+. y) .*. z is the same as do { tmp <- x .+. y; tmp .*. z } which makes for much more readable code. But we can easily specialize the signature for SMT expressions: (Embed m e) => [e IntType] -> m (e IntType)
3. The new interface supports doing more things with SMTLib expressions aside from using them in an SMT solver (evaluating them directly, doing abstraction etc), so I introduced the "Embed" class, which essentially states "this monad can produce SMTLib expressions". One such monad is the SMT monad, so we can specialize that as well: Backend b => [Expr b IntType] -> SMT b (Expr b IntType)

Hope that helps.

[hgoes]

Yes, I would suggest using the signature in item 2 or 3. Unfortunately, I don't know if there is a way to make the infered type signature more understandable.

[jwaldmann]

E.g., in ersatz (I know it's SAT not SMT, but they also write formulas) you really build terms, and only later interpret them (in whatever monad). So the term (formula) type looks nice and clean. https://hackage.haskell.org/package/ersatz-0.3.1/docs/Ersatz-Bit.html . (I think that's what you had with SMTExpr a in version 0.3.)

This has the advantage, e.g., that terms that describe numbers can be instances of Num (so you can use the standard definitions of sum, etc). Yes, Num is broken in many ways, but for simple things, it works good enough.

The disadvantage (of working in the Identity monad) is that you need (?) observable sharing for the term type and this looks ugly (e.g., unsafePerformIO (makeStableName' a) in https://hackage.haskell.org/package/ersatz-0.3.1/docs/src/Ersatz.Problem.html#runSAT ) but it's confined to a library.

[jwaldmann]

"inferred signatures more understandable" - I think if some type synonyms are in scope, ghci will try to use them (to some degree).

[hgoes]

Another disadvantage is that you have to keep a representation of all the formulas you're building in memory, basically replicating what your backend is doing. The advantage of the new API is that you can actually use the native expression type of whatever backend you're using as the result type of all SMTLib operations, thus avoiding having to translate back and forth between two representations.

I've built native backends for Z3 and MathSAT (not currently on hackage because they are incomplete) that make use of this fact.

My guess is that the ersatz library is designed to be more of an "specify a problem, send it off to the solver" interface, whereas my library aims for continuous interaction with a solver for example getting interpolants, incremental solving etc.