(\f -> fmap f id) 是否总是等价于 arr？答案

【问题标题】：Is (\f -> fmap f id) always equivalent to arr?(\f -> fmap f id) 是否总是等价于 arr？
【发布时间】：2015-07-24 19:29:31
【问题描述】：

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

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

【问题讨论】：

至少，Arrow 法律足以由instance Arrow a => Functor (a s) where fmap f v = v >>> arr f定义一个守法的Functor 实例。也许这与参数化一起足以确保这也是唯一守法的实例，尽管我还没有弄清楚细节，所以我不会声称它是真的。
请记住，对于函数和箭头，fmap 应该等于 (<<<)。
This comment 表明我是对的：参数化最多保证一个守法的Functor 实例。所以你的问题的答案似乎是“是”。
由于 arr 是 Arrow 的方法，而不是 Category，我仍然有些怀疑 - 我怀疑每个 Category 也是 Functor 需要是 @987654342 @。然而，反过来也是如此，因为每个 Arrow gives not just a Functor, but an Applicative。
@ØrjanJohansen “我怀疑每个 Category 也是 Functor 需要是 Arrow” - 事实上，虽然根本问题是 arr 和 first 是，正如 leftaroundabout 下面所说，“完全不同的东西结合在一起”。

标签： haskell functor category-theory arrows category-abstractions

【解决方案1】：

首先让我们弄清楚Arrow C 的含义。嗯，这是两个完全不同的东西——在我的书中，

well-pointed monoidal categories 的类。
categories which generalise Hask 的类。

arr 来自后者。 “概括”Hask？这意味着只有从 Hask 类别到 C 的映射。 – 在数学上，从一个类别映射到另一个类别正是 functor 所做的！（标准的Functor 类实际上只涵盖了一种非常特殊的函子，即Hask 上的内函子。）arr 是非内函子的态射方面，即“规范嵌入函子” ” Hask → C.

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

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

只是函子定律。

现在，如果您正在为一个类别实现 Functor 实例，这意味着什么？为什么，我敢说这只是意味着您正在表达相同的规范嵌入函子，但是通过 Hask 中C 的必要表示（这使其成为整体上的内函子）。因此，我认为是的，\f -> fmap f id 应该等同于 arr，因为基本上它们是表达同一事物的两种方式。

【讨论】：

@duplode：实际上不是。我发布了错误的链接（Function 做了相反的事情，它是专门的类，而不是通用函数）。这是正确的：“就constrained-categories而言，每个Category C也是Functor C (->) (->)也是EnhancedCat C (->)”。

【解决方案2】：

这是补充leftaroundabout解释的推导。为清楚起见，我将为(->) 保留(.) 和id，并为通用Category 方法使用(<<<) 和id'。

我们以preComp开头，也称为(>>>)：

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

fmap 在 Hask 内函子之间进行自然转换。对于同时具有Functor 实例的Category，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 是独立的。

【讨论】：