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 to`mapM 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 some`xs`

implies an explicit execution order which might forbid parallel implementations whereas`map`

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 would`ByteString`

look like if all functions returned`IO 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`

iff`exp`

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.