( -> fmap f id) 总是等价于 arr 吗？

Question

Category

的一些实例也是

Functor

的实例。例如：

{-# LANGUAGE ExistentialQuantification, TupleSections #-}

import Prelude hiding (id, (.))
import Control.Category
import Control.Arrow

data State a b = forall s. State (s -> a -> (s, b)) s

apply :: State a b -> a -> b
apply (State f s) = snd . f s

assoc :: (a, (b, c)) -> ((a, b), c)
assoc (a, (b, c)) = ((a, b), c)

instance Category State where
    id = State (,) ()
    State g t . State f s = State (\(s, t) -> assoc . fmap (g t) . f s) (s, t)

(.:) :: (Functor f, Functor g) => (a -> b) -> f (g a) -> f (g b)
(.:) = fmap . fmap

instance Functor (State a) where
    fmap g (State f s) = State (fmap g .: f) s

instance Arrow State where
    arr f = fmap f id
    first (State f s) = State (\s (x, y) -> fmap (,y) (f s x)) s

这里

arr f = fmap f id

代表

instance Arrow State

。对于所有也是

Category

实例的

Functor

实例来说，这是否正确？类型签名是：

arr               ::                 Arrow    a  => (b -> c) -> a b c
(\f -> fmap f id) :: (Functor (a t), Category a) => (b -> c) -> a b c

在我看来它们应该是等价的。

Answer 1

首先我们要明确

Arrow C

的含义。嗯，这是两个完全不同的东西结合在一起——在我的书中，

• 尖锐幺半群范畴的类。
• 泛化 Hask 的 类别类。

arr

来自后者。 “概括”Hask？这意味着只是拥有从类别 Hask 到

C

的映射。 – 从数学上讲，从一个类别映射到另一个类别正是函子所做的！ （标准

Functor

类实际上只涵盖一种非常具体的函子，即 Hask 上的 endofunctor。）

arr

是非 endofunctor 的态射方面，即“规范嵌入函子” Hask →

C

。

从这个角度来看，前两条箭头定律

arr id = id
arr (f >>> g) = arr f >>> arr g

只是函子定律。

现在，如果您为某个类别实现

Functor

实例，这意味着什么？为什么，我敢说这只是意味着您正在表达相同的规范嵌入函子，但是通过

Hask

中 C 的必要表示（这使得它总体上成为一个内函子）。因此我认为，是的，

\f -> fmap f id

应该等同于

arr

，因为基本上它们是表达同一事物的两种方式。

Answer 2

这里有一个推导来补充 leftaroundabout 的解释。为了清楚起见，我将为

(.)

保留

id

和

(->)

，并为通用

(<<<)

方法使用

id'

和

Category

。

我们从

preComp

开始，也称为

(>>>)

：

preComp :: Category y => y a b -> (y b c -> y a c)
preComp v = \u -> u <<< v

fmap

通过 Hask 函子之间的自然变换进行通勤。对于也有

Category

实例的

Functor

，

preComp v

是自然变换（从

y b

到

y a

），因此它与

fmap

交换。由此可见：

fmap f . preComp v = preComp v . fmap f
fmap f (u <<< v) = fmap f u <<< v
fmap f (id' <<< v) = fmap f id' <<< v
fmap f v = fmap f id' <<< v

这就是我们的候选人

arr

！那么让我们定义

arr' f = fmap f id'

。我们现在可以验证

arr'

遵循第一箭头定律...

-- arr id = id'
arr' id
fmap id id'
id'

...还有第二个：

-- arr (g . f) = arr g <<< arr f
arr' (g . f)
fmap (g . f) id'
(fmap g . fmap f) id'
fmap g (fmap f id')
fmap g (arr' f)
fmap g id' <<< arr' f -- Using the earlier result.
arr' g <<< arr' f

我想这就是我们所能做到的。其他五个箭头定律涉及

first

，并且正如 leftaroundabout 指出的，

arr

和

first

是独立的。