advancedtelematic / quickcheck-state-machine

Test monadic programs using state machine based models
Other
203 stars 25 forks source link

Actions that return two references can't be expressed #197

Closed stevana closed 6 years ago

stevana commented 6 years ago

If we have an action like:

Apa :: Action (Ref1, Ref2)

then the transition function will have access to v (Ref1, Ref2) rather than the much more useful (v Ref1, v Ref2).

Not sure how to solve this. It would be nice if failing semantics, i.e. when transition has access to Either err (v Ref) could also be made a special case of the solution.

stevana commented 6 years ago

One possible solution might involve introducing a universe of responses, e.g.:

data Response = Return Type | Type :+: Type | Type :*: Type

type familiy Response_ v u where
  Response_ v (Return a) = v a
  Response_ v (a :+: b)  = Either a (v b)
  Response_ v (a :*: b)  = (v a, v b)

And then change transition to be:

type Transition model act = forall v. model v -> act v resp -> Response_ v resp -> model v

This complicates the definition of actions however, by indexing them by Response rather than just *... It's also not as general as it could be, i.e. lets say you want to return three references. One could imagine using , data Response = ... | Response :*: Response instead, but this would make the implementation of, say, generating programs tricker (where we would need to use Typeable or singletons to reify the response and do the appropriate thing).

I guess another approach is to drop the indexing of actions altogether as discussed in #170. Something like:

data Response' v resp err
  = Return (v resp)
  | err :+: v resp
  | v resp :*: v resp

type Transition' model act resp err = forall v. 
    model v -> act v -> Response' v resp err -> model v

Thoughts?

stevana commented 6 years ago

Fixed as part of #209 by not using a GADT for actions, but instead having a response datatype. The transition function's type changed to:

model v -> act v -> resp v -> model v

Notice that there's no v around resp, more work is required by the user, see the mock function in the readme.