F-始代数の可換図式とFixF型の対応

結論

https://gyazo.com/c79c637ba446fc1489789991d5f22c73

これら2つの対応

F-始代数の可換図式

https://gyazo.com/153c9471a252753bf9c91fc5ca9b1839

HaskellのFixF型

code:hs

newtype FixF f = InF { outF :: f (FixF f) }

なお、下記のようにFix型を定義しても全く同じである

code:hs

newtype Fix f = Fix (f (Fix f))

直観的にはこういうことを書きたい

code:hs

FixF f ≅ f (FixF f)

μF

関手 F の最小不動点

code:hs

FixF f

これは、f を無限に展開してできる最小の再帰型になる

code:hs

FixF f

= f (FixF f)

= f (f (FixF f))

= f (f (f (...)))

inF

$ \mathsf{in}F: F(\mu F)\to \mu F

再帰構造を 1層包むコンストラクタ

code:haskell

InF :: f (FixF f) -> FixF f

outFはinFの逆射

$ \mathsf{in}F^{-1}: \mu F\to F(\mu F)

code:haskell

outF :: Fix f -> f (Fix f)

outF (Fix x) = x

下記が成り立つ

code:haskell

InF :: f (FixF f) -> FixF f

outF :: FixF f -> f (FixF f)

InF . outF = id

outF . InF = id

$ μF ≅ F(μF)という不動点性をコードで表現したもの

$ \varphi: F(X)\to X

code:haskell

type Algebra f a = f a -> a

cata(φ)

これがCatamorphism

$ f: \mu F\to Xとすると、f = cata phiと書ける

可換図式をそのままコードにすることで

https://gyazo.com/8ea9d2a20ad560a28028a734a44a4c32

code:haskell

cata :: Functor f => Algebra f a -> Fix f -> a

cata phi = phi . fmap (cata phi) . outF -- ★ = ③ . ②　. ①

下記のように定義されることもあるが同じである

code:hs

cata :: Functor f => Algebra f a -> Fix f -> a

cata phi (Fix x) = phi (fmap (cata phi) x)

下記が成り立つ

code:hs

f . InF = phi . fmap f