14

为什么在定义函数时重复

   duplicate :: w a -> w (w a)     

对于 Comonad 类型类(链接),您必须“在上下文中”修改所有元素(即更改上下文当前值以外的元素)。为什么不在Monad 中使用类似return的东西?

示例(拉链):

   data Z a = Z [a] a [a]     

为什么我不能将重复定义为

   duplicate z = Z [] z []     

我试图从 Comonad 规则中得出对副本函数的要求,但我总是得到一个副本,它只是将元素包装起来,就像在 monad 中的return一样,不需要做任何其他事情。

一篇博文说:

重复有点难以掌握。从一个列表拉链,我们必须构建一个列表拉链的列表拉链。这背后的意义(由每个实例必须满足的共单定律证实)是在复制结构内移动返回原始结构,由相同的移动改变

但我不明白为什么一定是这样。Comonad规则中的fmap 总是适用于被包装的元素,然后这个元素总是用extract “解包”,除了包装duplicate的参数之外,为什么还要在duplicate函数中做其他事情呢?

你能指出我错过了什么吗?我觉得我在某个地方犯了一些明显的错误,但我自己无法弄清楚。

提前感谢您的回复!

4

1 回答 1

7

如果您可以使用该类型做其他事情,而不是简单地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 =<= isFirstorisFirst =<= 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将在上下文中到处都有一个完整的“另一个拉链”,以保存该位置的值和该位置​​的上下文。

让我们看看我们可以从这些定律中推断出什么。稍微挥动一下函数的类别,我们可以看到=<= extractfmap 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 Zwith xin the middle 代表中间
  • right与右侧长度相同的列表

此外,我们可以看到左侧和右侧列表中的中间值必须与这些列表中的原始值相同。仅考虑这一定律,我们就足以要求对 的结果采用不同的结构duplicate

于 2014-12-04T04:13:38.513 回答