每个替代的Monad是否可以过滤？

问题描述 投票：8回答：1

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

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单面函子编码来定义像mapMaybe和filter这样的标准filter-y函数：

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)

但是此实现始终合法吗？有时合法吗（对于“有时”的一些正式定义）？证明，反例和/或非正式论点都将非常有用。谢谢。

haskell filter monads functor category-theory
1个回答
0
投票

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

第一部分：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取了第四个名字。顺便说一下，错误分别在maybeToRight和rightToMaybe中提供了note和hush。 Control.Error.Util。）

如上所述，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 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同构的少量武库来洗牌，证明[I]等于[II]，[III]等于[V]。现在我们归结为三个方程：

Either

参数可让我们吞下[I]中的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

但是，那只是...

mapMaybe (rightToMaybe . bwd elunit) = id

...等价于mapMaybe Just = id 中的守恒/身份定律：

witherable's Filterable

Filterable也有成分定律：

mapMaybe (Just . f) = fmap f

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

Filterable

朝另一个方向：

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

（（注：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。）

因此，[III]等效于可凋]]的id的组成定律。

在这一点上，我们可以使用合成法来处理[IV]：

id
这足以表明您的课程相当于Filterable的既定公式，这是一个非常不错的结果。以下是法律的摘要：
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.

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

第二部分：Alternate和Monad

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

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

按照更广泛的计划，我将切换到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 .)
是函子从Kleisli Maybe
到Hask的态射映射。由于函子的组成是函子，并且Filterable是从Kleisli f到Hask的函子的态射映射，mapMaybe是从Kleisli f]的函子的态射映射> [[Kleisli Maybe就足以使(=<<)合法。相关的函子律是：(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  -- Inconclusive.
-- 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。因此，重新设置样式的Alternative可能如下所示：
Monad
虽然有MonadPlus的一组法律最适合MonadPlus，但似乎没有人反对的为数不多的法律之一是：
mapMaybe
-- Lawful iff, for any g, empty >>= maybe empty return . g
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
匹配。）

摘要：

但是此实现始终合法吗？有时合法吗（对于“有时”的一些正式定义）？

只要相关的替代单子遵循左零mmapMaybe法则（该实现是合法的，我想这几乎涵盖了一个人可能最终要处理的所有替代单子）。值得强调的是Control.Monad provides mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a不包含在Control.Monad中，因为肯定有一些不是monad的可过滤对象，例如mfilter :: MonadPlus m => (a -> Bool) -> m a -> m a和filter（后者甚至不是mmapMaybe，尽管它确实有自己的MonadPlus）。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.