箭头没有箭的问题

25

如果我们将类别的理解限制为 Haskell 中通常的 Category 类:

class Category c where
  id :: c x x
  (>>>) :: c x y -> c y z -> c x z

那么我们可以说,Arrow 是一个 Category ,它还可以额外执行以下操作:

class Category c => Arrow c where
  (***) :: c x y -> c x' y' -> c (x,x') (y,y')
  (&&&) :: c x y -> c x y' -> c x (y,y')

我们可以轻易地推导出:

first :: c x y -> c (x,z) (y,z)
first a = a *** id

second :: c x y -> c (z,x) (z,y)
second a = id *** a

或者我们可以从firstsecond中推导出(***):

a1 *** a2 = first a1 >>> second a2

我们也可以推导出:

dup :: c x (x,x)
dup = id &&& id

或者我们可以通过 dup(***) 推出 (&&&)

a1 &&& a2 = dup >>> (a1 *** a2)

我的观点和问题是:

如果没有 arrArrow 还有什么意义和用处呢?它似乎非常连贯和有用。除了范畴定律之外,还有哪些箭头定律不涉及 arr 并在此保持不变呢?这一切在范畴论中意味着什么?


我基本上从 Reddit 偷了这个问题,并加以概括和阐述:http://www.reddit.com/r/haskell/comments/2e0ane/category_with_fanout_and_split_but_not_an_arrow/


我在我的constrained-categories项目中有一个类,有点傻乎乎地叫做Morphism。即使没有函数,一些法则仍然有意义...像fstconst这样的东西是该包中其他类的方法,并且需要使用它们来正确地制定法律。我会感到惊讶如果Edward、Conal或其他人没有在某个地方已经做过了,但是我不知道用哪个名字... - leftaroundabout
5
你可以阅读有关广义箭头的内容。 - Luis Casillas
1个回答

2
正如Arrow是一个带有产品的类别,没有arrArrow也是一个带有产品的类别(因此类别法则始终成立)。 arr是从Hask类别到c类别的一个函子。下面的代码显示了这一点。arr提供了一种将普通函数(在Hask中是态射)提升到实例化的c类别中的方法。这有点像fmap(从Hask到Hask的自函子),但更加通用。与此相关的一些箭头定律在这里描述了函子定律(虽然还有产品的定律)。
因此,省略arr,您将失去将普通函数提升的功能,或者从另一个角度来看,可以免费获得不需要实现它的特性。但是,所有其他特征都是相同的。
{-# LANGUAGE TypeOperators, RankNTypes #-}

-- | Functor arrow
type (:->) c d = forall a b. c a b -> d a b

-- | Hask category; types are objects, functions are morphisms.
type Hask = (->)

arr :: Arrow c => Hask :-> c
arr = Control.Arrow.arr

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接