每个替代 Monad 都可以过滤吗？

集合的范畴包括笛卡尔幺半群和柯笛卡尔幺半群。下面列出了这两种幺半群结构的规范同构类型：

type x + y = Either x y
type x × y = (x, y)

data Iso a b = Iso { fwd :: a -> b, bwd :: b -> a }

eassoc :: Iso ((x + y) + z) (x + (y + z))
elunit :: Iso (Void + x) x
erunit :: Iso (x + Void) x

tassoc :: Iso ((x × y) × z) (x × (y × z))
tlunit :: Iso (() × x) x
trunit :: Iso (x × ()) x

为了这个问题的目的，我定义Alternative成为 Hask 下的松散幺半群函子Either张量到 Hask 下(,)张量（仅此而已）：

class Functor f => Alt f
  where
  union :: f a × f b -> f (a + b)

class Alt f => Alternative f
  where
  nil :: () -> f Void

这些定律只是针对松散幺半群函子的定律。

关联性：

fwd tassoc >>> bimap id union >>> union
=
bimap union id >>> union >>> fmap (fwd eassoc)

左单元：

fwd tlunit
=
bimap nil id >>> union >>> fmap (fwd elunit)

右单位：

fwd trunit
=
bimap id nil >>> union >>> fmap (fwd erunit)

以下是如何恢复更熟悉的操作Alternative根据松散幺半群函子编码的一致性映射的类型类：

(<|>) :: Alt f => f a -> f a -> f a
x <|> y = either id id <$> union (Left <$> x, Right <$> y)

empty :: Alternative f => f a
empty = absurd <$> nil ()

我定义Filterable函子是oplaxHask 下的幺半群函子Either张量到 Hask 下(,) tensor:

class Functor f => Filter f
  where
  partition :: f (a + b) -> f a × f b

class Filter f => Filterable f
  where
  trivial :: f Void -> ()
  trivial = const ()

其定律只是向后宽松的幺半群函子定律：

关联性：

bwd tassoc <<< bimap id partition <<< partition
=
bimap partition id <<< partition <<< fmap (bwd eassoc)

左单元：

bwd tlunit
=
bimap trivial id <<< partition <<< fmap (bwd elunit)

右单位：

bwd trunit
=
bimap id trivial <<< partition <<< fmap (bwd erunit)

定义标准过滤器函数，例如mapMaybe and filter就 oplax 幺半群函子编码而言，留给感兴趣的读者作为练习：

mapMaybe :: Filterable f => (a -> Maybe b) -> f a -> f b
mapMaybe = _

filter :: Filterable f => (a -> Bool) -> f a -> f a
filter = _

问题是这样的：是每一个Alternative Monad also Filterable?

我们可以输入俄罗斯方块来实现：

instance (Alternative f, Monad f) => Filter f
  where
  partition fab = (fab >>= either return (const empty), fab >>= either (const empty) return)

但这种实施总是合法的吗？有时合法吗（对于“有时”的某些正式定义）？证明、反例和/或非正式论证都非常有用。谢谢。

这是一个广泛支持你美好想法的论点。

第一部分：mapMaybe

我的计划是重申这个问题mapMaybe，希望这样做能让我们进入更熟悉的领域。为此，我将使用一些Either-杂耍实用功能：

maybeToRight :: a -> Maybe b -> Either a b
rightToMaybe :: Either a b -> Maybe b
leftToMaybe :: Either a b -> Maybe a
flipEither :: Either a b -> Either b a

（我取了前三个名字relude https://hackage.haskell.org/package/relude-0.6.0.0/docs/Relude-Monad-Either.html，第四个来自errors https://hackage.haskell.org/package/errors-2.3.0/docs/Data-EitherR.html#v:flipEither。顺便一提，errors offers maybeToRight and rightToMaybe as note and hush分别在Control.Error.Util https://hackage.haskell.org/package/errors-2.3.0/docs/Control-Error-Util.html.)

正如你所指出的，mapMaybe可以定义为partition:

mapMaybe :: Filterable f => (a -> Maybe b) -> f a -> f b
mapMaybe f = snd . partition . fmap (maybeToRight () . f)

至关重要的是，我们也可以反过来：

partition :: Filterable f => f (Either a b) -> (f a, f b)
partition = mapMaybe leftToMaybe &&& mapMaybe rightToMaybe

这表明根据以下方面重新制定法律是有意义的mapMaybe。有了身份法，这样做给了我们一个很好的借口来完全忘记trivial:

-- Left and right unit
mapMaybe rightToMaybe . fmap (bwd elunit) = id  -- [I]
mapMaybe leftToMaybe . fmap (bwd erunit) = id   -- [II]

至于关联性，我们可以使用rightToMaybe and leftToMaybe将定律分解为三个方程，每个方程对应我们从连续划分中得到的每个分量：

-- Associativity
mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]
mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]
mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe leftToMaybe    -- [V]

参数化意味着mapMaybe是不可知论的Either我们在这里处理的价值观。既然如此，我们可以使用我们的小武器库Either同构来打乱事物并表明 [I] 等价于 [II]，而 [III] 等价于 [V]。我们现在只剩下三个方程：

mapMaybe rightToMaybe . fmap (bwd elunit) = id       -- [I]
mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]
mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]

参数化让我们能够吞下fmap in [I]:

mapMaybe (rightToMaybe . bwd elunit) = id

然而，这根本就是……

mapMaybe Just = id

...这相当于守恒定律/恒等律枯萎的's Filterable https://hackage.haskell.org/package/witherable-class-0/docs/Data-Witherable-Class.html:

mapMaybe (Just . f) = fmap f

That Filterable还有一个组合律：

-- The (<=<) is from the Maybe monad.
mapMaybe g . mapMaybe f = mapMaybe (g <=< f)

我们是否也可以从我们的法律中推导出这一点？让我们从[III]开始，再次让参数化发挥作用。这个比较棘手，所以我将其完整写下来：

mapMaybe rightToMaybe . fmap (bwd eassoc)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe  -- [III]

-- f :: a -> Maybe b; g :: b -> Maybe c
-- Precomposing fmap (right (maybeToRight () . g) . maybeToRight () . f)
-- on both sides:
mapMaybe rightToMaybe . fmap (bwd eassoc)
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe 
      . fmap (right (maybeToRight () . g) . maybeToRight () . f)

mapMaybe rightToMaybe . mapMaybe rightToMaybe 
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)  -- RHS
mapMaybe rightToMaybe . fmap (maybeToRight () . g)
  . mapMaybe rightToMaybe . fmap (maybeToRight () . f)
mapMaybe (rightToMaybe . maybeToRight () . g)
 . mapMaybe (rightToMaybe . maybeToRight () . f)
mapMaybe g . mapMaybe f

mapMaybe rightToMaybe . fmap (bwd eassoc)
  . fmap (right (maybeToRight () . g) . maybeToRight () . f)  -- LHS
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight () . g) . maybeToRight () . f)
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight ()) . maybeToRight () . fmap @Maybe g . f)
-- join @Maybe
--     = rightToMaybe . bwd eassoc . right (maybeToRight ()) . maybeToRight ()
mapMaybe (join @Maybe . fmap @Maybe g . f)
mapMaybe (g <=< f)  -- mapMaybe (g <=< f) = mapMaybe g . mapMaybe f

在另一个方向：

mapMaybe (g <=< f) = mapMaybe g . mapMaybe f
-- f = rightToMaybe; g = rightToMaybe
mapMaybe (rightToMaybe <=< rightToMaybe)
    = mapMaybe rightToMaybe . mapMaybe rightToMaybe
mapMaybe (rightToMaybe <=< rightToMaybe)  -- LHS
mapMaybe (join @Maybe . fmap @Maybe rightToMaybe . rightToMaybe)
-- join @Maybe
--     = rightToMaybe . bwd eassoc . right (maybeToRight ()) . maybeToRight ()
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight ()) . maybeToRight ()
      . fmap @Maybe rightToMaybe . rightToMaybe)
mapMaybe (rightToMaybe . bwd eassoc 
    . right (maybeToRight () . rightToMaybe) 
      . maybeToRight () . rightToMaybe)
mapMaybe (rightToMaybe . bwd eassoc)  -- See note below.
mapMaybe rightToMaybe . fmap (bwd eassoc)
-- mapMaybe rightToMaybe . fmap (bwd eassoc)
--     = mapMaybe rightToMaybe . mapMaybe rightToMaybe

