箭头定律:首先仅取决于该对的第一个组成部分.我们为什么需要这个? [英] Arrow law: first depends only on the first component of the pair. Why do we need this one?

问题描述

约翰·休斯(John Hughes)在他的《将Monads推广到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的影响...

那些法律仅仅是纯粹的形式化证据吗?

解决方案

简短的回答:有另一对法律涵盖"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)

回想一下，休斯说箭头是纯"的. (可以等同地，没有副作用")是否可以写为arr expr.因此，该定律指出，给定任何已经是纯函数且可以写为arr f的计算，将first应用于该计算也将导致纯计算(因为它的形式为arr expr且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在确定其副作用和构造其输出的C成分时可以依赖于输入的d成分的可能性成为可能.但是，arr fst >>> f动作的结构通过在允许f进行任何重要运算之前通过纯动作删除d组件消除了这种可能性.这两个动作是相等的(定律)，这清楚地说明了first f从<产生了C输出(以及副作用，通过f产生了副作用，因为first没有其自身的附加作用). c20>输入以不能依赖于d输入的方式.

LAW-B很难.形式化此属性的最明显方法是伪法则:

first f >>> arr snd = arr snd

直接声明first f不会更改提取的(arr snd)第二个成分.但是，休斯指出，这太太，因为它不允许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))

John Hughes in his "Generalising Monads to Arrows" writes (chapter 8):

We formalise the property that first f depends only on first components of pairs as follows: first f >>> arr fst = arr fst >>> f

I understand that the law filters out implementations of such sort:

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

instance Category KleisliMaybe where 
 ...

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

But the wording seems a bit odd for this case (I would have chosen "first has no side-effects" or something like that for such an instance).

So, what are other reasons to keep it around?

Moreover, there is another law: first f >>> second (arr g) = second (arr g) >>> first f. I did not find any implementations it filters out (I did - see the edit). How does this law help us?

---

Edit: more thoughts on the latter law.

Take a look at the following snippet:

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)))

Such an instance behaves this way:

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"

As far as I get it, we have got no law for second f = swap >>> first f >>> swap. Therefore, we can forbid both second and first to have any side-effects with this law. Yet, the original wording still does not seem to hint at that again:

...we formalise the intuition that the second component of the pair is unaffected by first f as a law...

Are those laws just pure formalisations for solid proofs?

解决方案

Short answer: There's a different pair of laws that cover "first and second have no side-effects":

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

After thinking about it, I THINK that both laws you've identified:

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

are, in fact, redundant because they follow from those no-side-effects laws, the other laws, and a couple of "free theorems".

Your counterexamples violate the no-side-effects laws, so that's why they also violate LAW-A and/or LAW-B. If someone has a true counterexample that obeys the no-side-effects laws but violates LAW-A or LAW-B, I'd be very interested in seeing it.

Long answer:

The property "first has no side effects (of its own, at least)" is better formalized by the law stated earlier in Section 8 of that article:

first (arr f) = arr (first f)

Recall that Hughes says an arrow is "pure" (equivalently, "has no side-effects") if it can be written arr expr. So, this law states that, given any computation that is already pure and so can be written arr f, applying first to that computation also results in a pure computation (because it is of the form arr expr with expr = first f). Therefore, first introduces no impurities / no effects of its own.

The other two laws:

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

are intended to capture the idea that for a particular instance Arrow Foo and a particular arrow action f :: Foo B C, the action:

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

acts on the first components of its input/output pairs as if the second components weren't there. The laws correspond to the properties:

1. LAW-A: the output component C and any side effects depend only on input B, not input d (i.e., no dependence on d)
2. LAW-B: the component d passes through unchanged, unaffected by the input B or any side effects (i.e., no effect on d)

With respect to LAW-A, if we consider the action first f :: Foo (B,d) (C,d) and focus on the C component of its output using a pure function to extract it:

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

then the result is the same as if we first forcibly remove the second component using a pure action:

arr fst :: Foo (B,d) B

and allow the original action f to act only on B:

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

Here, the structure of the first f >>> arr fst action leaves open the possibility that first f can depend on the d component of the input in formulating its side effects and constructing the C component of its output; but, the structure of the arr fst >>> f action eliminates this possibility by removing the d component via a pure action before allowing any non-trivial computation by f. The fact that these two actions are equal (the law) makes it clear that first f produces a C output (and side effects, through f, since first has no additional effects of its own) from the B input in a manner that can't also depend on the d input.

LAW-B is is harder. The most obvious way of formalizing this property would be the pseudolaw:

first f >>> arr snd = arr snd

which directly states that first f doesn't change the extracted (arr snd) second component. However, Hughes points out that this is too restrictive, because it doesn't allow first f to have side effects (or at least any that can survive the pure action arr snd). Instead, he provides the more complicated law:

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

The idea here is that, if first f ever modified the d value, then there would be some case where the following two actions would be different:

-- `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))

But, because of LAW-B, we have:

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

and so the actions are the same, contrary to our assumption.

HOWEVER, I conjecture that LAW-A and LAW-B are both redundant, because I believe (see my hesitation below) they follow from the other laws plus a "free theorem" for the signature:

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

Assuming first and second satisfy the no-side-effects laws:

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

then LAW-B can be rewritten as:

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

and this last statement is just the free theorem for first f. (Intuitively, since first f is polymorphic in the type of d, any pure action on d is necessarily "invisible" to first f, so first f and any such action will commute.) Similarly, there's a free theorem for:

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

that captures the idea that, since this signature is polymorphic in d, no pure pre-action on d can affect the action:

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

But the left-hand side can be rewritten:

-- 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

giving the right-hand side.

I only hesitate here because I'm not used to thinking about "free theorems" for possibly effectful arrows instead of functions, and so I'm not 100% sure that it goes through.

I'd be very interested to see if someone can come up with true counterexamples for these laws that violate LAW-A or LAW-B but satisfy the no-side-effects laws. The reason your counterexamples violate LAW-A and LAW-B is that they violate the no-side-effects laws. For your first example:

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

and for your second:

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

这篇关于箭头定律:首先仅取决于该对的第一个组成部分.我们为什么需要这个?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！