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

Is every Alternative Monad Filterable?

集的类别既是笛卡尔幺半群又是笛卡尔幺半群。下面列出了这两个幺半群结构的规范同构类型:

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

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)

根据 oplax 幺半群函子编码定义标准 filter-y 函数,如 mapMaybefilter,留给感兴趣的人作为练习 reader:

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)

但是这种实施总是合法的吗?它有时是合法的吗(对于 "sometimes" 的一些正式定义)?证明、反例、and/or 非正式论证都会非常有用。谢谢。

这里有一个广泛支持你美丽想法的论点。

第一部分: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, and the fourth from errors. By the way, errors offers maybeToRight and rightToMaybe as note and hush respectively, in Control.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]

至于结合律,我们可以使用 rightToMaybeleftToMaybe 将定律拆分为三个方程,一个对应于我们从连续分区中得到的每个分量:

-- 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]

参数化允许我们吞下[I]中的fmap:

mapMaybe (rightToMaybe . bwd elunit) = id

然而,这只是...

mapMaybe Just = id

... 相当于 witherable's Filterable 中的 conservation/identity 法则:

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 () b 不是 id,但在上面的推导中,左边的值无论如何都会被丢弃,因此将其删除是公平的,就好像它是 id.)

因此[III]等价于witherableFilterable.

的组合规律

此时,我们可以使用组合律来处理[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.

这足以表明您的 class 相当于 Filterable 的完善公式,这是一个非常好的结果。以下是法律的概述:

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

正如 witherable 文档所指出的,这些是从 Kleisli MaybeHask[= 的函子的函子定律255=].

第二部分:Alternative 和 Monad

现在我们可以解决您的实际问题,即关于替代 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定律说mapMaybe是函子从Kleisli Maybe到[=241的态射映射=]哈斯克。由于函子的合成是函子,而(=<<)是函子从Kleisli fHask的态射映射,(maybe empty return .) 是从 Kleisli MaybeKleisli f 的函子的态射映射足以使 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.

什么也做不了

此处的另一种方法是研究 AlternativeMonad class 之间的交互。碰巧的是,有一个 class 用于替代 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

虽然 varying opinions 哪一套法律最适合 MonadPlus,但似乎没有人反对的法律之一是...

mzero >>= f = mzero  -- Left zero

... 这正是我们在上面讨论的 empty 的 属性。 mmapMaybe 的合法性紧随左零定律。

(顺便说一下,Control.Monad provides mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a,它匹配我们可以使用 mmapMaybe 定义的 filter。)

总结:

But is this implementation always lawful? Is it sometimes lawful (for some formal definition of "sometimes")?

是的,执行是合法的。这个结论取决于 empty 确实是空的,它应该是空的,或者取决于遵循左零 MonadPlus 法则的相关替代单子,这归结为几乎相同的事情。

需要强调的是,Filterable不属于MonadPlus,我们可以用下面的反例来说明:

  • ZipList:可过滤,但不是 monad。 Filterable 实例与列表实例相同,尽管 Alternative 实例不同。

  • Map:可过滤,但既不是 monad 也不是 applicative。事实上,Map 甚至不能应用,因为 pure 没有合理的实现。但是,它确实有自己的 empty.

  • MaybeT f:虽然它的 MonadAlternative 实例需要 f 是一个单子,并且是一个孤立的 empty 定义至少需要 ApplicativeFilterable 实例只需要 Functor f(如果你将 Maybe 层滑入其中,任何东西都可以过滤)。

第三部分:空

在这一点上,人们可能仍然想知道 emptynilFilterable 中究竟扮演了多大的角色。它不是 class 方法,但大多数实例似乎都有它的合理版本。

我们可以确定的一件事是,如果可过滤类型有任何居民,至少其中一个将是空结构,因为我们总是可以取出任何居民并过滤掉所有东西:

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

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

最后一点,您有 使用强幺半群仿函数的可能性,因此 AlternativeFilterable 通过 union/partitionnil/trivial 同构。将 unionpartition 作为互逆是可以想象的,但相当有限,因为 union . partition 丢弃了一些关于大量实例的元素排列的信息。至于另一个同构,trivial . nil 是微不足道的,但是 nil . trivial 很有趣,因为它意味着只有一个 f Void 值,这个值占 [=53= 的相当大一部分] 实例。碰巧这个条件有一个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 的右零定律,尽管 there are good reasons to contest its status as a law 那个特定的 class.