Actions that return two references can't be expressed about quickcheck-state-machine HOT 2 CLOSED

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?

from quickcheck-state-machine.

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.

from quickcheck-state-machine.