That's true (and mostly is due to the concrete nature of Bool) but even so, parametricity does help a lot implementing that function. `forall a.` cuts down on p

That's true (and mostly is due to the concrete nature of Bool) but even so, parametricity does help a lot implementing that function. `forall a.` cuts down on possible implementations, but you still gotta program sometimes :) In a more dependently-typed language, we can write something like this f1 :: (p :: a -> Bool) -> [a] -> [a `suchThat` p a] f2 :: (p :: a -> Bool) -> [a] -> [a `suchThat` not (p a)] and that would make it so f1 couldn't be filterNot and f2 couldn't be filter. And we get the added benefit of giving the caller of our function the proof that the elements have passed that predicate (maybe they can make use of that downstream) But even in this case, there's nothing stopping you from just always returning an empty list. Not all theorems come for free!