Is (\ f -> 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. Ну, это две совершенно разные вещи, объединенные – в моей книге,

• Класс well-pointed monoidal categories.
• Класс categories which generalise Hask.

arr происходит от последнего. “ Обобщение ” Hask? То, что это означает, - это просто картирование из категории Hask до C. – И математически, отображение из одной категории в другую - это именно то, что делает functor! (Стандартный Functor класс фактически охватывает только очень специфический вид функторов, а именно endofunctors на HASK.) arr морфизм-аспект не-endofunctor, а именно “ канонического вложения функтор ” Hask → C.

С этой точки зрения, первые две стрелки Законов

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

являются только законы функторов.

Теперь, что это означает, если вы используете экземпляр Functor для категории? Почему, я полагаю, это просто означает, что вы выражаете тот же самый канонический функтор встраивания, но через необходимое представление C назад в Hask (что делает его полнофункциональным endofunctor). Поэтому я бы сказал, что да, \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 endofunctors.Для Category, который также имеет экземпляр Functor, preComp v является естественным преобразованием (отдо 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, а в качестве остаточных точек arr и first являются независимыми.