IO in Propertys

[voidus]

Heya,

I'm thinking about how to test some code that needs IO to run.
The situations I'm thinking about are more like using STM internally or something, the possibility of IO making the property unreliable is not really my focus here.

I didn't find anything in the docs, so I looked into the code. Relevant definitions:

newtype TestResultT e m a = TestResultT {
      runTestResultT :: m (TestResult e a)
    }
newtype Property' e a = WrapProperty {
      unwrapProperty :: TestResultT e (StateT TestRun Gen) a
    }
newtype Gen a = Gen { runGen :: SampleTree -> (a, [SampleTree]) }

So there's no base IO behind Gen (like in hedgehog) that we could expose through MonadIO, even if we wanted to. And we don't:

-- NOTE: 'Gen' is /NOT/ an instance of 'Alternative'; this would not be
-- compatible with the generation of infinite data structures. For the same
-- reason, we do not have a monad transformer version of Gen either.

This leaves the question: Is there a way to do what I'm looking for?

I've tried:

1. Changing TestResultT to m (IO (TestResult e a)), but couldn't write the monad instance, presumably because m isn't a monad transformer.
   Since TestResultT is applied to StateT TestRun Gen, requiring a transformer is out
2. I've reworked the Predicate to basically run in IO, but got stuck when implementing assert, which is not a big surprise I guess.

Right now, I can't really see a way to implement this at all (short of making Gen a transformer).

Maybe an interesting approach is to split the Property in a generation phase (without IO, with gen) and an assertion phase (with IO, without gen)? Seems annoying type-wise, but that would prevent the obvious footgun of depending on external input during test prep.

[edsko]

Indeed, the choice not to have IO in Gen, or support a general transformer API in Gen, is quite deliberate, as you already point out. In principle we have more leeway with Property', although we do have to be a bit careful.

However, I agree with you that a separation is the way to go here; this is the route taken for example by libraries such as quickcheck-state-machine, quickcheck-dynamic/quickcheck-lockstep, and others.

I don't think it would be that hard actually, because Property and its infrastructure is already quite general. Here's where I would start experimenting. In the tasty driver, we have

data Test = Test TestOptions (Property' String ())

We can add another

data TestIO = TestIO TestOptions (Property' String (IO ()))

alongside, with correspoinding

testPropertyIO :: TestName -> Property' String (IO ()) -> TestTree

(Perhaps it would even make sense to generalize the existing Test datatype rather than define a second one, not 100% sure.) The IsTest instance for this would do what the existing one does and share most of its code, but would perform one additional step for the test to pass: the returned IO action should run without exceptions. I think this would achieve the separation you mention, and would then also open the door to more full-fledged state modelling infrastructure (I'd love to see something like quickcheck-lockstep in falsify at some point).

What do you think? If you'd like to give it a go and get stuck somewhere, let me know and I'll try to think along.

[voidus]

Thank you for the encouragement and guidance. I'll try to look into it some more in the next days 🙂

[ejconlon]

+1 from me on this feature. I have some serialization code that is "morally pure" but allocates and fills buffers in IO during encoding, and I would love to be able to drop my unsafePerformIO!

[dpercy]

I'm also interested in this feature! (I have an external system that I want to compare to a simpler implementation in Haskell.) Maybe I could contribute something or extend #62.

On that PR, @voidus says:

I definitely want to look into making assert (or maybe a new similar function) work in IO so we can get the same rich predicates that we're used to.

We'd also probably want collect to work in IO: that way you can log the outputs from the IO action rather than just the generated inputs. So we need a type that has logging and failure, and IO, but not Gen.

Would it make sense to split the types this way?

newtype PropertyT m e a = WrapPropertyT {
      unwrapPropertyT :: TestResultT e (StateT TestRun m) a
    }

type Property' = PropertyT Gen
type PropertyIO = PropertyT IO

Then assert and collect would work in any PropertyT m, while gen requires PropertyT Gen and liftIO requires PropertyT IO. assert wouldn't need to resort to exceptions because TestResultT is available in both phases.

I suppose the Tasty adapter would take a Property (PropertyIO ()) which looks strange to me. Maybe PropertyT / PropertyIO should be called something else, to reflect that it's only about logging and failure.

What do you think: does this approach make sense?

[edsko]

@dpercy Sorry for the slow reply, I'm swamped with work. I think that the approach you sketch is not quite what we want (though perhaps I misunderstand). With IO at the bottom of the monad stack instead of Gen, you basically exclude 95% of what falsify offers. I still think my earliest suggestion is the way to go (#62 is a first stab at it but I think @voidus marked it as a a first proof of concept and it needs cleaning up). As for collect and assert, there is no reason why you can't just use eval :: Predicate '[] -> Either Err () in IO and throw an exception on the Left case; for logging it might perhaps be useful if instead of IO () we had IO [String] or some such (or perhaps Logger -> IO (), I don't know).

The most important consideration here is that all this would then still have a very strict phase separation: first generate the IO action, and then evaluate it (including, perhaps, additional asserts and additional logging). If that phase separation is too limiting, then things get a whole lot harder.