9

的一些实例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

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

4

2 回答 2

6

首先让我们弄清楚是什么Arrow C意思。嗯，这是两个完全不同的东西结合在一起——在我的书中，

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

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

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

只是函子定律。

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

于 2015-07-25T02:08:37.217 回答
3

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

我们从 开始preComp，也称为(>>>)：

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

fmap在Hask endofunctors之间进行自然转换。对于Category也有Functor实例的 a ，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独立的。

于 2015-07-25T07:41:07.883 回答