provide filter for Alternative and Monad?

[safareli]

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]

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

[safareli]

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]

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]

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]

Oh yeah of course, that certainly seems more plausible.