Skip to content

provide filter for Alternative and Monad? #43

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

Closed
safareli opened this issue Apr 21, 2017 · 5 comments
Closed

provide filter for Alternative and Monad? #43

safareli opened this issue Apr 21, 2017 · 5 comments

Comments

@safareli
Copy link

We can define filter which work on any Alternative and Monad

filter ::  m a. Alternative m => Monad m => (a -> Boolean) -> m a -> m a
filter f m = m >>= \x -> if f x then pure x else empty

I think this repo is best place for it, but i might be wrong.

@paf31
Copy link
Contributor

paf31 commented Apr 21, 2017

Sounds useful, but we should consider using MonadZero or MonadPlus. What can you prove about this function given just Alternative and Monad?

@safareli
Copy link
Author

Technically we need Plus for empty, Chain for >>= and Applicative for pure

::  m a. Plus m => Chain m => Applicative m => (a -> Boolean) -> m a -> m a

But if we should use one from MonadZero or MonadPlus I guess MonadZero is just enough.

About proving something don't know, there are cople filter and filterMap related laws in Filterable. (btw filterMap could be implemented this way too)

I think these are correct assumptions:

(filter g) <<< (filter f) = filter (\x -> f x || g x) -- composition?
(filter f) <<< (filter f) = filter f -- ???
filter (const true) = id -- identity?

@hdgarrood
Copy link
Contributor

You can prove things with just Monad and Alternative; see for example #51.

filter (const true) = identity is fairly easy to establish: we have:

filter (const true) m
= m >>= \x -> if const true x then pure x else empty
= m >>= \x -> pure x
= m >>= pure
= m

I don't think filter g <<< filter f = filter (\x -> f x || g x) holds though. Consider:

filter isOdd (filter isEven (pure 1))
= filter isOdd (pure 1 >>= \x -> if isEven x then pure x else empty)
= filter isOdd (if isEven 1 then pure 1 else empty)
= filter isOdd empty
= empty >>= if isOdd x then pure x else empty
= empty

filter (\x -> isOdd x || isEven x) (pure 1)
= pure 1 >>= \x -> if (isOdd x || isEven x) then pure x else empty
= if (isOdd 1 || isEven 1) then pure 1 else empty
= pure `

However, I'm struggling to think of a concrete type for which this would be useful. For sequence types like List or Array which have a concat-mappy Bind instance, this will do the same as your standard filterA, but with terrible performance. For effect types like Effect or Aff, it's essentially an assertion that the result satisfies the predicate supplied, except that you'll get a useless error message if it doesn't. If that's the kind of thing you want, it would be better to use MonadThrow, I think.

I'm going to close this for now for this reason plus the fact that it hasn't been touched in a long time, but please feel free to comment if I'm missing something.

@safareli
Copy link
Author

This might be correct:

-(filter g) <<< (filter f) = filter (\x -> f x || g x)
+(filter g) <<< (filter f) = filter (\x -> f x && g x)

(not posting with intent to reopen this issue tho)

@hdgarrood
Copy link
Contributor

Oh yeah of course, that certainly seems more plausible.

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

3 participants