Your reply makes me think that I probably didn’t explain my original proposal clearly enough, so I shall try to elaborate further.
It’s very important to note that I am not suggesting running the SMT solver directly in the IO
monad. I am suggesting defining a monad SMT
(in fact in practice probably a transformer SMTT
) in which SMT actions can be run. In particular there will be a function solve :: Params -> SMT Result
. This SMT
monad will be (morally) pure. That is, the following equivalences hold in SMT
:
do
x <- mx
y <- my
...
==
do
y <- my
x <- mx
...
do
_ <- m
...
==
do
...
do
x1 <- m
x2 <- m
...
==
do
x1 <- m
let x2 = x1
...
(If they don’t hold exactly then they hold modulo some set of observations that you care about. That’s the “morally” part.)
These equivalences (or similar) allow you to prove the results that you want. In particular:
Is
mapM (f <=< g) xs
, in fact, equal tomapM g xs >>= mapM f
?
Yes! In SMT
it would be.
Then the question arises “how do I get the a
out of an SMT a
?”. Well, the answer is you use runSMT :: SMT a -> IO a
.
Calling
mapM f xs
for somexs
implies an explicit execution order which might forbid parallel implementations whereasmap
is inherently parallel.
I’m not sure what you mean. map
is not “inherently parallel”. It is sequential, as can be verified by looking at its implementation. Perhaps you are thinking of parMap
? But if you want similar “parallel” functionality in SMT
then you can define parallelSMT :: SMT a -> SMT b -> SMT (a, b)
, without needing to pretend that calling out to an external process is “pure”.
Another aspect is the API design. Up to which point is it a good idea to burden all users and all uses of a library to deal with implementation specific (i.e.: non-essential) complexity just because the implementors couldn’t solve an implementation puzzle?
This seems to be begging the question: what exactly about SMT
is “complexity”? It would just be a normal monad, something that Haskellers are perfectly happy to deal with.
A great example is the
bytestring
library. It provides an API designed to be pure and elegant and hides a lot of the implementation concerns away where they belong: inside the implementation. How wouldByteString
look like if all functions returnedIO ByteString
instead?
I’m not sure what you mean. bytestring
isn’t secretly using IO
inside and unsafePerformIO
is not used in it, except to allocate ByteString
s (which arguably should be a pure part of the run time system). It doesn’t call out to external processes!
In the particular example of the SMT solver, we need
IO
just because there is no SMT solver written purely in Haskell, hence we need to talk to another process. Otherwise, it is an operation that has a very clear specification:solve env exp = True
iffexp
is SAT.
Sure, and solving in the SMT
monad also has a very clear specification solve env exp = pure True
iff exp
is SAT.
I’m still not seeing how a monadic interface is much of an inconvenience, and certainly not at all an inconvenience to the compared to the rest of the codebase which is presumably using many monads already. So if you could elaborate further with more details of such inconvenience then I would appreciate it.