Jos*_*ica 8 haskell traversable
我记得在某处读到过这样的类型不能是Traversable:
data Bar a = Bar a deriving(Show)
instance Functor Bar where
fmap f (Bar x) = Bar (f x)
instance Foldable Bar where
foldMap f (Bar x) = f x <> f x
Run Code Online (Sandbox Code Playgroud)
我记得的一点解释是,为了foldMap = foldMapDefault保持,Traversable实例必须多次访问其元素,这是合法实例无法做到的。但是,我不记得为什么合法实例不能这样做。考虑这个:
instance Traversable Bar where
sequenceA (Bar x) = Bar <$ x <*> x
Run Code Online (Sandbox Code Playgroud)
乍一看还不错。这样做有什么违法?
我仍然没有解释为什么Traversables 通常不能多次访问它们的元素,但我确实弄清楚了为什么我的问题中的特定实例是非法的:
ATraversable具有三个定律:自然性、同一性和复合性。fmap = fmapDefault和也应该如此foldMap = foldMapDefault。自然是自由的参数化。对于有Traversable问题的身份,fmap = fmapDefault和foldMap = foldMapDefault都是微不足道的验证。因此,失败的必定是合成法则。我开始操纵sequenceA它的版本并将东西插入其中,最后得到了这个:
(\y z -> Bar <$ y <*> z) <$> x <*> x = (\y z -> Bar <$ z <*> z) <$> x <*> x
Run Code Online (Sandbox Code Playgroud)
现在很清楚如何找到反例了。首先,我们需要找到一个y和z这样的Bar <$ y <*> z和Bar <$ z <*> z是不同的。由于y不用于其内在价值,因此它必须引起某种效果。通过检查,y = Nothing并且z = Just ()将导致在第一个是Nothing,第二个之中Just (Bar ())。
接下来,我们需要找到一个x这样的,第一次使用xwill 是 our y,Nothing第二次使用xwill 是我们的z, Just ()。我们可以State为此使用,其中初始状态是Nothing,并且x是get <* put (Just ())。
现在我们认为我们有一个完整的反例,所以让我们验证它。原来的定律是sequenceA . fmap Compose = Compose . fmap sequenceA . sequenceA,所以让我们把它的每一边放在它自己的变量中:
import Data.Functor.Compose
lhs = sequenceA . fmap Compose
rhs = Compose . fmap sequenceA . sequenceA
Run Code Online (Sandbox Code Playgroud)
并存储我们的x:
import Control.Monad.State
x = get <* put (Just ())
Run Code Online (Sandbox Code Playgroud)
最后,把它们放在一起:
?> evalState (getCompose $ lhs $ Bar x) Nothing
Nothing
?> evalState (getCompose $ rhs $ Bar x) Nothing
Just (Bar ())
Run Code Online (Sandbox Code Playgroud)
我们的反例有效!如果法律成立,lhs并且rhs将是等效的,但它们显然不是,因为将一个转换为另一个会产生不同的结果。
有一些合理的有利位置可以解决这个问题。我在这里的策略虽然可能有点粗糙,但效果很好,同时说明了关键思想,没有太多技术复杂性。
\n这个答案有两个部分。第一部分介绍了所选的观点和主要结论,如果读者时间有限,可以独立阅读。第二部分对此进行了扩展,提供了详细的理由。最后,有一个简明的列表,列出了国家允许和禁止的事情Traversable。
答案有点长,所以这里有一个部分标题列表,可以使用 Ctrl+F 跳过:
\n第一部分
\n第二部分
\n事实上,有人可能会反对这个答案对于这种格式来说太长了。在我的辩护中,我注意到父问题在有关重复效果的部分中得到了解决,其他所有内容要么证明了直接答案的合理性,要么与上下文相关。
\n最终,这一切都归结为我所说的形状和内容分解。用最简单的术语来说,这意味着Traversable可以通过这样的类进行编码:
class (Functor t, Foldable t) => Fillable t where\n fill :: t () -> [a] -> t a\nRun Code Online (Sandbox Code Playgroud)\nfill采用t函数形状(我们在这里使用t ()值表示),并用从列表中提取的内容填充它[a]。我们可以信赖Functor并Foldable给我们一个另一个方向的转换:
detach :: (Functor t, Foldable t) => t a -> (t (), [a])\ndetach = (() <$) &&& toList\nRun Code Online (Sandbox Code Playgroud)\n有了fill和detach,我们就可以sequenceA具体实施了sequenceA来实现:分离,对列表进行排序,然后填充:
sequenceFill :: (Fillable t, Applicative f) => t (f a) -> f (t a)\nsequenceFill = uncurry (fmap . fill) . second (sequenceList) . detach\n\n-- The usual sequenceA for lists.\nsequenceList :: Applicative f => [f a] -> f [a]\nsequenceList = foldr (liftA2 (:)) (pure [])\nRun Code Online (Sandbox Code Playgroud)\n也可以用fill以下方式来定义,虽然有点尴尬:Traversable定义,虽然有点尴尬:
-- Partial, handle with care.\nfillTr :: Traversable t => t () -> [a] -> t a\nfillTr = evalState . traverse (const pop)\n where\n pop = state (\\(a : as) -> (a, as))\nRun Code Online (Sandbox Code Playgroud)\n(有关此方法的现有技术,请参阅此答案。)
\n就这方面而言Fillable,Traversable法律是这么说的fill,而且detach 几乎见证了同构的两个方向:
fill必须是左逆detach:
uncurry fill . detach = id\nRun Code Online (Sandbox Code Playgroud)\n这相当于恒等律Traversable。
detach必须表现为左逆,fill只要fill(否则情况无望):
-- Precondition: length (toList sh) = length as\n detach . uncurry fill $ (sh, as) = (sh, as)\nRun Code Online (Sandbox Code Playgroud)\n该性质对应于组合定律。事实上,它本身比复合定律更强。然而,如果我们假设恒等律,那么它在本质上就等同于复合律。既然如此,可以将这些属性作为Traversable,除非您想单独研究组合定律。(在我们更仔细地研究组合定律之后,答案的第二部分将更详细地解释这种近似等价性。)
这一切与你的问题有什么关系?假设我们想要定义一个在不改变可遍历形状的情况下复制效果的遍历(因为改变它会公然违反恒等律)。现在,假设我们sequenceA实际上是sequenceFill,如上面所定义的,我们有哪些选项?由于sequenceFill搭载sequenceList,已知它只会访问每个元素一次,因此我们唯一的希望是依赖一个伴生Foldable实例toList,使得detach,因此 生成一个包含重复元素的列表。Fillable在这种情况下我们可以让法律成立吗?
第一定律问题不大。原则上,我们总是可以定义,fill以便它撤消重复,丢弃 引入的元素的额外副本detach。
然而,如果我们进行重复数据删除fill,第二定律就注定失败。通过参数化,fill无法区分列表与detach我们可能提供给它的任何其他列表引入的重复项,因此detach . uncurry fill总是会用其他元素的重复项替换某些元素。
既然如此,traverseFill复制效果的a只能由非法的产生Fillable。由于Fillable法律与法律是等价的Traversable,因此我们得出结论,法律Traversable不能复制效果。
(顺便说一句,上面讨论的效果重复场景适用于您的Bar类型:它不符合第二Fillable定律,因此它也不符合Traversable合成定律,如您的反例所示。)
我非常喜欢的一篇涵盖这个问题及其相关问题的论文是 Bird 等人的Understanding Idiomatic Traversals Backwards and Forwards (2013)。尽管一开始看起来可能不是这样,但它的方法与我在这里展示的密切相关。detach特别是,它的“表示定理”与这里探讨的/关系本质上是相同的fill,主要区别在于论文中的定义更严格,无需大惊小怪。fill在给出错误列表时需要大惊小怪应该做什么长度。
尽管我不会尝试提出伯德等人的完整论点。论文中,在这个答案的上下文中值得注意的是,其对上述表示定理的证明如何依赖于自由应用函子的表述。我们可以稍微改变一下这个想法,以从免费的角度Traversable获得额外的展示ApControl.Applicative.Free:
-- Adapted from Control.Applicative.Free.\n\ndata Ap f a where\n Pure :: a -> Ap f a\n Ap :: f a -> Ap f (a -> b) -> Ap f b\n\ninstance Applicative (Ap f) where\n pure = Pure\n Pure f <*> y = fmap f y\n Ap x y <*> z = Ap x (flip <$> y <*> z)\n\nliftAp :: f a -> Ap f a\nliftAp x = Ap x (Pure id)\n\nretractAp :: Applicative f => Ap f a -> f a\nretractAp (Pure a) = pure a\nretractAp (Ap x y) = x <**> retractAp y\nRun Code Online (Sandbox Code Playgroud)\n\nclass (Functor t, Foldable t) => Batchable t where\n toAp :: t (f a) -> Ap f (t a)\n\nsequenceBatch :: (Batchable t, Applicative f) => t (f a) -> f (t a)\nsequenceBatch = retractAp . toAp\n\ntoApTr :: Traversable t => t (f a) -> Ap f (t a)\ntoApTr = traverse liftAp\nRun Code Online (Sandbox Code Playgroud)\n我非常确定以下是适当的法律,尽管可能值得仔细检查:
\nretractAp . toAp . fmap Identity . runIdentity = id\ntoAp . fmap Identity . runIdentity . retractAp = id\nRun Code Online (Sandbox Code Playgroud)\ndetach尽管这看起来与我们一开始的简陋和组合相去甚远fill,但它最终只是同一想法的更精确的编码。值可以是包装在 中的Ap f (t a)单个结构,也可以是由适当数量的函数限制的零个或多个值(构造函数)的序列,该函数接受与 s一样多的s 并产生一个t aPuref aApaf at a。就我们对形状和内容分解的初步尝试而言,我们有:
f a值中的 s对应Ap于内容列表;
该函数(如果有)编码在重新组装可遍历结构时要使用哪种形状,以及如何填充它。在类型级别巧妙地避免了形状列表不匹配问题,静态地保证函数将具有正确的数量;
\n至于效果,retractAp以明显的方式发挥着将它们组合起来的作用,就像sequenceList在 中所做的那样sequenceFill。
(第一部分结束。)
\n正如所承诺的,第二部分将首先证明这Fillable确实是Traversable. 接下来,我将使用定义的调整版本,这些版本更容易用笔和纸操作:
-- Making the tuple shuffling implicit. It would have been fine to use\n-- the derived Foldable and Traversable. I will refrain from that here\n-- only for the sake of explicitness. \nnewtype Decomp t a = Decomp { getDecomp :: (t (), [a]) }\n deriving Functor\n\nderiving instance (Show a, Show (t ())) => Show (Decomp t a)\n\ndetach\' :: (Functor t, Foldable t) => t a -> Decomp t a\ndetach\' = Decomp . detach\n\nfill\' :: Fillable t => Decomp t a -> t a\nfill\' = uncurry fill . getDecomp\n\n-- Sequence the list, then shift the shape into the applicative layer.\n-- Also a lawful sequenceA (amounts to Compose ((,) (t ())) []).\nsequenceList\' :: Applicative f => Decomp t (f a) -> f (Decomp t a)\nsequenceList\'\n = fmap Decomp . uncurry (map . (,)) . second sequenceList . getDecomp\n\ninstance Traversable Decomp where\n sequenceA = sequenceList\'\n\ninstance Foldable Decomp where\n foldMap = foldMapDefault\n\nsequenceFill\' :: (Fillable t, Applicative f) => t (f a) -> f (t a)\nsequenceFill\' = fmap fill\' . sequenceList\' . detach\'\nRun Code Online (Sandbox Code Playgroud)\nsequenceFill\'(顺便说一句,上面更清晰的定义提供了一个很好的机会来注意,如果我们要离开编写实际 Haskell 的限制,那么将一路携带的形状移动到类型级别并不需要太多,实际上,根据可能的形状来划分可遍历函子。据我所知,这将使我们顺利实现容器的标准依赖类型处理。我不会在这里进一步深入研究;如果您觉得就像探索一样,我衷心推荐Conor McBride(养猪工)关于该主题的答案。)
我们可以从处理身份法开始,这是一个更直接的问题:
\n-- Abbreviations:\nI = Identity\nuI = runIdentity\nC = Compose\nuC = getCompose\nRun Code Online (Sandbox Code Playgroud)\n\n-- Goal: Given the identity law...\nsequenceFill\' @_ @I . fmap I = I\n-- ... obtain detach-then-fill:\nfill\' . detach\' = id\n\nsequenceFill\' @_ @I . fmap I = I\nuI . fmap fill\' . sequenceList\' @I . detach\' . fmap I = id\n-- sequenceList is lawful (identity law):\nuI . fmap fill\' . I . fmap uI . detach\' . fmap I = id\nuI . fmap fill\' . I . detach\' . fmap uI . fmap I = id\nuI . fmap fill\' . I . detach\' = id\nuI . I . fill\' . detach\' = id\nfill\' . detach\' = id -- Goal.\nRun Code Online (Sandbox Code Playgroud)\n由于上述推导中的所有步骤都是可逆的,因此我们可以得出同构的分离-然后填充方向等效于恒等律的结论。
\n至于组合律,我们可以从使用相同的策略开始:
\n-- Goal: Given the composition law...\nsequenceFill\' @_ @(C _ _) . fmap C = C . fmap sequenceFill\' . sequenceFill\'\n-- ... obtain fill-then-detach...\ndetach\' . fill\' = id\n-- ... within the domain specified by its precondition.\n\nsequenceFill\' @_ @(C _ _) . fmap C = C . fmap sequenceFill\' . sequenceFill\'\nfmap fill\' . sequenceList\' @(C _ _) . detach\' . fmap C\n = C . fmap (fmap fill\' . sequenceList\' . detach\')\n . fmap fill\' . sequenceList\' . detach\'\n-- LHS\nfmap fill\' . sequenceList\' @(C _ _) . detach\' . fmap C\nfmap fill\' . sequenceList\' @(C _ _) . fmap C . detach\'\n-- sequenceList\' is lawful (composition law)\nfmap fill\' . C . fmap sequenceList\' . sequenceList\' . detach\'\nC . fmap (fmap fill\') . fmap sequenceList\' . sequenceList\' . detach\'\nC . fmap (fmap fill\' . sequenceList\') . sequenceList\' . toList\'\n-- RHS\nC . fmap (fmap fill\' . sequenceList\' . detach\')\n . fmap fill\' . sequenceList\' . detach\'\nC . fmap (fmap fill\' . sequenceList\') . fmap (detach\' . fill\') \n . sequenceList\' . detach\'\n-- LHS = RHS\nC . fmap (fmap fill\' . sequenceList\') . sequenceList\' . detach\'\n = C . fmap (fmap fill\' . sequenceList\') . fmap (detach\' . fill\') \n . sequenceList\' . detach\'\n-- C is injective:\nfmap (fmap fill\' . sequenceList\') . sequenceList\' . detach\'\n = fmap (fmap fill\' . sequenceList\') . fmap (detach\' . fill\')\n . sequenceList\' . detach\' -- On hold.\nRun Code Online (Sandbox Code Playgroud)\n在这一点上,我们似乎陷入了一个比detach\' . fill\' = id我们预期要发现的更弱的财产中。从好的方面来说,它有一些好处:
上述推导中的所有步骤都是可逆的,因此该性质等价于合成律。
\n填充等式两边的sequenceList\' . detach\'和fmap (fmap fill\' . sequenceList\')额外项使得 everyfill\'前面有 a detach\',而 everydetach\'后面有 a fill\'。这意味着填充然后分离定律的前提自动成立。
填充然后分离法则比该属性严格更强。既然如此,如果detach\' . fill\' = id(在前提条件等的范围内),那么这个性质以及组合律也成立。
稍后我将回顾这些观察结果,以证明我之前的主张detach\' . fill\' = id可以被视为Traversable法律。
在我们继续我们的正常日程之前,短暂休息一下。通过将组合律中的两个应用函子专门化为 ,我们可以发现一些琐事Identity。从我们停下来的地方继续:
fmap (fmap fill\' . sequenceList\') . sequenceList\' . detach\'\n = fmap (fmap fill\' . sequenceList\') . fmap (detach\' . fill\')\n . sequenceList\' . detach\'\n-- In particular:\nfmap (fmap fill\' . sequenceList\' @I) . sequenceList\' @I . detach\'\n = fmap (fmap fill\' . sequenceList\' @I) . fmap (detach\' . fill\') \n . sequenceList\' @I . detach\'\n-- sequenceList\' is lawful (identity):\nfmap (fmap fill\' . I . fmap uI) . I . fmap uI . detach\'\n = fmap (fmap fill\' . I . fmap uI) . fmap (detach\' . fill\') . I\n . fmap uI . detach\'\n-- shift the I leftwards, and the uI rightwards, on both sides:\nI . I . fill\' . detach\' . fmap uI . fmap uI\n = I . I . fill\' . detach\' . fill\' . detach\' . fmap uI . fmap uI\n-- I is injective, and fmap uI is surjective:\nfill\' . detach\' = fill\' . detach\' . fill\' . detach\'\nRun Code Online (Sandbox Code Playgroud)\n我们最终得到 的幂等性fill\' . detach\',并且间接地得到 的幂等性sequenceA。尽管这样的性质就我们而言并不令人惊讶Traversable,因为它直接遵循恒等律,但相当有趣的是它本身也遵循组合律。(与此相关的是,我有时想知道我们是否可以从Semitraversable只有成分定律的类别中获得任何里程。)
现在是重新审视您最初的问题的好时机:到底为什么效果重复会导致法律出现问题?演示Fillable有助于澄清其中的联系。让我们再看看组合律的两边,以我们刚刚给出的形式:
fmap (fmap fill\' . sequenceList\') \n . sequenceList\' . detach\' -- LHS\n\n fmap (fmap fill\' . sequenceList\') \n . fmap (detach\' . fill\') \n . sequenceList\' . detach\' -- RHS\nRun Code Online (Sandbox Code Playgroud)\n让我们假设恒等律成立。在这种情况下,重复效果的唯一可能来源sequenceFill\'是被重复的元素detach\'(因为sequenceList\'不重复,并且fill\'由于恒等律而不能重复)。
现在,如果detach\'在某些位置引入重复项,fill\'则必须删除它们以便恒等律成立。然而,由于参数化,这些位置的元素将始终被删除,即使相关元素实际上并未重复,因为列表不是由detach\'. 换句话说,fill\'无害地删除重复项有一个前提条件,即必须给出可能由 生成的列表detach\'。在组合法则中,根据应用效果的不同,第一个法则可能sequenceList\'会产生不符合此前提条件的列表。在这种情况下,fmap fill\'右侧后面的 将会消除sequenceList\'实际上未重复的内部效果(请记住第一个仅处理外部应用层),第二个将及时检测到差异sequenceList\' . detach\',这作用于内部效果层,我们最终会违法。
事实上,我们可以肯定一些更强有力的东西:如果sequenceFill\'重复效果,总是有可能以上述方式违反法律。对于这样的主张,我们所需要的只是一个足够好的反例:
advance :: State (Const (Sum Natural) x) (Const (Sum Natural) x)\nadvance = get <* modify (+1)\nRun Code Online (Sandbox Code Playgroud)\n诀窍是,如果您对仅包含 副本的列表进行排序advance,则保证返回的列表不会有任何重复的Const (Sum Natural)效果:
GHCi> flip evalState 0 $ sequenceA (replicate 3 advance)\n[Const (Sum {getSum = 0}),Const (Sum {getSum = 1}),Const (Sum {getSum = 2})]\nRun Code Online (Sandbox Code Playgroud)\n既然如此,如果这样的列表达到sequenceFill\'重复效果的实现,则fmap fill\'其中的将始终丢弃非重复项:
data Bar a = Bar a\n deriving (Show, Functor)\n\ninstance Foldable Bar where\n foldMap f (Bar x) = f x <> f x\n\n-- This corresponds to your Traversable instance.\ninstance Fillable Bar where\n fill (Decomp (_, [x, y])) = Bar y\nRun Code Online (Sandbox Code Playgroud)\n\nGHCi> flip evalState 0 <$> (advance <$ Bar ())\nBar (Const (Sum {getSum = 0}))\nGHCi> flip evalState 0 <$> detach\' (advance <$ Bar ())\nDecomp {getDecomp = (Bar (),[Const (Sum {getSum = 0}),Const (Sum {getSum = 0})])}\nGHCi> flip evalState 0 $ (sequenceList\' . detach\') (advance <$ Bar ())\nDecomp {getDecomp = (Bar (),[Const (Sum {getSum = 0}),Const (Sum {getSum = 1})])}\nGHCi> flip evalState 0 $ (fmap fill\' . sequenceList\' . detach\') (advance <$ Bar ())\nBar (Const (Sum {getSum = 1}))\nRun Code Online (Sandbox Code Playgroud)\n现在违规是不可避免的:
\nGHCi> lhs = fmap (fmap fill\' . sequenceList\') . sequenceList\' . detach\'\nGHCi> rhs = fmap (fmap fill\' . sequenceList\') . fmap (detach\' . fill\') . sequenceList\' . detach\'\nGHCi> flip evalState 0 $ lhs (advance <$ Bar ())\nConst (Sum {getSum = 1})\nGHCi> flip evalState 0 $ rhs (advance <$ Bar ())\nConst (Sum {getSum = 2})\nRun Code Online (Sandbox Code Playgroud)\n(正如您可能已经注意到的,与您答案advance中的反例非常相似,只是进行了调整,以便它可以与任意可遍历的结构一起使用。)
这足以表明效果的重复与合成定律不相容。
\n此时,有一个方便的方法来证明为什么我们可以使用简化的 fill-then-detach 属性......
\n-- Precondition: length (toList sh) = length as\ndetach\' . fill\' $ (sh, as) = (sh, as)\nRun Code Online (Sandbox Code Playgroud)\n...代替我们在过去几节中处理的更庞大的组合定律。再次假设恒等律成立。在这种情况下,我们可以将可能的实现分为detach\'两种情况:
detach\'从不重复元素。因此,detach\'在填充然后分离前提条件的限制内,满射(例如,如果可遍历函子是长度为 6 的向量,则detach\'可以生成长度为 6 的所有可能列表,尽管它不会生成其他长度的列表)。但是,如果具有左逆函数的函数是满射函数,则其左逆函数也是右逆函数。因此,detach\' . fill\' = id在前提条件的范围内,组合律成立。
(“在填充然后分离前提条件的限制内”可能感觉像是挥手,但我相信通过使用依赖类型根据形状划分可遍历函子类型可以使其变得严格,就像我在第二部分的开头。)
\ndetach\'重复元素。然而,在这种情况下,随之而来的重复效应意味着复合定律将不成立,正如我们刚才所示,而且更强的定律也不会成立。detach\' . fill\' = id性质也不会成立。
既然如此,只要Traversable恒等律成立,组合律和Fillable填充然后分离律就总是一致的;它们之间的差异只能在违反身份法的实现中体现出来。因此,如果放在一起,Fillable答案第一部分中所述的定律等价于Traversable。
该演示文稿的一个美妙之处Fillable在于它如何明确表明,我们在定义合法性时唯一的自由选择sequenceA是效果的排序顺序。一旦通过选择实现选择了某个顺序Foldable,它决定了toList和detach\',sequenceList\'在对效果进行排序时必须遵循该顺序。此外,因为fill\'(在填充然后分离前提条件的范围内)是detach\',因此它是唯一确定的。
我们在基础库中的类层次结构与 的排列方式并不完全相同Fillable:realsequenceA是一种自给自足的方法Traversable,与 不同的是sequenceFill\',它的实现不依赖于Foldable。Foldable相反,和之间的联系Traversable是通过超类一致性律理顺的:
-- Given:\nfoldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m\nfoldMapDefault f = getConst . traverse (Const . f)\n\nfoldMapDefault = foldMap\nRun Code Online (Sandbox Code Playgroud)\nFunctor(和 也有类似的属性fmapDefault,但参数性意味着它遵循恒等律。)
根据toList和sequenceA,该定律变为:
toList = getConst . sequenceA . fmap (Const . (:[]))\nRun Code Online (Sandbox Code Playgroud)\n如果我们sequenceA = sequenceFill\'再回到Fillable演讲中……
getConst . fmap fill\' . sequenceList\' . detach\' . fmap (Const . (:[]))\ngetConst . fmap fill\' . sequenceList\' . fmap (Const . (:[])) . detach\'\n-- fmap @(Const _) doesn\'t do anything:\ngetConst . sequenceList\' . fmap (Const . (:[])) . detach\'\n-- sequenceList\' is lawful (foldMapDefault law):\ntoList @(Detach _) . detach\'\nsnd . getDecomp . detach\'\ntoList\nRun Code Online (Sandbox Code Playgroud)\n...我们的结论是该foldMapDefault法律自动成立。
在恒等律和组合律之后,第三个最著名的定律Traversable是应用函子中的自然性,通常简称为自然性律:
-- Precondition: h is an applicative homomorphism, that is:\n-- h (pure a) = pure a\n-- h (u <*> v) = h u <*> h v\nh . sequenceA = sequenceA . fmap h\nRun Code Online (Sandbox Code Playgroud)\n虽然有用,并且在理论方面也很重要(它反映了sequenceA应用函子和应用同态范畴中自然变换的另一种观点,例如在 Jaskelioff 和 Rypacek 的《遍历定律的调查》中进行了讨论),但自然性定律遵循自由定理sequenceA(按照 Voigtl\xc3\xa4nder 的风格,涉及构造函数类的自由定理),因此在这个答案的上下文中没有太多可说的。
鸟等人。第一部分提到的论文在第 6 节中讨论了一种不同的自然性属性,作者将其称为“数据类型中的自然性”。与众所周知的自然性法则不同,它是可遍历函子本身的自然性属性:
\n-- Precondition: r preserves toList, that is\n-- toList . r = toList\nfmap r . sequenceA = sequenceA . r\nRun Code Online (Sandbox Code Playgroud)\n(Bird 等人没有Foldable明确使用,而是用 来表述该性质contents = getConst . traverse (Const . (:[])。假设foldMapDefault相干律成立,则没有区别。)
这个Fillable视角非常适合这种自然属性。首先我们可以注意到我们也可以对某些函子进行自然变换t来进行处理Decomp t:
-- Decomp as a higher-order functor.\nhmapDecomp :: (forall x. t x -> u x) -> Decomp t a -> Decomp u a\nhmapDecomp r (Decomp (sh, as)) = Decomp (r sh, as)\nRun Code Online (Sandbox Code Playgroud)\n如果r保留toList(或者,我们甚至可以说,如果它是可折叠同态),则它也保留detach\',反之亦然:
-- Equivalent to toList . r = toList\nhmapDecomp r . detach\' = detach\' . r\'\nRun Code Online (Sandbox Code Playgroud)\n(hmapDecomp不影响内容列表,并且作为一种自然变换,可以r与(() <$)detach\'进行交换。)
如果我们进一步假设这些定律,我们可以利用和是逆Fillable的事实(在填充然后分离定律的前提条件范围内)从转变为:fill\'detach\'rdetach\'fill\'
hmapDecomp r . detach\' = detach\' . r\nhmapDecomp r . detach\' . fill\' = detach\' . r . fill\'\nhmapDecomp r = detach\' . r . fill\'\nfill\' . hmapDecomp r = fill\' . detach\' . r . fill\'\nfill\' . hmapDecomp r = r . fill\'\nRun Code Online (Sandbox Code Playgroud)\n也就是说,应用到形状然后填充它与填充然后应用到填充后的形状r相同。r
此时,我们可以回到sequenceFill\':
fill\' . hmapDecomp r = r . fill\'\nfmap (fill\' . hmapDecomp r) = fmap (r . fill\')\nfmap (fill\' . hmapDecomp r) . sequenceList\' . detach\'\n = fmap (r . fill\') . sequenceList\' . detach\'\n-- LHS\nfmap (fill\' . hmapDecomp r) . sequenceList\' . detach\'\n-- sequenceList\' only changes the list, and `hmapDecomp` r only the shape.\nfmap fill\' . se
| 归档时间: |
|
| 查看次数: |
213 次 |
| 最近记录: |