Skip to content

Instantly share code, notes, and snippets.

@isovector
Created Oct 6, 2021
Embed
What would you like to do?
prepropEquivInterpreters
:: forall effs x r1 r2
. (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
=> (forall a. Sem r1 a -> IO a)
-> (forall a. Sem r2 a -> IO a)
-> (forall r. Members effs r => Gen (Sem r x))
-> Property
prepropEquivInterpreters int1 int2 mksem = property $ do
SomeSem sem <- liftGen @effs @x mksem
pure $ ioProperty $ do
a1 <- int1 sem
a2 <- int2 sem
pure $ a1 === a2
newtype SomeSem effs a = SomeSem
{ getSomeSem :: forall r. (Inject effs r) => Sem r a
}
liftGen
:: forall effs a
. Members effs effs
=> (forall r. Members effs r => Gen (Sem r a))
-> Gen (SomeSem effs a)
liftGen g = do
a <- g @effs
pure $ SomeSem $ inject a
inject :: Inject effs r => Sem effs a -> Sem r a
inject (Sem a) = a $ liftSem . deject . hoist inject
class Inject effs r where
deject :: Union effs (Sem r) a -> Union r (Sem r) a
instance Inject '[] r where
deject = absurdU
instance {-# INCOHERENT #-} Inject r r where
deject = id
instance (Member eff r, Inject effs r) => Inject (eff ': effs) r where
deject u =
case decomp u of
Left u' -> deject u'
Right w -> Union membership w
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment