Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cokleisli does not satisfy Choice laws #99

Open
viercc opened this issue Dec 15, 2021 · 1 comment
Open

Cokleisli does not satisfy Choice laws #99

viercc opened this issue Dec 15, 2021 · 1 comment

Comments

@viercc
Copy link

viercc commented Dec 15, 2021

The instance instance Comonad w => Choice (Cokleisli w) doesn't follow the Choice laws. It would have been if Cokleisli w was a conforming ArrowChoice, but it isn't (although it has the instance.)

ekmett/comonad#36

Maybe it's already alarmed by the notice 'extract' approximates 'costrength' attached to the Choice instance, but it wasn't clear for me.

@jasoncarr0
Copy link

jasoncarr0 commented Dec 15, 2021

To copy it out here, this is an alternate, explicit implementation:

left (Cokleisli f) = Cokleisli (\fac ->
  case extract fac of
    Right c -> Right c
    Left a -> Left . f $ fmap (either id (const a)) fac)

which has also been mentioned in a few other forums. I have previously verified that it meets the definition for co-cartesian co-strength manually, and it appears that these could be equivalent to the laws for Choice at first glance, and likewise this should meet the laws, although it would be a breaking change in the implementation.

It's not clear why the implementation would appear to not be the same, if the linked issue is to be believed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants