每个替代的 Monad 都是可过滤的吗？

Question

集合的范畴既是笛卡尔幺半群又是余笛卡尔幺半群。下面列出了见证这两个幺半群结构的典型同构的类型：

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为从Either张量下的 Hask 到张量下的 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函子定义为从张量下的 Hask 到张量下的Hask 的 oplax 幺半群函子：Either(,)

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)

像定义标准过滤-Y功能mapMaybe和filter在方面oplax monoidal函子了编码作为练习留给感兴趣的读者：

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

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

---

问题是这样的：是每个Alternative Monad也Filterable？

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

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

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

Answer 1

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

第一部分：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中获取了前三个名称，从error中获取了第四个名称。顺便说一下，errors在 中分别提供了maybeToRight和rightToMaybeasnote和。）hushControl.Error.Util

正如您所指出的，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和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[I] 中的内容：

mapMaybe (rightToMaybe . bwd elunit) = id

然而，这根本就是……

mapMaybe Just = id

...这相当于witherable的守恒定律/恒等律Filterable：

mapMaybe (Just . f) = fmap f

这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 () bis not id，但在上面的推导中，左值无论如何都会被丢弃，因此将其删除就好像它是一样id。）

因此[III] 等价于witherable的合成法则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

正如witherable文档所指出的，这些是从Kleisli Maybe到Hask的函子的函子法则。

第二部分：Alternative 和 Monad

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

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定律说这是函子从Kleisli Maybe到HaskmapMaybe的态射映射。由于函子的复合是一个函子，并且是函子从Kleisli f到Hask的态射映射，因此函子从Kleisli Maybe到Kleisli f的态射映射就足够合法了。相关函子定律是：(=<<)(maybe empty return .)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 = emptygemptyabsurd <$> nil ()f =<< empty = emptyf

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

直观上， ifempty确实为空（考虑到我们在这里使用的定义，它一定是空的），不会有 的值可f应用于，因此f =<< empty除了 之外不会产生任何结果empty。

这里的另一种方法是研究Alternative和Monad类的交互。碰巧，有一个替代 monad 的类：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

虽然对于哪一套法律最适合有不同的意见MonadPlus，但似乎没有人反对的法律之一是......

mzero >>= f = mzero  -- Left zero

empty...这正是我们上面几段讨论的属性。的合法性mmapMaybe立即遵循左零定律。

（顺便说一下，Control.Monad提供了mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a，它与filter我们可以使用定义的匹配mmapMaybe。）

总之：

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

是的，实施是合法的。这个结论取决于empty确实是空的，因为它应该是空的，或者取决于遵循左零定律的相关替代单子MonadPlus，这可以归结为几乎相同的事情。

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

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

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

• MaybeT f：虽然它Monad和Alternative实例需要f是一个单子，并且一个独立的empty定义至少需要Applicative，Filterable但实例只需要（如果你在其中Functor f插入一个层，任何东西都变得可过滤）。Maybe

第三部分：空

empty在这一点上，人们可能仍然想知道在其中到底nil扮演了多大的角色Filterable。它不是一个类方法，但大多数实例似乎都有一个合理的版本。

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

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

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

最后一点，您提到了使用强幺半群函子的可能性，以便Alternative和通过制作/和/同构Filterable来链接。具有和作为互逆是可以想象的，但相当有限，因为它丢弃了有关大部分实例的元素排列的一些信息。至于另一个同构，虽然微不足道，但很有趣，因为它意味着只有一个值，适用于相当大的实例份额。碰巧这种情况有一个版本。如果我们要求的话，对于任何...unionpartitionniltrivialunionpartitionunion . partitiontrivial . nilnil . trivialf VoidFilterableMonadPlusu

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，尽管有充分的理由质疑其作为该特定类别定律的地位。