haskell - 箭头定律：首先仅取决于对的第一个分量。为什么我们需要这个？

Question

John Hughes 在他的“Generalising Monads to Arrows”中写道（第 8 章）：

first f我们将仅依赖于对的第一个组件 的属性形式化如下：first f >>> arr fst = arr fst >>> f

我知道法律会过滤掉这种类型的实现：

newtype KleisliMaybe a b = KMb { runKMb :: a -> Maybe b }

instance Category KleisliMaybe where 
 ...

instance Arrow KleisliMaybe where
 first f = KMb $ const Nothing
 ...

但是对于这种情况，措辞似乎有点奇怪（对于这种情况，我会选择“first没有副作用”或类似的东西）。

那么，保留它的其他原因是什么？

此外，还有一条规律：first f >>> second (arr g) = second (arr g) >>> first f。我没有找到它过滤掉的任何实现（我确实 - 请参阅编辑）。这部法律对我们有什么帮助？

---

编辑：关于后一种法律的更多想法。

看看下面的代码片段：

newtype KleisliWriter = KW { runKW :: a -> (String, b) }

instance Category KleisliWriter where
 ...

instance Arrow KleisliWriter where
 arr f = KW $ \ x -> ("", f x)
 first  (KW f) = KW $ \ ~(a, d) -> f a >>= (\ x -> ("A", (x, d)))
 second (KW f) = KW $ \ ~(d, b) -> f b >>= (\ x -> ("B", (d, x)))

这样的实例的行为方式如下：

GHCi> c = KW $ \ x -> ("C", x)
GHCi> fst . runKW (first c >>> second (arr id)) $ (1, 2)
"CAB"
GHCi> fst . runKW (second (arr id) >>> first c) $ (1, 2)
"BCA"

据我所知，我们没有法律second f = swap >>> first f >>> swap。因此，我们可以禁止这两种方法second，也可以禁止first这条法律产生任何副作用。然而，原来的措辞似乎仍然没有再次暗示这一点：

...我们将直觉中的第二个组成部分不受first f法律的影响...

那些法律只是纯粹的形式化的可靠证明吗？

标签： haskellmonadsarrowscombinatorskleisli

Answer 1

简短的回答： 有一对不同的法律涵盖“first并且second没有副作用”：

first (arr f) = arr (first f)
second (arr f) = arr (second f)

在考虑之后，我认为您已经确定了两条法律：

first f >>> arr fst          =   arr fst >>> f                -- LAW-A
first f >>> second (arr g)   =   second (arr g) >>> first f   -- LAW-B

事实上，它们是多余的，因为它们遵循那些无副作用定律、其他定律和几个“自由定理”。

你的反例违反了无副作用的法律，这就是为什么它们也违反了 LAW-A 和/或 LAW-B。如果有人有一个真正的反例，它遵守无副作用定律但违反了 LAW-A 或 LAW-B，我会非常有兴趣看到它。

长答案：

该属性“first没有副作用（至少它自己的）”由该条第 8 节前面所述的法律更好地形式化：

first (arr f) = arr (first f)

回想一下，Hughes 说过，如果可以写箭头，它就是“纯的”（相当于“没有副作用”）arr expr。因此，该定律指出，给定任何已经是纯的并且可以编写的计算arr f，应用于first该计算也会导致纯计算（因为它的形式是arr exprwith expr = first f）。因此，first不引入杂质/没有自身的影响。

其他两条法律：

first f >>> arr fst          =   arr fst >>> f                -- LAW-A
first f >>> second (arr g)   =   second (arr g) >>> first f   -- LAW-B

旨在捕捉对于特定instance Arrow Foo和特定箭头动作的想法，f :: Foo B C动作：

first f :: forall d. Foo (B,d) (C,d)

作用于其输入/输出对的第一个组件，就好像第二个组件不存在一样。定律对应于性质：

1. LAW-A：输出组件C和任何副作用仅取决于输入B，而不是输入d（即不依赖于d）
2. LAW-B：组件d通过不变，不受输入B或任何副作用的影响（即对 没有影响d）

对于 LAW-A，如果我们考虑动作first f :: Foo (B,d) (C,d)并关注C其输出的组成部分，使用纯函数提取它：

first f >>> arr fst :: Foo (B,d) C

那么结果与我们首先使用纯动作强制删除第二个组件相同：

