Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
I want to implement lift :: Member e r => Sem '[e] a -> Sem r a. Raise doesn't work for my purposes because everything is necessarily polymorphic and the instances don't terminate
lift :: Member e r => Sem '[e] a -> Sem r a
Hmm, maybe you could just go through Sem, unpacking that Union with single effect and sending it further?
yeah, was trying that, but the types make my head spin
who wrote this library even??
Wait, couldn't you just raise it over Embed (Sem r), interpret into it and call runEmbedded?
Embed (Sem r)
now that's an interesting idea
this seems to do it:
inject :: forall eff r a. Member eff r => Sem '[eff] a -> Sem r a
inject (Sem a) = Sem $ \k -> a $ \case
Union Here (Weaving e s f n v) ->
k $ Union (membership @eff) $ Weaving e s (inject . f) n v
amazing what a nap can do
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 (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
starting to get my sea legs back
hsakell sucks ass
• Could not deduce: Members effs effs arising from a use of ‘gen’
type family Members2 es r :: Constraint where
Members2 r r = ()
Members2 ' r = ()
Members2 (e ': es) r = (Member e r, Members2 es r)
no, doesnt seem to work great actually
adding Members effs effs to the context works /shrug
Members effs effs
put this all together to make some stuff that can prove equivalence of interpreters https://gist.github.com/isovector/681d15e9ca398692278df3612dcfc3cd