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

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)

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

```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 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

Testing before https://gist.github.com/Lysxia/11306596b08e2589a5a0dca9bf24b51a - decide.hs

@Lysxia Do you mean that `const b <\$> fab` wouldn'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 b` now. It'll overwrite stuff that we don't need to overwrite

Hmm, 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