8

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

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为从张量下的EitherHask 到张量下的 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)

定义标准的 filter-y 函数，例如mapMaybe并filter根据 oplax monoidal functor encoding 留给感兴趣的读者作为练习：

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)

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

4

1 回答 1

3

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

第一部分：mapMaybe

我在这里的计划是重述这个问题mapMaybe，希望这样做能让我们更熟悉。为此，我将使用一些Either-juggling 实用程序函数：

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中取了前三个名字，从errors中取了第四个名字。顺便说一下，errors分别提供maybeToRight和rightToMaybeasnote和hushin 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]

至于关联性，我们可以使用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 '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

正如枯萎的文档所指出的，这些是从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定律说这mapMaybe是从Kleisli Maybe到Hask的函子的态射映射。由于函子的组合是函子，并且(=<<)是从Kleisli f到Hask的(maybe empty return .)函子的态射映射，因此作为从Kleisli Maybe到Kleisli 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。

这里的另一种方法是研究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和联系起来。具有和作为互逆是可以想象的，但相当有限，因为它丢弃了关于大部分实例的元素排列的一些信息。至于另一个同构，是微不足道的，但有趣的是它意味着只有一个值，适用于相当大份额的实例。碰巧有这种情况的一个版本。如果我们要求，对于任何...Filterableunionpartitionniltrivialunionpartitionunion . 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，尽管有充分的理由质疑其作为该特定类别的定律的地位。

于 2020-03-22T04:50:18.170 回答