Skip to content
New issue

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

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

Already on GitHub? # to your account

Clarify laws of NonDet #284

Open
michaelpj opened this issue Dec 4, 2024 · 2 comments
Open

Clarify laws of NonDet #284

michaelpj opened this issue Dec 4, 2024 · 2 comments

Comments

@michaelpj
Copy link
Contributor

NonDet satisfies the "left-catch" law for MonadPlus but not the "left-distribution" law. This is a little surprising, since that makes it more "maybe-like" than "list-like" (Maybe satisfies "left-catch" but not "left-distribution", and vice versa for lists), which isn't quite what I'd expect for a non-determinism monad.

return x `mplus` m = return x -- left catch
(m `mplus` n) >>= k  =  (m >>= k) `mplus` (n >>= k) -- left distribution

In practice this means that:

do
   v <- a <|> b
   f v

is not the same as

(f a <|> f b)

so you can't guard after you <|>, etc.

I don't think it's possible to satisfy "left-distribution" with NonDet as it's currently implemented, since it's implemented with exceptions. So I just think we should say something in the documentation, to save future people some time!

@arybczak
Copy link
Member

arybczak commented Dec 5, 2024

Somewhat related: fused-effects/fused-effects#457

Perhaps this effect shouldn't have been named NonDet 😛 but it's too late.

Do you have any suggestion for the documentation improvement?

@michaelpj
Copy link
Contributor Author

Interesting! I think that's the opposite. I don't know what "algebraic" means in this context, but it sounds like their Choice effect satisfies left-distribution ,which is what I want.

I'll make you a PR :)

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

No branches or pull requests

2 participants