Open maralorn opened 4 years ago
Following our discussion on irc I am still trying to wrap my head around the catch handling in eff.
While looking at the law for catch I wondered if the pure is correct there.
catch
pure
According to this type signature:
catch :: Error e :< effs => Eff (Error e ': effs) a -> (e -> Eff effs a) -> Eff effs a
I deduce the types catch (throw x) f :: Eff effs a and f x :: Eff effs a, so pure (f x) :: Applicative a1 => a1 (Eff effs a)?
catch (throw x) f :: Eff effs a
f x :: Eff effs a
pure (f x) :: Applicative a1 => a1 (Eff effs a)
So I think instead of catch (throw x) f ≡ pure (f x) it should just be catch (throw x) f ≡ f x.
catch (throw x) f ≡ pure (f x)
catch (throw x) f ≡ f x
Following our discussion on irc I am still trying to wrap my head around the catch handling in eff.
While looking at the law for
catchI wondered if thepureis correct there.According to this type signature:
I deduce the types
catch (throw x) f :: Eff effs aandf x :: Eff effs a, sopure (f x) :: Applicative a1 => a1 (Eff effs a)?So I think instead of
catch (throw x) f ≡ pure (f x)it should just becatch (throw x) f ≡ f x.