Là (\ f -> fmap f id) luôn luôn tương đương với arr?

Question

Một số trường hợp của Category cũng là trường hợp của Functor. Ví dụ:

{-# 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 

Đây arr f = fmap f id cho instance Arrow State. Điều này có đúng với mọi trường hợp của Category cũng là trường hợp của Functor không? Các chữ ký loại là:

arr    ::     Arrow a => (b -> c) -> a b c 
(\f -> fmap f id) :: (Functor (a t), Category a) => (b -> c) -> a b c 

Dường như với tôi rằng chúng phải tương đương nhau.

Answer 1

Trước tiên, hãy hiểu rõ ràng phương thức Arrow C. Vâng, đó là hai điều khá riêng biệt được kết hợp – trong sách của tôi,

• Lớp học well-pointed monoidal categories.
• Lớp học categories which generalise Hask.

arr xuất phát từ sau. “ Generalize ” Hask? Điều này có nghĩa là chỉ cần có ánh xạ từ danh mục Hask đến C. – Và toán học, ánh xạ từ một thể loại này sang danh mục khác chính xác là những gì mà functor làm được! (Tiêu chuẩn Functor lớp thực sự chỉ bao gồm một loại rất cụ thể của functors, cụ thể là endofunctors trên Hask.) arr là cấu xạ-khía cạnh của một tổ chức phi endofunctor, cụ thể là “ kinh điển nhúng functor ” Hask → C.

Từ quan điểm này, hai luật mũi tên đầu tiên

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

chỉ là những luật functor.

Bây giờ, điều đó có nghĩa là gì nếu bạn đang triển khai một cá thể Functor cho một danh mục? Tại sao, tôi daresay nó chỉ đơn giản có nghĩa là bạn đang thể hiện cùng một functor nhúng kinh điển, nhưng thông qua các đại diện cần thiết của C trở lại trong Hask (mà làm cho nó một endofunctor tổng thể). Do đó tôi cho rằng có, \f -> fmap f id nên tương đương với arr, vì về cơ bản chúng là hai cách thể hiện cùng một điều.

Answer 2

Dưới đây là một dẫn xuất để bổ sung giải thích của leftaroundabout. Để rõ ràng, tôi sẽ đặt trước (.) và id cho (->) và sử dụng (<<<) và id' cho phương thức chung Category.

Chúng tôi bắt đầu với preComp, còn được gọi là (>>>):

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

fmap đi lại với biến đổi tự nhiên giữa Hask endofunctors.Đối với một số Category cũng có một phiên bản Functor, preComp v là một phép biến đổi tự nhiên (từ y b đến y a) và vì vậy nó bắt đầu với fmap. Sau đó:

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 

Đó là ứng cử viên của chúng tôi arr! Vì vậy, hãy xác định arr' f = fmap f id'. Bây giờ chúng ta có thể xác minh rằng arr' theo pháp luật mũi tên đầu tiên ...

-- arr id = id' 
arr' id 
fmap id id' 
id' 

... và lần thứ hai một quá:

-- 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 

Tôi cho rằng đó là như xa như chúng ta có thể nhận được. Năm luật mũi tên khác liên quan đến first và khi đường biên trái chỉ ra arr và first là độc lập.