Coapplicatives from comonads - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

Can anyone see if the following definition:

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)

Asad Saeeduddin

Would be the same as the following definition(s):

Asad Saeeduddin
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
  1. Shouldn't const b <$> fab be either (const b) id <$> fab?
  2. This looks easily quickcheckable.

After fixing the definition, the proof

Equivalent definitions of "decide" for comonads (comonads are (some kind of) monoidal functors) - comonad_decide.v

It's honestly easier to prove with Coq than to think about whatever that means.


Also, the QuickCheck tests:

Testing before - decide.hs
Asad Saeeduddin

@Lysxia Do you mean that const b <$> fab wouldn't typecheck or that it's wrong despite typechecking?

Asad Saeeduddin

I vaguely remember sticking all this in an ideone snippet before I posted here, so I think it typechecks

Asad Saeeduddin

Also, thanks so much for working out a proof!

Asad Saeeduddin

Oh, right. I get what's wrong with const b now. It'll overwrite stuff that we don't need to overwrite

Asad Saeeduddin

Hmm, I'm increasingly suspicious that what I've labeled a strength isn't actually a strength

Asad Saeeduddin

Although that discussion is probably more appropriate for #Category theory