Hask圏における自然変換
いつもの自然変換の図を具体的にHask圏に当てはめて考えてみる
型は全て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で書くとこういう型の関数になるはず
hsnat :: (Functor f, Functor g) => f a -> g a a は多相で、natを選ぶ毎に f,g は固定になる上図に合わせて具体的に書くとこうなる
hseta :: Identity a -> [a]となり、個別の射の集まりに名前をつけるなら以下のようになる
hseta_int :: Identity Int -> [Int]
eta_char :: Identity Char -> [Char]
eta_bool :: Identity Bool -> [Bool]
.. Identity Int -> [Int] 一つ取ってみても当てはまる関数はいくつも考えられるhseta1 n = [n]
eta2 n = [n*10]
eta3 n = [n+10]
..「射の集まり」になっていることがわかる
Identity は書かなくても同じなので(?)上の例はこうなるhseta :: a -> [a]ドメインもコドメインもIdentityだと考えればこういう関数も自然変換だということになる
hseta :: Identity a -> Identity a
eta :: a -> aつまり、任意の多相関数は自然変換になる(?)
「任意の多相関数」は広く言いすぎか
ちなみにこういうのはだめ
hseta :: Identity a -> Identity b a と b が異なっているのがだめFunctorで挟む型は同じものでないといけない
逆にFunctorのネストした型も自然変換になる
hsnat :: (Functor f, Functor g, Functor h) => f (g a) -> h a だから例えば以下の関数は全て自然変換になる
hsnat1 :: Identity a -> a
nat1' :: a -> a -- nat1と同じ
nat1'':: Identity (Identity a) -> a -- nat1と同じ
nat2 :: Maybe [a] -> aちなみにこれはだめ
hsnat :: Maybe b -> a可換に関して
自然変換は、ただの関手間の射なだけではだめで、圏論でよく見るあの正方形の図を可換にする必要がある
上図で言うなら、以下の等式が成り立つ必要がある
\eta_\mathrm{Char} . \mathrm{f} == \mathrm{fmap}(f) . \eta_\mathrm{Int}
この例では片方がIdentityなので一般化してHaskellで書くならこう
hseta_char . (fmap f) == (fmap f) . eta_int左辺が緑の矢印、右辺が青色の矢印を表している
実際に試してみる
以下の様な自然変換の一部の関数の型を定義して
hsimport Data.Functor.Identity
import Data.Char
eta_int :: Identity a -> [a]
eta_int (Identity a) = [a]
f :: Int -> Char
f = toEnum型を確かめてみると等しくなる
preludeeta . (fmap f) :: Identity Int -> [Char]
(fmap f) . eta :: Identity Int -> [Char]前者の
eta は eta_char であり、後者は eta_int であるこれを一つの自然変換
eta で扱えるのである挙動も等しくなる
hseta . (fmap f) $ 3 -- > "\ETX"
(fmap f) . eta $ 3 -- > "\ETX"垂直合成を考えてみる
最初の図にFunctor型クラスの
Maybe を追加した List から Maybe への自然変換μをHaskellで書くとこうなるhsmu :: [a] -> Maybe a先程と同様に
a は任意の型が入るHaskからHaskへの自然変換の垂直合成\mu\circ\etaを考える
hs eta :: Identity a -> [a]
mu :: [a] -> Maybe aこのとき
mu . eta :: Identity a -> Maybe a となる
可換性を考える
hsmu_char . eta_char . (fmap f) -- 緑
mu_char . (fmap f) . eta_int -- 黄色
(fmap f) . mu_int . eta_int -- 青これら3つの関数はどれも
Identity Int -> Maybe Char であり、実際同じ結果になる例えばこんな感じ
hsimport 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一応水平合成も図だけ見ておこう
これ全然違くね？
こういうのだぞ
ここでMonad型クラスの定義を参照する
hsclass Monad m where
(>>=) :: m a -> (a -> m b) -> m b
return :: a -> m a -- 自然変換
join :: m (m a) -> m a -- 自然変換上の議論から明らかに
return や join は自然変換であることがわかる関数を関数モナドとしてみればなるのかと思ったが
b 出てきてるしやっぱわからんhs(>>=) :: m a -> (a -> m b) -> m b
↓
(>>=) :: (->) (m a) ((a -> m b) -> m b)pursにData.NaturalTransformationというmoduleがある
そこで
(~>) という関数が定義されている refpurs(hs)type NaturalTransformation :: forall k. (k -> Type) -> (k -> Type) -> Type
type NaturalTransformation f g = forall a. f a -> g a上で議論した話と同じで特に難しいことはない
使用例はData.Listの中とか見ればちらほらある ref
これを
purs(hs)head :: ∀ a. List a -> Maybe aこうかける
purs(hs)head :: List ~> Maybeただそれだけのことである
参考