arr fst :: Foo (B,d) B

并允许原始操作f仅作用于B：

arr fst >>> f :: Foo (B,d) C

在这里，first f >>> arr fst动作的结构留下了在制定其副作用和构造其输出的分量时first f依赖于输入分量的可能性；但是，动作的结构通过在允许任何非平凡计算之前通过纯动作删除组件来消除这种可能性。这两个动作相等的事实（定律）清楚地表明，以一种不能依赖于输入的方式从输入产生输出（和副作用，通过，因为它本身没有额外的影响）.dCarr fst >>> fdffirst fCffirstBd

LAW-B 更难。形式化此属性的最明显方法是伪定律：

first f >>> arr snd = arr snd

它直接声明first f不会更改提取的 ( arr snd) 第二个组件。然而，Hughes 指出这限制性太强，因为它不允许first f产生副作用（或者至少任何可以在纯粹的动作中幸存下来的副作用arr snd）。相反，他提供了更复杂的法则：

first f >>> second (arr g)   =   second (arr g) >>> first f

这里的想法是，如果first f曾经修改过该d值，那么在某些情况下，以下两个操作会有所不同：

-- `first f` changes `inval` to something else
second (arr (const inval)) >>> first f
-- if we change it back, we change the action
second (arr (const inval)) >>> first f >>> second (arr (const inval))

但是，由于 LAW-B，我们有：

second (arr (const inval)) >>> first f >>> second (arr (const inval))
-- associativity
= second (arr (const inval)) >>> (first f >>> second (arr (const inval)))
-- LAW-B
= second (arr (const inval)) >>> (second (arr (const inval)) >>> first f)
-- associativity
= (second (arr (const inval)) >>> (second (arr (const inval))) >>> first f
-- second and arr preserve composition
= second (arr (const inval >>> const inval)) >>> first f
-- properties of const function
= second (arr (const inval)) >>> first f

所以动作是相同的，与我们的假设相反。

但是，我推测 LAW-A 和 LAW-B 都是多余的，因为我相信（请参阅下面我的犹豫）它们遵循其他定律以及签名的“自由定理”：

first f :: forall d. Foo (B,d) (C,d)

假设first并second满足无副作用定律：

first (arr f) = arr (first f)
second (arr f) = arr (second f)

那么 LAW-B 可以重写为：

first f >>> second (arr g)              = second (arr g) >>> first f
-- no side effects for "second"
first f >>> arr (second g)              = arr (second g) >>> first f
-- definition of "second" for functions
= first f >>> arr (\(x,y) -> (x, g y))  = arr (\(x,y) -> (x, g y)) >>> first f

最后一条语句只是 的自由定理first f。（直观地说，由于first f的类型是多态的d，任何纯动作对d来说必然是“不可见的” first f，因此first f任何这样的动作都会对等。）同样，有一个自由定理：

first f >>> arr fst :: forall d. Foo (B,d) C

这抓住了这样一个想法，因为这个签名在 中是多态的d，所以没有纯粹的预操作d会影响操作：

arr (\(x,y) -> (x, g y)) >>> (first f >>> arr fst) = first f >>> arr fst

但是左边可以改写：

-- by associativity
(arr (\(x,y) -> (x, g y)) >>> first f) >>> arr fst
-- by rewritten version of LAW-B
(first f >>> arr (\(x,y) -> (x, g y))) >>> arr fst
-- by associativity
first f >>> (arr (\(x,y) -> (x, g y)) >>> arr fst)
-- `arr` preserves composition
first f >>> arr ((\(x,y) -> (x, g y)) >>> fst)
-- properties of fst
first f >>> arr fst

给出右手边。

我只是在这里犹豫，因为我不习惯为可能有效的箭头而不是函数考虑“自由定理”，所以我不能 100% 确定它会通过。

我很想看看是否有人可以为这些违反 LAW-A 或 LAW-B 但满足无副作用法律的法律提出真正的反例。您的反例违反 LAW-A 和 LAW-B 的原因是它们违反了无副作用定律。对于您的第一个示例：

> runKMb (first (arr (2*))) (2,3)
Nothing
> runKMb (arr (first (2*))) (2,3)
Just (4,3)

第二个：

> runKW (first (arr (2*))) (1,2)
("A",(2,2))
> runKW (arr (first (2*))) (1,2)
("",(2,2))