Haskell中的範疇之函子和自然變換
在上一篇Haskell中的範疇 - 知乎專欄文章中,介紹了範疇的一些基本概念。在這一篇中,我們將從單個範疇中走出來,建立範疇之間的態射,進而得到範疇的範疇。另外,由範疇之間的態射,得到函子,由函子之間的態射,得到自然變換,從而得到了函子範疇。這樣我們就一步步的得到了更多的範疇,有了更多好用的性質和代數結構,在函數式編程中有了更多的用處。
下面,我們先從函子開始吧。
- 函子
若我們將範疇看成是一個更高層的範疇的對象,則兩個範疇之間的態射就是函子。函子將範疇中的對象a變換為範疇中的對象F a,將範疇中的態射f變換為範疇中的態射F f,並保持了範疇的結構不變,即這兩個範疇都必須滿足範疇需要的定律。所以函子必須滿足如下的定律:
在Haskell中,函子用類型類Functor 以如下方式來約束。
class Functor f wheren fmap :: (a -> b) -> f a -> f bnnfmap id = id --保持單位元不變nfmap (f . g) = fmap f . fmap g --保持組合操作不變n
在Haskell的類型系統中,函子就是類型構造子,函子 F 將簡單類型a 構造為複雜類型 F a,將簡單類型的函數 f 變換為複雜類型的函數 F f,並滿足上面的函子定律。很常見的一個簡單的函子是Maybe,其將一個類型 a 變換為Maybe a,表示恰好有個類型 a 的值,或者什麼都沒有。函子Maybe的定義如下:
data Maybe a = Nothing | Just anninstance Functor Maybe wheren fmap :: (a -> b) -> Maybe a -> Maybe bn fmap f Nothing = Nothingn fmap f (Just a) = Just (f a)nn-- 推導 fmap id = idn fmap id Nothingn= Nothingn= id Nothingnn fmap id (Just a)n= Just an= id (Just a)nn-- 推導 fmap (f . g) = fmap f . fmap gn fmap (f . g) Nothingn= Nothingn= fmap f (fmap g Nothing)n= (fmap f . fmap g) Nothingnn fmap (f . g) (Just a)n= Just (f (g a))n= fmap f (Just (g a))n= fmap f (fmap g (Just a))n= (fmap f . fmap g) (Just a)n
由此可見,Maybe的定義滿足函子定律,因此是一個函子。
注意:類型構造子只有同時變換類型和函數,且滿足函子定律時,才是一個函子。
函子的用處是將簡單類型的函數通過類型構造子提升為複雜類型的函數,且不需要寫額外的代碼,使得一些基本函數可以應用到多種複雜數據類型的成員中,提高了這些基本函數的重用性。例如列表函子 [ ],其將普通函數 (*2) 提升為將列表中的所有數乘以2得到一個新列表的函數。
當函子連接的兩個範疇都是同一個時,即從一個函子到其自身的函子,稱為自函子。Haskell中的函子都是Hask範疇的自函子。
範疇有對偶性,因此對於任意一個函子,都存在一個函子,是一個對偶範疇到範疇的函子,稱為反變函子。我們前面介紹的函子也叫協變函子,反變函子與協變函子的不同是其改變了態射的方向,目標範疇與源範疇中的態射方向是相反的。
反變函子用類型類ContraFunctor 以如下方式來約束。
class ContraFunctor f wheren contramap :: (b -> a) -> f a -> f b --態射的方向是反的nncontramap id = id --保持單位元不變ncontramap (g . f) = fmap f . fmap g --改變了組合次序,從對偶範疇來看則 n --是保持組合操作不變n
態射是可以組合的,函子作為範疇之間的態射,那自然也是可以組合的。函子 F 和函子 G 組合後得到一個新函子 H,這三個函子的關係表示為。在Haskell中有如下的形式:
newtype Compose f g a = Compose {getCompose :: f (g a)} deriving (Show)nninstance (Functor f, Functor g) => Functor (Compose f g) wheren fmap k (Compose fga) = Compose $ fmap (fmap k) fgan
有時為了簡化書寫,我們也可以用符號:.: 來表示函子的組合操作。
type f :.: g = Compose f gn
常用的數據類型State s a的類型構造子State s就是由((->) s)函子和(, s)函子組合得到的函子。
newtype State s a = State { runState :: s -> (a, s) }nninstance Functor (State s) wheren fmap :: (a -> b) -> State s a -> State s bn --fmap f st = State $ fmap (fmap f) (runState st)n fmap f st = State $ s -> let (a, s) = runState st s in (f a, s)n
- 範疇的範疇(Cat範疇)
將範疇看成對象,函子就是範疇之間的態射。與單位態射相對應的,是單位函子,就是一個沒有任何改變的自函子,即有。任何函子與單位函子的組合都是其自身,即有和。
newtype Identity a = Identity { runIdentity :: a }nninstance Functor Identity wheren fmap f (Identity a) = Identity (f a)nn-- Identity a ? anidphi :: (Identity a) -> anidphi = runIdentitynnidpsi :: a -> (Identity a)nidpsi = Identitynn-- Compose f Id a ? f anfidphi :: Functor f => (Compose f Identity) a -> f anfidphi (Compose x) = fmap runIdentity xnnfidpsi :: Functor f => f a -> (Compose f Identity) anfidpsi fa = Compose (fmap Identity fa)n
函子的組合運算滿足結合律,多個函子組合時其結果和組合次序無關,即有
fphi :: (Functor f, Functor g, Functor h) =>n (Compose (Compose f g) h) a -> (Compose f (Compose g h)) anfphi (Compose (Compose fg_ha)) = Compose (fmap Compose fg_ha)nnfpsi :: (Functor f, Functor g, Functor h) =>n (Compose f (Compose g h)) a -> (Compose (Compose f g) h)) anfpsi (Compose (Compose f_gha)) = Compose (Compose (fmap getCompose f_gha))n
這樣我們就有了範疇的範疇,記為Cat範疇,這也是範疇論被稱為貓論的由來。在Cat範疇中,對象是範疇,態射是函子,函子的組合滿足結合律,單位元是單位函子。
- Hom函子
任意範疇中兩個對象 a 和 b 之間的所有態射組成的集合叫Hom-Set,記為。範疇中的所有Hom-Set在一起組成了一個Set範疇,我們可以看到範疇和這個Set範疇之間存在態射,就是協變Hom函子。
在中,如果把對象 a 固定,對象 b 是任意可變的,那我們就得到了,這是一個從範疇到Set範疇的函子,我們稱之為協變Hom函子。
instance Functor ((->) a) wheren fmap f g = f . gn
在中,如果把對象 b 固定,對象 a 是任意可變的,那我們就得到了,這是一個從範疇到Set範疇的函子,我們稱之為反變Hom函子。
instance ContraFunctor (Op a) wheren contramap f (Op g) = Op (g . f)n
協變Hom函子和反變Hom函子使得範疇中的對象可以在Set範疇中表示出來,這是很有意義的事情,後續我們將會具體介紹這些意義和用處。
在中,如果對象 a 和對象 b 都是任意可變的,那我們就得到了,這是一個從範疇到Set範疇的二函子,我們稱之為Hom函子。這個我們後續會再次介紹。
- 自然變換
若我們有函子 F 和函子 G, 都是範疇到範疇之間的函子。那麼對於範疇中的任意對象 a,則在範疇中分別有對應的對象F a 和G a,F a和G a之間存在函數。對於範疇中的任意對象 b,則在範疇中分別有對應的對象F b和G b,F b和G b之間存在函數。如果函數和滿足一致性關係,即對於範疇上的態射,滿足交換關係,則稱變換是函子 F和 G的自然變換。
在Haskell中,我們用如下的方式來定義自然變換。
newtype Nat f g = Nat {runNat :: forall a. f a -> g a }n
這個定義沒有一致性關係的約束,需要程序員在定義具體的自然變換時確保其滿足如下所示的一致性關係。這是Haskell相比Idris弱的地方。
phi :: Nat f gnphi . fmap k = fmap k . phi --一致性關係n
自然變換實際上就是由函子 F 和 G 確定的範疇上的一組態射族,這組態射族由範疇中所有的 a 得到的範疇中的對象對之間的態射組成,而且這些態射都必須滿足自然變換的一致性關係。
如果自然變換的函數是一個同構態射,也就是對象和是同構的,且對範疇中所有的 a 都成立,那自然變換就是一個自然同構。且自然變換t 存在一個相反的自然變換。
在Haskell中有很多常見的自然變換的例子,下面列出了幾個。
safeHead 函數是列表函子到Maybe函子到自然變換
safeHead :: [a] -> Maybe ansafeHead [] = NothingnsafeHead (x:xs) = Just xnn---- 一致性關係 ----nsafeHead . fmap k = fmap k . safeHeadnn---- 一致性關係的證明 ----n safeHead (fmap k [])n= safeHead []n= Nothingnn fmap k (safeHead [])n= fmap k Nothingn= Nothingnn safeHead (fmap k [a, b])n= safeHead [(k a), (k b)]n= Just (k a)nn fmap k (safeHead [a, b])n= fmap k (Just a)n= Just (k a)n
maybeToList函數是Maybe函子到列表函子的自然變換
maybeToList :: Maybe a -> [a]nmaybeToList Nothing = []nmaybeToList Just a = [a]nn---- 一致性關係 ----nmaybeToList . fmap k = fmap k . maybeToListnn---- 一致性關係的證明 ----n maybeToList (fmap k Nothing)n= maybeToList Nothingn= []nn fmap k (maybeToList Nothing)n= fmap k []n= []nn maybeToList (fmap k (Just a))n= maybeToList (Just (k a))n= [k a]nn fmap k (maybeToList (Just a))n= fmap k [a]n= [k a]n
reverse函數是列表函子到其自身的自然同構,reverse函數沒有改變列表的形狀(即列表的長度),是一個同構函數。
reverse :: [a] -> [a]nreverse [] = []nreverse (x:xs) = reverse xs ++ [x]nn---- 一致性關係 ----nreverse . fmap k = fmap k . reversenn---- 一致性關係的證明 ----n reverse (fmap k [a, b, c])n= reverse [k a, k b, k c]n= [k c, k b, k a]nn fmap k (reverse [a, b, c])n= fmap k [c, b, a]n= [k c, k b, k a]n
- 自然變換的組合
自然變換可以看成是函子之間的態射,因此也是可以組合的。
若函子F、函子G 和函子H 都是範疇到範疇的函子,是函子F 到函子G 的自然變換,是函子G 到函子H 的自然變換。則我們可以將和組合起來,得到一個新的自然變換,這個組合又稱為自然變換的垂直組合。
自然變換的垂直組合的Haskell表示如下。
vertComp :: (Functor f , Functor g, Functor (h :: k -> *))n => Nat g h -> Nat f g -> Nat f hnvertComp beta@(Nat gh) alpha@(Nat fg) = Nat $ gh . fgn
自然變換的垂直組合本質上就是態射的組合,因此是滿足結合律的。
gamma `vertComp` (beta `vertComp` alpha)n= Nat hk `vertComp` (Nat gh `vertComp` Nat fg)n= Nat ( hk . (gh . fg))n= Nat ((hk . gh) . fg )n= (Nat hk `vertComp` Nat gh) `vertComp` Nat fgn= (gamma `vertComp` beta) `vertComp` alphan
若函子F、函子F 是範疇到範疇的函子,函子G、函子G『是範疇到範疇的函子,是函子F 到函子F 的自然變換,是函子G 到函子G 的自然變換。我們也可以將和組合起來,得到一個新的自然變換,這個組合又稱為自然變換的水平組合,這裡我們用和垂直組合不同的符號來表示水平組合。
自然變換的水平組合的Haskell表示如下。
horzComp :: (Functor f, Functor f, Functor g, Functor g)n => Nat g g -> Nat f f -> Nat (g :.: f) (g :.: f)n -- gg :: g a -> g an -- ff :: f a -> f an -- gfa :: g (f a)n -- fg x :: f (g a)n -- fmap ff :: g (f a) -> g (f a)nhorzComp beta@(Nat gg) alpha@(Nat ff)n = Nat $ (Compose gfa) -> Compose (fmap ff (gg gfa))n
自然變換的水平組合本質上是函子的組合,因此也滿足結合律。
gamma `vertComp` (beta `vertComp` alpha)n= Nat hk `vertComp` (Nat gh `vertComp` Nat fg)n= Nat (Compose . fmap (fmap fg . gh) . hk . getCompose)n= Nat (Compose . (fmap (fmap fg) . fmap gh) . hk . getCompose)n= Nat (Compose . fmap (fmap fg) . (fmap gh . hk) . getCompose)n= (Nat hk `vertComp` Nat gh) `vertComp` Nat fgn= (gamma `vertComp` beta) `vertComp` alphan
垂直組合和水平組合是可以混合在一起的,即垂直組合後得到的自然變換也可以再次與其他自然變換水平組合,同樣的,水平組合後得到的自然變換也可以再次與其他自然變換垂直組合。
垂直組合和水平組合是可以互換的,先垂直複合再水平複合與先水平複合再垂直複合所得到的結果是相等的 ,即有,我們稱之為自然變換的垂直水平互換定律。
我們再來看一個特殊的自然變換的水平組合,一個函子F和自然變換的水平組合, 可以將其看成是函子F 上的恆等自然同構和自然變換的水平組合。
當自然變換在前面時,稱這個組合是前置水平組合,其形式為,定義為,有時為了更簡明些,前置水平組合簡記為。Haskell中表示如下。
preFComp :: (Functor f, Functor g, Functor h)n => Nat g h -> g (f a) -> h (f a)npreFComp (Nat gh) fa = gh fan
當自然變換在後面時,稱這個組合是後置組合,其形式為,定義為,有時為了書寫更簡明,後置水平組合簡記為。Haskell中表示如下。
postFComp :: (Functor f, Functor g, Functor h)n => Nat g h -> f (g a) -> f (h a)npostFComp (Nat gh) fa = fmap gh fan
自然變換的水平組合可以直觀的認為其擴展了自然變換的寬度,由單個函子之間的自然變換擴展為多個函子組合後的函子之間的自然變換。我們前面提到的Cat範疇就是由函子的組合得來的,自然變換的水平組合使得組合後的函子也是存在自然變換的。
自然變換的垂直組合則可以直觀的認為其擴展了自然變換的深度,由兩個函子之間的自然變換擴展為跨越多個函子的自然變換,多個函子都可以通過自然變換聯繫起來。若我們將函子看成對象,那就通過自然變換的垂直組合得到了函子範疇。
- 函子範疇
範疇到範疇之間的所有函子組成了一個函子範疇,對象就是範疇到範疇之間的函子,態射就是這些函子之間的自然變換,態射的組合操作就是自然變換的垂直組合。單位元就是函子上的恆等自然同構,結合律可以由自然變換的垂直組合的結合律得到。
在Haskell中,函子範疇的定義如下:
instance Category Nat wheren id = Nat idn Nat f . Nat g = Nat (f . g)n
函子範疇是一個非常基礎的概念,在後續的文章中將會多處用到這一概念。將這裡介紹的函子和自然變換的概念理解透徹後,會對後續的學習非常有利。
學習了這一章的內容後,特別是自然變換的垂直組合、水平組合的概念,已經有了理解單子這個概念的基礎了。不過先別急,在介紹單子之前,我們先看點其他東西吧。
本章到此結束,意猶未盡的朋友請等待下一篇:範疇上的代數結構
推薦閱讀:
※什麼是函數式語言?
※函數式編程能否解決所有經典的演算法問題?
※請問大家了解函數式語言編譯器的實現技術嘛?
※宏展開與衛生宏展開