（注：虽然maybeToRight () . rightToMaybe :: Either a b -> Either () b is not id，在上面的推导中，无论如何，左值都会被丢弃，因此将其删除是公平的，就好像它是一样id.)

因此[III]等价于复合律枯萎的's Filterable.

此时，我们可以用组合律来处理[IV]：

mapMaybe rightToMaybe . mapMaybe leftToMaybe . fmap (bwd eassoc)
    = mapMaybe leftToMaybe . mapMaybe rightToMaybe   -- [IV]
mapMaybe (rightToMaybe <=< leftToMaybe) . fmap (bwd eassoc)
    = mapMaybe (letfToMaybe <=< rightToMaybe)
mapMaybe (rightToMaybe <=< leftToMaybe . bwd eassoc)
    = mapMaybe (letfToMaybe <=< rightToMaybe)
-- Sufficient condition:
rightToMaybe <=< leftToMaybe . bwd eassoc = letfToMaybe <=< rightToMaybe
-- The condition holds, as can be directly verified by substiuting the definitions.

这足以表明你的课程达到了一个完善的公式Filterable，这是一个非常好的结果。以下是法律的回顾：

mapMaybe Just = id                            -- Identity
mapMaybe g . mapMaybe f = mapMaybe (g <=< f)  -- Composition

As the 枯萎的文档注释，这些是函子的函子定律克莱斯利也许 to Hask.

第二部分：Alternative 和 Monad

现在我们可以解决您的实际问题，即关于替代单子的问题。您提议的实施partition was:

partitionAM :: (Alternative f, Monad f) => f (Either a b) -> (f a, f b)
partitionAM
    = (either return (const empty) =<<) &&& (either (const empty) return =<<)

按照我的更广泛的计划，我将转向mapMaybe推介会：

mapMaybe f
snd . partition . fmap (maybeToRight () . f)
snd . (either return (const empty) =<<) &&& (either (const empty) return =<<)
    . fmap (maybeToRight () . f)
(either (const empty) return =<<) . fmap (maybeToRight () . f)
(either (const empty) return . maybeToRight . f =<<)
(maybe empty return . f =<<)

所以我们可以定义：

mapMaybeAM :: (Alternative f, Monad f) => (a -> Maybe b) -> f a -> f b
mapMaybeAM f u = maybe empty return . f =<< u

或者，用无点拼写：

mapMaybeAM = (=<<) . (maybe empty return .)

上面几段我注意到Filterable法律规定mapMaybe是函子的态射映射克莱斯利也许 to Hask。由于函子的复合是一个函子，并且(=<<)是函子的态射映射克莱斯利夫 to Hask, (maybe empty return .)是函子的态射映射克莱斯利也许 to 克莱斯利夫足以mapMaybeAM是合法的。相关函子定律是：

maybe empty return . Just = return  -- Identity
maybe empty return . g <=< maybe empty return . f
    = maybe empty return . (g <=< f)  -- Composition

该恒等定律成立，所以让我们关注组合定律：

maybe empty return . g <=< maybe empty return . f
    = maybe empty return . (g <=< f)
maybe empty return . g =<< maybe empty return (f a)
    = maybe empty return (g =<< f a)
-- Case 1: f a = Nothing
maybe empty return . g =<< maybe empty return Nothing
    = maybe empty return (g =<< Nothing)
maybe empty return . g =<< empty = maybe empty return Nothing
maybe empty return . g =<< empty = empty  -- To be continued.
-- Case 2: f a = Just b
maybe empty return . g =<< maybe empty return (Just b)
    = maybe empty return (g =<< Just b)
maybe empty return . g =<< return b = maybe empty return (g b)
maybe empty return (g b) = maybe empty return (g b)  -- OK.

所以，mapMaybeAM是合法的，当且仅当maybe empty return . g =<< empty = empty对于任何g。现在，如果empty定义为absurd <$> nil ()，正如您在这里所做的那样，我们可以证明f =<< empty = empty对于任何f:

f =<< empty = empty
f =<< empty  -- LHS
f =<< absurd <$> nil ()
f . absurd =<< nil ()
-- By parametricity, f . absurd = absurd, for any f.
absurd =<< nil ()
return . absurd =<< nil ()
absurd <$> nil ()
empty  -- LHS = RHS

