每个替代Monad都可以过滤吗? [英] Is every Alternative Monad Filterable?

问题描述

集合的类别既是笛卡尔单曲面的又是笛卡尔笛卡尔的.下面列出了见证这两个单调结构的规范同构的类型:

The category of sets is both cartesian monoidal and cocartesian monoidal. The types of the canonical isomorphisms witnessing these two monoidal structures are listed below:

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的松散单曲面函子(且不再存在):

---

For the purposes of this question I define Alternative to be a lax monoidal functor from Hask under the Either tensor to Hask under the (,) tensor (and no more):

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

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

法律只是那些松散的单曲面仿函数的法律.

The laws are just those for a lax monoidal functor.

关联性:

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类型类恢复更为熟悉的操作的方法:

Here is how to recover the more familiar operations for the Alternative typeclass in terms of the coherence maps of the lax monoidal functor encoding:

(<|>) :: 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:

---

I define Filterable functors to be oplax monoidal functors from Hask under the Either tensor to Hask under the (,) 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 ()

由于其律法落后于松散的单等子函子律:

Having for its laws just backwards lax monoidal functor laws:

关联性:

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单面函子编码定义诸如mapMaybe和filter之类的标准filter-y函数，作为感兴趣的读者的练习:

Defining standard filter-y functions like mapMaybe and filter in terms of the oplax monoidal functor encoding left as an exercise to the interested 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吗?

---

The question is this: is every Alternative Monad also Filterable?

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

We can type tetris our way to an implementation:

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

但是这种实现总是合法的吗?有时合法吗(对于有时"的一些正式定义)?证明，反例和/或非正式论点都将非常有用.谢谢.

But is this implementation always lawful? Is it sometimes lawful (for some formal definition of "sometimes")? Proofs, counterexamples, and/or informal arguments would all be very useful. Thanks.

推荐答案

此处提出了一个广泛支持您美丽想法的论点.

Here goes an argument which is broadly supportive of your beautiful idea.

我的计划是按照mapMaybe重述该问题，希望这样做可以使我们更熟悉.为此，我将使用一些Either -juggling实用程序功能:

My plan here is restating the problem in terms of mapMaybe, hoping that doing so will bring us to more familiar ground. To do so, I will use a few Either-juggling utility functions:

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 ，第四个来自 Control.Error.Util .)

(I took the first three names from 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定义:

As you noted, mapMaybe can be defined in terms of partition:

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

至关重要的是，我们也可以采用其他方法:

Crucially, we can also go the other way around:

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

这表明按照mapMaybe重塑法律是很有意义的.根据身份法，这样做为我们提供了一个很好的借口，完全忘记了trivial:

This suggests it makes sense to recast your laws in terms of mapMaybe. With the identity laws, doing so gives us a great excuse to forget entirely about trivial:

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

关于关联性，我们可以使用rightToMaybe和leftToMaybe将定律分为三个方程式，一个是从连续分区中获得的每个分量:

As for associativity, we can use rightToMaybe and leftToMaybe to split the law in three equations, one for each component we get from the successive partitions:

-- 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].现在我们归结为三个方程式:

Parametricity means mapMaybe is agnostic with respect to the Either values we are dealing with here. That being so, we can use our little arsenal of Either isomorphisms to shuffle things around and show that [I] is equivalent to [II], and [III] is equivalent to [V]. We are now down to three equations:

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:

Parametricity allows us to swallow the fmap in [I]:

mapMaybe (rightToMaybe . bwd elunit) = id

但是，那只是...

mapMaybe Just = id

...等效于 可干的Filterable :

... which is equivalent to the conservation/identity law from witherable's Filterable:

mapMaybe (Just . f) = fmap f

Filterable也具有成分定律:

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

我们也可以从我们的法律中得出这一点吗?让我们从[III]开始，再一次让参数化工作.这个比较棘手，因此我将其完整记录下来:

Can we also derive this one from our laws? Let's start from [III] and, once more, have parametricity do its work. This one is trickier, so I'll write it down in full:

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.)

(Note: While maybeToRight () . rightToMaybe :: Either a b -> Either () b is not id, in the derivation above the left values will be discarded anyway, so it is fair to strike it out as if it were id.)

因此，[III]等同于可凋的Filterable的组成定律.

Thus [III] is equivalent to the composition law of witherable's Filterable.

在这一点上，我们可以使用组成定律来处理[IV]:

