decide :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide fx = case extract fx of
Left a -> Left $ either id (const a) <$> fx
Right b -> Right $ either (const b) id <$> fx
lightly edited from the final snippet here (which doesn't typecheck and might have a typo)
symm :: Either a b -> Either b a
symm = either Right Left
lcostrength :: Comonad f => f (Either a b) -> Either a (f b)
lcostrength fab = case extract fab of
Left a -> Left a
Right b -> Right $ const b <$> fab
rcostrength :: Comonad f => f (Either a b) -> Either (f a) b
rcostrength = symm . lcostrength . fmap symm
decide1 :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide1 = lcostrength . fmap rcostrength . duplicate
decide2 :: Comonad f => f (Either a b) -> Either (f a) (f b)
decide2 = rcostrength . fmap lcostrength . duplicate
-- decide1 = decide2 =? decide
Can anyone see if the following definition:
lightly edited from the final snippet here (which doesn't typecheck and might have a typo)
Would be the same as the following definition(s):
const b <$> fabbeeither (const b) id <$> fab?After fixing the definition, the proof https://gist.github.com/Lysxia/11306596b08e2589a5a0dca9bf24b51a
It's honestly easier to prove with Coq than to think about whatever that means.
Also, the QuickCheck tests: https://gist.github.com/Lysxia/2394853edba387c3ba0fa8599e44a7be
@Lysxia Do you mean that
const b <$> fabwouldn't typecheck or that it's wrong despite typechecking?I vaguely remember sticking all this in an ideone snippet before I posted here, so I think it typechecks
Also, thanks so much for working out a proof!
Oh, right. I get what's wrong with
const bnow. It'll overwrite stuff that we don't need to overwriteHmm, I'm increasingly suspicious that what I've labeled a strength isn't actually a strength
Although that discussion is probably more appropriate for #Category theory
nvm it's a strength