直观地讲，如果empty确实是空的（考虑到我们在这里使用的定义，它一定是空的），因此不会有任何值f应用于，等等f =<< empty不会产生任何结果，除了empty.

这里的另一种方法是研究Alternative and Monad类。碰巧，有一个替代 monad 的类：MonadPlus https://downloads.haskell.org/ghc/8.8.3/docs/html/libraries/base-4.13.0.0/Control-Monad.html#t:MonadPlus。据此，重新设计了mapMaybe可能看起来像这样：

-- Lawful iff, for any f, mzero >>= maybe empty mzero . f = mzero
mmapMaybe :: MonadPlus m => (a -> Maybe b) -> m a -> m b
mmapMaybe f m = m >>= maybe mzero return . f

虽然有不同意见 https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus#Other_suggested_laws哪一套法律最适合MonadPlus，似乎没有人反对的法律之一是……

mzero >>= f = mzero  -- Left zero

...这正是empty我们在上面讨论了几段。的合法性mmapMaybe紧接着左零定律。

（顺便，Control.Monad提供mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a https://downloads.haskell.org/ghc/8.8.3/docs/html/libraries/base-4.13.0.0/Control-Monad.html#v:mfilter，它匹配filter我们可以定义使用mmapMaybe.)

总之：

但这种实施总是合法的吗？有时合法吗（对于“有时”的某些正式定义）？

是的，实施是合法的。这个结论取决于empty确实是空的，因为它应该是空的，或者在左零之后的相关替代单子上MonadPlus法，归结起来几乎是同一件事。

值得强调的是Filterable不包含在MonadPlus，我们可以通过以下反例来说明：

• ZipList：可过滤，但不是单子。这Filterable实例与列表的实例相同，尽管Alternative一个是不同的。

• Map：可过滤，但既不是单子也不是应用程序。实际上，Map甚至无法应用，因为没有合理的实施pure。然而它确实有自己的empty.

• MaybeT f: 虽然其Monad and Alternative实例需要f成为一个单子，并且是一个孤立的empty定义至少需要Applicative, the Filterable实例只需要Functor f（如果你滑倒任何东西都变得可以过滤Maybe层到其中）。

第三部分：空

说到这里，人们可能仍然想知道它的作用有多大。empty, or nil，真正发挥作用的是Filterable。它不是一个类方法，但大多数实例似乎都有一个合理的版本。

我们可以确定的一件事是，如果可过滤类型有任何居民，那么至少其中一个将是一个空结构，因为我们总是可以取出任何居民并过滤掉所有内容：

chop :: Filterable f => f a -> f Void
chop = mapMaybe (const Nothing)

的存在chop，虽然并不意味着会有single nil空值，或者chop总是会给出相同的结果。例如，考虑一下，MaybeT IO, whose Filterable实例可能被认为是审查结果的一种方式IO计算。该实例是完全合法的，尽管chop可以产生不同的MaybeT IO Void带有任意值的值IO影响。

最后一点，你有提到 https://stackoverflow.com/questions/60732274/is-every-alternative-monad-filterable/60796049#comment107679715_60796049使用强幺半群函子的可能性，以便Alternative and Filterable通过制作链接union/partition and nil/trivial同构。拥有union and partition因为互逆是可以想象的，但相当有限，因为union . partition丢弃有关大部分实例的元素排列的一些信息。至于另一个同构，trivial . nil是微不足道的，但是nil . trivial有趣的是它意味着只有一个f Void价值，占有相当大份额的东西Filterable实例。碰巧有一个MonadPlus此条件的版本。如果我们要求的话，对于任何u...

absurd <$> chop u = mzero

...然后替换mmapMaybe从第二部分，我们得到：

absurd <$> chop u = mzero
absurd <$> mmapMaybe (const Nothing) u = mzero
mmapMaybe (fmap absurd . const Nothing) u = mzero
mmapMaybe (const Nothing) u = mzero
u >>= maybe mzero return . const Nothing = mzero
u >>= const mzero = mzero
u >> mzero = mzero

这个性质被称为右零定律MonadPlus， 尽管有充分的理由质疑其作为法律的地位 https://winterkoninkje.dreamwidth.org/90905.html属于那个特定的班级。