如果您可以使用该类型做其他事情,而不是简单地extract
使用它,这一点很重要。直观地说,如果你唯一能做的就是提取值,那么类型只保存一个值,所以复制一个值就是复制所有内容。一般来说,这不是真的,拉链也不是这样。
这些Comonad
规律只是伪装在类型函数上的范畴规律w a -> b
。由于这些来自类别,因此根据类别而不是Comonad
法律来推理它们可能更容易。 extract
是这个类别的标识, =<=
是合成算子。
-- | Right-to-left 'Cokleisli' composition
(=<=) :: Comonad w => (w b -> c) -> (w a -> b) -> w a -> c
f =<= g = f . extend g
我们也知道extend f = fmap f . duplicate
,所以我们可以写
f =<= g = f . fmap g . duplicate
这看起来很容易推理。现在,让我们为您的Z
类型配备另一个我们可以讨论的功能。仅当在列表中的某个位置表示一个值isFirst
时才会返回 true ,而它之前没有任何内容。Z
isFirst :: Z a -> Bool
isFirst (Z [] _ _) = True
isFirst _ = False
现在,让我们考虑当我们使用isFirst
三类法则时会发生什么。唯一似乎立即适用于它的只有两个extract
是由 组成的左右身份=<=
。由于我们只是在反驳这一点,我们只需要找到一个反例。我怀疑其中一个extract =<= isFirst
orisFirst =<= extract
将失败为 input Z [1] 2 []
。这两个都应该和 一样isFirst $ Z [1] 2 []
,也就是False
。我们会extract =<= isFirst
先尝试,结果恰好成功。
extract =<= isFirst $ Z [1] 2 []
extract . fmap isFirst . duplicate $ Z [1] 2 []
extract . fmap isFirst $ Z [] (Z [1] 2 []) []
extract $ Z [] (isFirst (Z [1] 2 [])) []
extract $ Z [] False []
False
当我们尝试时,isFirst =<= extract
我们不会那么幸运。
isFirst =<= extract $ Z [1] 2 []
isFirst . fmap extract . duplicate $ Z [1] 2 []
isFirst . fmap extract $ Z [] (Z [1] 2 []) []
isFirst $ Z [] (extract (Z [1] 2 [])) []
isFirst $ Z [] 2 []
True
当我们duplicate
丢失有关结构的信息时。事实上,除了拉链的单一焦点之外,我们丢失了关于无处不在的所有信息。正确的duplicate
将在上下文中到处都有一个完整的“另一个拉链”,以保存该位置的值和该位置的上下文。
让我们看看我们可以从这些定律中推断出什么。稍微挥动一下函数的类别,我们可以看到=<= extract
是fmap extract . duplicate
,这需要是恒等函数。显然,我正在重新发现法律是如何在Control.Category
. 这让我们可以写一些类似的东西
z = (=<= extract) z
z = fmap extract . duplicate $ z
现在,z
只有一个构造函数,所以我们可以将其替换为
Z left x right = fmap extract . duplicate $ Z left x right
从它们的重复类型,我们知道它必须返回相同的构造函数。
Z left x right = fmap extract $ Z lefts (Z l x' r) rights
如果我们申请fmap
这个Z
,我们有
Z left x right = Z (fmap extract lefts) (extract (Z l x' r)) (fmap extract rights)
如果我们将其按构造函数的部分拆分,Z
我们将得到三个等式
left = fmap extract lefts
x = extract (Z l x' r)
right = fmap extract rights
这告诉我们,至少duplicate (Z left x right)
必须成立的结果:
left
与左侧长度相同的列表
- a
Z
with x
in the middle 代表中间
right
与右侧长度相同的列表
此外,我们可以看到左侧和右侧列表中的中间值必须与这些列表中的原始值相同。仅考虑这一定律,我们就足以要求对 的结果采用不同的结构duplicate
。