Hask圏における自然変換

#圏論とプログラミング

いつもの自然変換の図を具体的にHask圏に当てはめて考えてみる

https://gyazo.com/679bda9961cfcb26a11e26042b361605

型は全てHask圏の対象である

IdentityとかListはFunctor型クラスに属する型

その間の射が自然変換ηになる

自然変換といえど実体は射のあつまりなので個別に見てみると

$ \eta_\mathrm{Int}:: \mathrm{Int}\to[\mathrm{Int}]

$ \eta_\mathrm{Char}:: \mathrm{Char}\to[\mathrm{Char}]

$ \eta_\mathrm{Bool}:: \mathrm{Bool}\to[\mathrm{Bool}]

図には書いてないが

他にもたくさんある

これら一つ一つがそもそも射の集まりであり、これら全ての集まりが自然変換$ \etaになる

これらをHaskellで書くとこういう型の関数になるはず

code:hs

nat :: (Functor f, Functor g) => f a -> g a

aは多相で、natを選ぶ毎にf,gは固定になる

上図に合わせて具体的に書くとこうなる

code:hs

eta :: Identity a -> a

となり、個別の射の集まりに名前をつけるなら以下のようになる

code:hs

eta_int :: Identity Int -> Int

eta_char :: Identity Char -> Char

eta_bool :: Identity Bool -> Bool

Identity Int -> [Int]一つ取ってみても当てはまる関数はいくつも考えられる

code:hs

eta1 n = n

eta2 n = n*10

eta3 n = n+10

「射の集まり」になっていることがわかる

Identityは書かなくても同じなので(?)上の例はこうなる

code:hs

eta :: a -> a

ドメインもコドメインもIdentityだと考えればこういう関数も自然変換だということになる

code:hs

eta :: Identity a -> Identity a

eta :: a -> a

つまり、任意の多相関数は自然変換になる(?)

「任意の多相関数」は広く言いすぎかmrsekut.icon

ちなみにこういうのはだめ

code:hs

eta :: Identity a -> Identity b

aとbが異なっているのがだめ

Functorで挟む型は同じものでないといけない

逆にFunctorのネストした型も自然変換になる

code:hs

nat :: (Functor f, Functor g, Functor h) => f (g a) -> h a

だから例えば以下の関数は全て自然変換になる

code:hs

nat1 :: Identity a -> a

nat1' :: a -> a -- nat1と同じ

nat1'':: Identity (Identity a) -> a -- nat1と同じ

nat2 :: Maybe a -> a

ちなみにこれはだめ

code:hs

nat :: Maybe b -> a

可換に関して

https://gyazo.com/8007c085f7a66064a78f26b4638dfe15

自然変換は、ただの関手間の射なだけではだめで、圏論でよく見るあの正方形の図を可換にする必要がある

上図で言うなら、以下の等式が成り立つ必要がある

$ \eta_\mathrm{Char} . \mathrm{f} == \mathrm{fmap}(f) . \eta_\mathrm{Int}

この例では片方がIdentityなので一般化してHaskellで書くならこう

code:hs

eta_char . (fmap f) == (fmap f) . eta_int

左辺が緑の矢印、右辺が青色の矢印を表している

実際に試してみる

以下の様な自然変換の一部の関数の型を定義して

code:hs

import Data.Functor.Identity

import Data.Char

eta_int :: Identity a -> a

eta_int (Identity a) = a

f :: Int -> Char

f = toEnum

型を確かめてみると等しくなる

code:prelude

eta . (fmap f) :: Identity Int -> Char

(fmap f) . eta :: Identity Int -> Char

前者のetaはeta_charであり、後者はeta_intである

これを一つの自然変換etaで扱えるのである

挙動も等しくなる

code:hs

eta . (fmap f) $ 3 -- > "\ETX"

(fmap f) . eta $ 3 -- > "\ETX"

垂直合成を考えてみる

https://gyazo.com/8199e0292f0a05822cfbb4d0c5ea0d00

最初の図にFunctor型クラスのMaybeを追加した

ListからMaybeへの自然変換μをHaskellで書くとこうなる

code:hs

mu :: a -> Maybe a

先程と同様にaは任意の型が入る

HaskからHaskへの自然変換の垂直合成$ \mu\circ\etaを考える

code:hs

eta :: Identity a -> a

mu :: a -> Maybe a

このときmu . eta :: Identity a -> Maybe aとなる

https://gyazo.com/8c7dce5bc6ee7db96f1de8b496237ee0

可換性を考える

https://gyazo.com/31184795c0e6b978177c9dd29bb13b09

code:hs

mu_char . eta_char . (fmap f) -- 緑

mu_char . (fmap f) . eta_int -- 黄色

(fmap f) . mu_int . eta_int -- 青

これら3つの関数はどれもIdentity Int -> Maybe Charであり、実際同じ結果になる

例えばこんな感じ

code:hs

import Data.Functor.Identity

import Data.Char

import Data.Maybe

f :: Int -> Char

f = toEnum

-- eta

eta_int :: Identity Int -> Int

eta_int (Identity n) = n

eta_char :: Identity Char -> Char

eta_char (Identity c) = c

-- mut

mu_int :: Int -> Maybe Int

mu_int = listToMaybe

mu_char :: Char -> Maybe Char

mu_char = listToMaybe

一応水平合成も図だけ見ておこう

#WIP

https://gyazo.com/396dc5aec06ec702ce67268c29263789

これ全然違くね？mrsekut.icon

https://gyazo.com/b5f80b53cf94f998c8ea91fb02f24f98

こういうのだぞmrsekut.icon

ここでMonad型クラスの定義を参照する

code:hs

class Monad m where

(>>=) :: m a -> (a -> m b) -> m b

return :: a -> m a -- 自然変換

join :: m (m a) -> m a -- 自然変換

上の議論から明らかにreturnやjoinは自然変換であることがわかる

bindも自然変換だと書いている記事があったがよくわからない #?? ref

関数を関数モナドとしてみればなるのかと思ったがb出てきてるしやっぱわからん

code:hs

(>>=) :: m a -> (a -> m b) -> m b

↓

(>>=) :: (->) (m a) ((a -> m b) -> m b)

pursにData.NaturalTransformationというmoduleがある

https://pursuit.purescript.org/packages/purescript-prelude/3.1.0/docs/Data.NaturalTransformation

そこで(~>)という関数が定義されている ref

code:purs(hs)

type NaturalTransformation :: forall k. (k -> Type) -> (k -> Type) -> Type

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

上で議論した話と同じで特に難しいことはない

使用例はData.Listの中とか見ればちらほらある ref

これを

code:purs(hs)

head :: ∀ a. List a -> Maybe a

こうかける

code:purs(hs)

head :: List ~> Maybe

ただそれだけのことである

https://qiita.com/KNaito/items/aa03e156a9974d52e1e9

参考

https://wiki.haskell.org/Category_theory/Natural_transformation

https://qiita.com/KNaito/items/aa03e156a9974d52e1e9

https://bartoszmilewski.com/2015/04/07/natural-transformations/