Подтвердить что ты не робот

Стрелка без arr

Если мы ограничиваем наше понимание категории обычным классом Category в Haskell:

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

Тогда скажем, что a 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

Или мы можем получить (***) из first и second:

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

Мы также можем получить:

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

Или мы можем получить (&&&) с учетом dup и (***):

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

Какой мой вопрос и что мой вопрос? Это:

Что такое Arrow без arr? Это кажется совершенно последовательным и полезным. Существуют ли законы стрельбы (кроме законов категории), которые не включают arr и остаются здесь нетронутыми? И что это значит в теории категорий?

Я в основном украл этот вопрос из reddit, но обобщил и изложил его: http://www.reddit.com/r/haskell/comments/2e0ane/category_with_fanout_and_split_but_not_an_arrow/

4b9b3361

ОТВЕТЫ

Ответ 1

Так же, как Arrow является категорией с продуктом, Arrow без arr также является категорией с продуктом (таким образом, законы категории всегда сохраняются).

arr является функтором от категории Хаск до категории c. Ниже показан код, показанный ниже. arr обеспечивает способ поднять нормальные функции (морфизмы в Hask) в экземплярную категорию c. Это похоже на fmap (endofunctor от 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