Являются ли естественные преобразования, которые мы применяем к Койонеде, чтобы получить функтор, действительно естественными преобразованиями?

У меня теоретический вопрос о природе типа, который используется во многих примерах, объясняющих лемму Койонеды. Их обычно называют «естественными преобразованиями», которые, насколько мне известно, являются отображениями между функторами. Что меня озадачивает, так это то, что в этих примерах они иногда преобразуются из Set в некоторый функтор F. Так что на самом деле это не похоже на отображение между функторами, а что-то более расслабленное.

Вот код, о котором идет речь:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Coyo where

import           Data.Set (Set)
import qualified Data.Set as Set

data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

instance Functor (Coyoneda f) where
  fmap f (Coyoneda c fa) =  Coyoneda (f . c) fa

set :: Set Int
set = Set.fromList [1,2,3,4]

lift :: f a -> Coyoneda f a
lift fa = Coyoneda id fa

lower :: Functor f => Coyoneda f a -> f a
lower (Coyoneda f fa) = fmap f fa

type NatT f g = forall a. f a -> g a

coyoset :: Coyoneda Set Int
coyoset = fmap (+1) (lift set)

applyNatT :: NatT f g -> Coyoneda f a -> Coyoneda g a
applyNatT n (Coyoneda f fa) = Coyoneda f (n fa)

-- Set.toList is used as a "natural transformation" here
-- while it conforms to the type signature of NatT, it
-- is not a mapping between functors `f` and `g` since
-- `Set` is not a functor.
run :: [Int]
run = lower (applyNatT Set.toList coyoset)

Что я здесь не понимаю?

РЕДАКТИРОВАТЬ: После обсуждения #haskell в freenode я думаю, мне нужно немного прояснить свой вопрос. Это в основном: «Что такое Set.toList в теоретико-категориальном смысле? Поскольку это, очевидно (?) Не естественное преобразование».


haskell category-theory
person raichoo    schedule 31.07.2015    source источник

Ответы (1)


arrow_upward
13
arrow_downward

Чтобы n был естественным преобразованием в Haskell, он должен подчиняться (для всех f)

(fmap f) . n == n . (fmap f)

Это не относится к Set.toList.

fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = [0, 0, 0]
Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = [0]

Вместо этого он подчиняется другому своду законов. Существует еще одно преобразование n' в обратном направлении, так что выполняется следующее:

n' . (fmap f) . n == fmap f

Если мы выберем f = id и применим закон функторов fmap id == id, мы увидим, что это означает, что n' . n == id, и, следовательно, у нас есть аналогичная формула:

(fmap f) . n' . n == n' . (fmap f) . n == n' . n . (fmap f)

n = Set.toList и n' = Set.fromList подчиняются этому закону.

Set.map (const 0) . Set.fromList   . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = fromList [0]

Я не знаю, как мы можем это назвать, кроме как наблюдение того, что Set является классом эквивалентности списков. Set.toList находит представительного члена класса эквивалентности, а Set.fromList является частным.

Наверное, стоит отметить, что Set.fromList - естественная трансформация. По крайней мере, это разумная подкатегория Hask, где a == b подразумевает f a == f b (здесь _ 21_ является равенством от Eq). Это также подкатегория Hask, где Set - функтор; он исключает подобные вырожденные вещи.

leftaroundabout также отметил, что Set.toList является естественным преобразованием в подкатегории Hask, где морфизмы ограничены. в инъективные функции, где f a == f b означает a == b.

person Cirdec    schedule 31.07.2015
comment
В инъективной подкатегории даже toList является естественным преобразованием. - person leftaroundabout; 01.08.2015
comment
Спасибо за ответ! Значит, n' и n образуют здесь пару секция / отвод? - person raichoo; 01.08.2015
comment
@raichoo Да, n и n' - это целое семейство пар сечение / отвод, начиная с n' . n == id. Не все пары сечение / отвод будут подчиняться более строгому закону n' . fmap f . n == fmap f. - person Cirdec; 01.08.2015