Open Lysxia opened 6 years ago
Perhaps it would make sense to move your trick into the library? That way we can also use Map (Reference ...)
-like models...
I thought a bit more about this, and I'm beginning to wonder if post-conditions shouldn't have the type model Symbolic -> act Symbolic resp -> resp -> Bool
?
Or perhaps the Var
from Symbolic
can be threaded through into Concrete
and used for equality checks?
I played around a bit more with this in #209, see:
data Concrete a where
Concrete :: Typeable a => a -> Unique -> Concrete a
instance Eq (Concrete a) where
Concrete _ u1 == Concrete _ u2 = u1 == u2
instance Eq (r a) => Eq (Reference a r) where
Reference r1 == Reference r2 = r1 == r2
reference :: Typeable a => a -> IO (Reference a Concrete)
reference x = Reference <$> (Concrete x <$> newUnique)
It seems to work, but I needed:
transition :: forall r. ForallF Ord r => model r -> cmd r -> resp r -> model r
Which is terrible to work with, but maybe we can revisit this approach when GHC gets qualified contexts.
We have an instance
(Eq1 v, Eq a) => Eq (Reference v a)
, which requires that the underlying reference type be comparable (Eq a
). That happens to be fine withIORef
but in general reference types such as mutable vectors do not have such an instance. A workaround is a wrapper that carries a unique identifier for each reference (see here for example), but could qc-state-machine integrate that somehow?