A simple account of "filterability" using category theory
A categorical interpretation of what it means to be "filterable".
class Functor f => Filterable f
where
trivial :: f Void -> ()
partition :: f (Either a b) -> (f a, f b)
A filterable functor is a symmetric oplax monoidal functor from ->
under the Either
monoidal structure to ->
under the (,)
monoidal
structure.
This is nice, because it has sensible interactions with the concept of
Alternative
functors, which are simply symmetric lax monoidal functors
between the same structures:
class Functor f => Alternative f
where
empty :: () -> f Void
union :: (f a, f b) -> f (Either a b)
The laws simply follow from the definition of (co)-lax monoidal functors, and somewhat surprisingly, manage to catch definitions of filtering that "feel wrong". See the quickcheck stuff in the code (and try out some "wrong" instance definitions to see if they're caught).
Some functors happen to only support one of Filterable
and
Alternative
, some support both, and some (fewer still), happen to
support both in a way such that the pairs of coherence maps form an
isomorphism. Such functors are strong monoidal functors between the
aforementioned monoidal structures.
instance (Monad f, Alternative f) => Filterable f
where
partition m = (m >>= either pure (const empty), m >>= either (const empty) pure)
-- Incidentally, this works out to what I wrote by hand and quickchecked for [] and Maybe
class Functor f => Decide f
where
decide :: f (Either a b) -> Either (f a) (f b)
instance (Decide f, Alternative f) => Filterable f
where
partition m = either (, mempty) (mempty, ) $ decide m
Filterable seems to have something to do with the ability to write "conditional tautologies", as in the dichotomy between Hilbert style vs Gentzen style deduction.
TODO: Pursue this