Open ksqsf opened 3 years ago
Hi and thanks for starting this discussion again!
About 5 months ago I asked the same thing, e.g. building an improved interface layer over the current one. There has been an attempt at this in the past:
https://hackage.haskell.org/package/z3-0.3.2/docs/Z3-Lang-Prelude.html
As far as I understood it was abandoned because library users preferred to build their own abstractions which directly match their needs. But @IagoAbal told me that he is still open to it. I have not started working on this yet, but would love to. What I was missing so far was my own use case because I am currently not using the library in any projects. If you bring this, I am happy to help with building a higher-layer interface.
My perspective on your specific points:
- Every call is prefixed with
mk
The current API is a minimal wrapper around the C API, so the function names should just be camelCased versions of the original C API functions [1]. In my opinion, having consistent naming with the Z3 documentation is worth more than these prefixes hurt. In a higher layer interface we could definitely choose new names.
- Every call is inside the Z3 monad, so even if it's just building an AST, there must be <$> and <*>. sequences are spilled everywhere without clear motivation.
I think this is because there isn't much of a Haskell AST, a Haskell AST node is just a wrapped ForeignPtr
to the C AST node. So before being able to use a new node, the monadic action of calling the constructor needs to be performed. I think we should avoid re-defining and building a separate Haskell AST. But maybe we could play some tricks behind the scenes in order to make something like this possible (correct me if this is not what you described/wanted):
xPlusy <- mkAdd [mkFreshIntVar "x", mkFreshIntVar "y"]
-- as opposed to
x <- mkFreshIntVar "x"
y <- mkFreshIntVar "y"
xPlusy <- mkAdd [x,y]
- Literals must be mk'd. This is an unnecessary burden.
Definitely! It would be very nice if we could automatically lift Haskell Bool
and Int
literals at least. But I think this is a job for a higher layer and this low-level API does not need it.
- Do we really need Int in evalInt m? The type seems to be deducible from the context.
Since it is all ForeignPtr
s from the Haskell perspective, there is no sort information on the Haskell level, e.g. the AST is untyped. So eval
just computes a ForeignPtr -> ForeignPtr
function and then additional information is required to interpret the resulting node. Deducing Int
from the context would require a typed AST I believe.
- mkLe mkSub ... They all seem unintuitive and ugly.
Same as point 1.
So I think there are two key ideas here worth discussing/pursuing:
BoolAST
, IntAST
, ArrayAST s1 s2
etc), i.e. turn sort-errors directly into Haskell compiler errors. I think the type systems should be compatible such that this is possible in a natural way. But maybe there are API functions which then no longer typecheck on the Haskell level, not sure. Maximum safety, minimum flexibility. A second option could be dynamic where we store the sort as additional field with the AST node and check sorts at runtime. This would most likely give better error messages, but it is not 100% clear to me if that provides additional value since Z3 also sort-checks. It would still allow us to drop the Int
from evalInt
and the like.Apart from these I think the current API has its place and should stay as a minimal transparent C wrapper.
Thanks for your detailed reply!
I agree that the low-level API should be kept, and the 'simpler' interface should be a separate module (or even a package).
But maybe we could play some tricks behind the scenes in order to make something like this possible (correct me if this is not what you described/wanted) [...]
I'm not sure how to do this, but this example looks really neat! If it's achievable, I believe most of my complaints are instantly gone.
Typed AST
It seems that the previous Z3.Lang
is exactly this. I'm still not sure why it's abandoned. My guess is that a separate AST type doesn't always satisfy people's needs, so the interoperability with the low-level API is important. If so, a complete wrapper (like z3py) and/or convert functions from/to raw z3 types should be enough.
My plan is to first experiment with the previous Z3.Lang and see how it can be extended in the next few days.
Template Haskell
I think it can be used to generate Z3
monad-compatible code, so interoperability is better than typed AST. But on a second thought, syntax like [z3|if x<0 then -x else x]
doesn't add more value than If (x<0) (-x) x
, and we have to implement a type checker to infer the types of literals. (This is my gut feeling, so maybe I'm wrong here.)
My plan is to first experiment with the previous Z3.Lang and see how it can be extended
Sounds good, feel free to ping me or report any problems/requests here. I will think about potential designs as well and hopefully then we can draft something.
I think it's interesting to have a deep DSL. Generate an intermediate AST, perform some checks on it, then pass it down to the lower-level Z3 library. That should help making a better higher-level API, although errors would still be caught at runtime. I personally don't have time to get into that kind of project, but I am happy to participate in discussions and review code.
But I don't find a shallow DSL powered by Haskell's type hackery to be very interesting, and it's a lot harder and more work than one initially thinks. That is why we abandoned Z3.Lang
. If you want to play with SMT and write stuff by hand... then yes a shallow DSL is very nice. But if you're writing a tool that uses Z3 as a verification backend, and then you generate different SMT problems depending on what you get as input... then that shallow DSL is not that useful and, in fact, it may actually be rather cumbersome to work with.
Hey guys! What's the current state of this issue?
Hi! I wasn't aware of SBV when I opened this issue. I was frustrated then, because I thought Haskell deserved something better than a low level wrapper. It took me some time to discover (maybe rediscover?) SBV. SBV seems pretty complete and capable, and fulfills my current needs.
I certainly see the necessity of a low-level Z3 library (the current haskell-z3
), but I'm not sure I want to work on a / another Z3-specific high-level wrapper now. So, feel free to close this issue! :)
The current interface IMHO is pretty primitive. The readme includes a 4queen example, but that is unnecessarily tedious, frustrating, and straight terrifying.
I believe you have more experience with z3 than me, but I made some simplifications to the 4queen example. It's still very tedious.
Specifically,
mk
.Z3
monad, so even if it's just building an AST, there must be<$>
and<*>
.sequence
s are spilled everywhere without clear motivation.mk
'd. This is an unnecessary burden.Int
inevalInt m
? The type seems to be deducible from the context.mkLe
mkSub
... They all seem unintuitive and ugly.As I personally want to use Haskell for my next z3-related project, I'm concerned with the productivity implication. I used to use z3py. Simple tasks are really simple, intuitive, and even good-looking. But complex tasks are ugly (e.g. folding over a list of expressions). Haskell-z3 seems to be on the opposite extreme, where complex tasks are made fairly easy (e.g.
assert =<< mkAnd =<< T.sequence [ mkLe _1 qi | qi <- q ]
) but simple tasks are less than ideal (e.g.mkInteger 0 >>= \_0 -> join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
versus z3py's straightforwardIf(0 <= x, x, -x)
).I believe Haskell-z3 can have the best of the both worlds. But before I set out to start coding, I decide to create an issue first to gather opinions: Is a better interface really needed? What could the design be? What are the previous attempts (if any) and how they turned out to be? After a design is sketched out, I'm willing to implement it. If it's not really important or it's a dead-end, I'll save some time. :)
(IMHO, the whole situation is like embedding the Z3 language into Haskell, and we automatically get several existing designs: Free monads, GADTs, and tagless final. But I'd like to add that Template Haskell should also be considered, as it allows us to write something like
[z3| if 0 <= x then x else -x |]
instead ofmkInteger 0 >>= \_0 -> join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x
. This however still needs duplicating AST definitions, which is very undesirable.)