At this point, we can use the composition law to deal with [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公式，这是一个非常不错的结果.这是法律的回顾:

This suffices to show your class amounts to a well-established formulation of Filterable, which is a very nice result. Here is a recap of the laws:

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

正如 witherable 文档所述，这些是从 Kleisli Maybe 到 Hask 的函子的函子定律.

As the witherable docs note, these are functor laws for a functor from Kleisli Maybe to Hask.

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

Now we can tackle your actual question, which was about alternative monads. Your proposed implementation of 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演示文稿:

Following my broader plan, I will switch to the mapMaybe presentation:

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

或者，使用无意义的拼写:

Or, in a pointfree spelling:

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

在上面的几段中，我注意到Filterable律说mapMaybe是从 Kleisli Maybe 到 Hask 的函子的态射映射.由于函子的组成是函子，而(=<<)是函子从 Kleisli f 到 Hask 的态射图，(maybe empty return .)是函子的态射图从 Kleisli May 到 Kleisli f 足以使mapMaybeAM合法.相关的函子定律是:

A few paragraphs above, I noted the Filterable laws say that mapMaybe is the morphism mapping of a functor from Kleisli Maybe to Hask. Since the composition of functors is a functor, and (=<<) is the morphism mapping of a functor from Kleisli f to Hask, (maybe empty return .) being the morphism mapping of a functor from Kleisli Maybe to Kleisli f suffices for mapMaybeAM to be lawful. The relevant functor laws are:

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

此身份法成立，因此让我们关注一下构成:

This identity law holds, so let's focus on the composition one:

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是任何g的合法iff maybe empty return . g =<< empty = empty.现在，如您在此处所做的那样，如果将empty定义为absurd <$> nil ()，我们可以证明对于任何f::

Therefore, mapMaybeAM is lawful iff maybe empty return . g =<< empty = empty for any g. Now, if empty is defined as absurd <$> nil (), as you have done here, we can prove that f =<< empty = empty for any 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.

Intuitively, if empty is really empty (as it must be, given the definition we are using here), there will be no values for f to be applied to, and so f =<< empty can't result in anything but empty.

这里的另一种方法是研究Alternative和Monad类的交互.碰巧的是，有一个替代monad的类:

A different approach here would be looking into the interaction of the Alternative and Monad classes. As it happens, there is a class for alternative monads: MonadPlus. Accordingly, a restyled mapMaybe might look like this:

-- 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，似乎没人反对的法律之一是...

While there are varying opinions on which set of laws is most appropriate for MonadPlus, one of the laws no one seems to object to is...

mzero >>= f = mzero  -- Left zero

...正是我们在上面讨论的几段内容的empty属性. mmapMaybe的合法性从左零定律立即得出.

... which is precisely the property of empty we were discussing a few paragraphs above. The lawfulness of mmapMaybe follows immediately from the left zero law.

(偶然地， Control.Monad提供了mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a ，它与我们可以使用mmapMaybe定义的filter相匹配.)

(Incidentally, Control.Monad provides mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a, which matches the filter we can define using mmapMaybe.)

总结:

但是这种实现总是合法的吗?有时候合法吗(对于有时"的一些正式定义)?

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

是的，实施是合法的.该结论取决于empty是否确实为空，或者取决于遵循左零MonadPlus律的相关替代单子，其归结为几乎相同的东西.

Yes, the implementation is lawful. This conclusion hinges on the empty being indeed empty, as it should, or on the relevant alternative monad following the left zero MonadPlus law, which boils down to pretty much the same thing.

值得强调的是，MonadPlus并未包含Filterable，正如我们可以通过以下反例进行说明:

It is worth emphasising that Filterable isn't subsumed by MonadPlus, as we can illustrate with the following counterexamples:

• ZipList:可过滤，但不能过滤. Filterable实例与列表的实例相同，即使Alternative实例不同.

• ZipList: filterable, but not a monad. The Filterable instance is the same as the one for lists, even though the Alternative one is different.

Map:可过滤，但既不能使用monad也不能使用.实际上，Map甚至无法应用，因为pure没有明智的实现.但是，它确实有自己的empty.

Map: filterable, but neither a monad nor applicative. In fact, Map can't even be applicative because there is no sensible implementation of pure. It does, however, have its own empty.

MaybeT f:尽管其Monad和Alternative实例需要f为单子，而单独的empty定义将至少需要Applicative，仅Filterable实例需要Functor f(如果将Maybe层滑入其中，任何东西都可以过滤).

MaybeT f: while its Monad and Alternative instances require f to be a monad, and an isolated empty definition would need at least Applicative, the Filterable instance only requires Functor f (anything becomes filterable if you slip a Maybe layer into it).

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

At this point, one might still wonder how big of a role empty, or nil, really plays in Filterable. It is not a class method, and yet most instances appear to have a sensible version of it lying around.

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

The one thing we can be certain of is that, if the filterable type has any inhabitants at all, at least one of them will be an empty structure, because we can always take any inhabitant and filter everything out:

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

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

The existence of chop, though doesn't mean there will be a single nil empty value, or that chop will always give out the same result. Consider, for instance, MaybeT IO, whose Filterable instance might be thought of as a way to censor results of IO computations. The instance is perfectly lawful, even though chop can produce distinct MaybeT IO Void values that carry arbitrary IO effects.

最后一点，您被认为是与强单曲面函子一起工作，从而使Alternative和Filterable通过形成union/partition和nil/trivial同构而链接起来.考虑到union和partition作为互逆，对于union . partition来说，对于大部分实例来说，它们放弃了一些有关元素排列的信息，这是可以想象的，但却是相当有限的.至于其他同构，trivial . nil是微不足道的，但是nil . trivial有趣的是，它暗示只有一个f Void值，该值可容纳大量的Filterable实例.碰巧有这种情况的MonadPlus版本.如果我们要求，对于任何u ...

On a final note, you have alluded to the possibility of working with strong monoidal functors, so that Alternative and Filterable are linked by making union/partition and nil/trivial isomorphisms. Having union and partition as mutual inverses is conceivable but fairly limiting, given that union . partition discards some information about the arrangement of the elements for a large share of instances. As for the other isomorphism, trivial . nil is trivial, but nil . trivial is interesting in that it implies there is just a single f Void value, something that holds for a sizeable share of Filterable instances. It happens that there is a MonadPlus version of this condition. If we demand that, for any u...

absurd <$> chop u = mzero

...然后替换第二部分中的mmapMaybe，我们得到:

... and then substitute the mmapMaybe from part two, we get:

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的右零定律，尽管有充分的理由进行竞争它作为该特定类别的法律的地位.

This property is known as the right zero law of MonadPlus, though there are good reasons to contest its status as a law of that particular class.

这篇关于每个替代Monad都可以过滤吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！