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

约翰·休斯 (John Hughes) 在他的“将单子概括为箭头”中写道（第 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 and first该法律有任何副作用。然而，最初的措辞似乎仍然没有再次暗示这一点：

...我们形式化了直觉，即该对的第二个组成部分不受first f作为法律...

这些法律只是纯粹的形式化确凿证据吗？

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

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

想了想之后，我THINK您已经确定的两条法律：

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)

回想一下，休斯说，如果箭头可以写，那么它就是“纯粹的”（相当于“没有副作用”）arr expr。因此，该定律指出，给定任何已经是纯粹的计算，因此可以写成arr f, 申请first该计算也会导致纯计算（因为它的形式是arr expr with 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可以取决于d输入的组成部分在制定其副作用和构建C其输出的组成部分；但是，该结构的arr fst >>> f行动通过消除这种可能性d在允许任何不平凡的计算之前通过纯动作来组件f。这两个行为是平等的（法律）这一事实清楚地表明：first f产生一个C输出（和副作用，通过f, since first本身没有额外的效果）B以这样的方式输入can't还取决于d input.

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

first f >>> arr snd = arr snd

这直接说明了first f不会改变提取的（arr snd) 第二个组成部分。然而，休斯指出，这是too限制性的，因为它不允许first f产生副作用（或至少任何可以在纯粹的行动中幸存下来的副作用）arr snd）。相反，他提供了更复杂的法律：

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

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

-- `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 and 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, so 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))