Дали естествените трансформации, които прилагаме върху Coyoneda, за да получим Functor, всъщност са естествени трансформации?

Имам теоретичен въпрос относно природата на тип, който се използва в много примери, обясняващи лемата на Coyoneda. Те обикновено се наричат ​​"естествени трансформации", които, доколкото ми е известно, съпоставят между функтори. Това, което ме озадачава, е, че в тези примери те понякога картографират от 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 (тук == е равенство от 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