Skip to content

Instantly share code, notes, and snippets.

@aiya000

aiya000/catamorphism-with-nico.md

Created July 7, 2018 08:48
Show Gist options
  • Save aiya000/c5919ba4039376bdf0574ba3f68a25c7 to your computer and use it in GitHub Desktop.
Save aiya000/c5919ba4039376bdf0574ba3f68a25c7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
catamorphism-with-nico.md

矢澤にこ先輩と一緒にcatamorphism！

予防線

導入

にこ「おはよう〜、希」
希「お、にこっち。 おはようさん！」

希「にこっち〜、最近なんか面白いことあった」
にこ「ここのところはcatamorphismについて、Haskellで学んでたわ」
希「catamorphism ―カタモフィズム― ？」

にこ「catamorphismは圏の上での再帰の構造を持っていて、これをを使えばFunctor f制約だけで畳み込みができるの」
希「へ〜！」

希「面白そうやん。 うち、最近刺激がなくって暇なん。 詳しくおしえて〜な」
にこ「そうねえ、私の復習にもなるし、今日は暇だし。いいわよ」

にこ「にこはdata-fix1のhackageを見て学んだわ」
にこ「今回解説するコードの全文はこちら2よ」

流れについて

にこ「catamorphismはF-始代数っていうモノの上で表現されててね、F-始代数はF-代数っていうモノと一緒に考えられるの」
希「面白そうな名前がどんどん出てくるなぁ」

にこ「希もHaskellが好きよね。だからこんな流れで、対応するHaskellコードと一緒に説明していくわね」
希「Haskellいいやんな〜♪」

  1. F-代数について
  2. F-代数の準同型写像について
  3. F-始代数について
  4. catamorphismについて

F-代数をHaskellで表す

にこ「希はF-代数、知ってる？」
希「知らんなぁ。 モノイド、群、環とかの仲間？」
にこ「ううん。 F-代数は圏の上で考えられる構造だから、それらの代数的構造とは基本が違うかな」

にこ「まずF-代数のFは、ある自己関手Fのことなの」
希「HaskellのFunctor Fインスタンスやんな」
にこ「それそれ」

にこ「だから例えば自己関手Gに対してはG-代数…みたいに言ったりするわ」

にこ「F-代数は(Int, F Int -> Int)のような、対象と射の組なの」
希「F Int -> Intって不思議な射の形やね」
にこ「面白いところよね」

にこ「F-代数(X, F X -> X)を、言葉を乱用してF-代数Xとか言ったりもするわよ」

にこ「F-代数をHaskellの型クラスで表現してみると…こうね。 f a -> aがあればaの値も1つ以上あるはずだから、ここではobject :: aみたいなものは要請しないでおくわね」

-- | あるfに対するf-代数(a, f a -> a)の表現
class Functor f => FAlgebra f a where
  down :: f a -> a -- ^ あるf a -> aの値

にこ「今回はわかりやすくdownを型クラスに固定したけど、data-fix1パッケージは固定しない実装をしてたわね」

にこ「ここでそのインスタンスを定義する前に、catamorphismを扱う上でわかりやすい例としてList aを定義するわ」

-- |
-- `Cons 10 (Cons 20 (Cons 30 Nil)) :: List Int (List Int (List Int (List Int b)))`
-- のように型が再帰するリスト
data List a b = Nil | Cons a b
  deriving (Show)

にこ「Nil :: List a bなことに注意ね」

希「なんやすごい変な型やんね…要素数によって型が変わる？」

  • Nil :: List Int b
  • Cons 10 Nil :: List Int (List Int b)
  • Cons 10 (Cons 20 Nil) :: List Int (List Int (List Int b))

にこ「目の付け所がシャープね。さすが」
希「へへ。 …なんなんこれ？」
にこ「これは後でやる、F-始代数Fixっていうので扱うとちょうどそれらが同一の型で扱えるようになるの！」

希「それぞれ異なる型を持つ値を同一に扱える…ってすごいやんな」
にこ「型が再帰しているという限定的な状況下でのみの話だけどね。 そういうものとかをrecursion schemeとか言ったりするみたいね」

にこ「あとはこれのFunctorインスタンスが必要ね」

-- | List aがf-代数のfになれるようにする
instance Functor (List a) where
  fmap f x = case x of
    Nil      -> Nil
    Cons a b -> Cons a (f b)

にこ「あるaに対してのList a-代数を定義してみましょう。 …ここではList Bool-代数やList [String]-代数を任意のaとして、統一的にList a-代数と呼んでいくわね」

-- | List a-代数 (String, List a String -> String)
instance FAlgebra (List a) String where
  down :: List a String -> String
  down Nil = []
  down (Cons _ xs) = '0' : xs

-- | List a-代数 (Int, List a Int -> Int)
instance FAlgebra (List a) Int where
  down :: List a Int -> Int
  down Nil = 0
  down (Cons _ n) = n + 1

にこ「ここでList a-代数Intのdownの実装が後々大事になってくるわ。 これはF-始代数についてやるときに見ていきましょ」

希「ふむふむ」ｶﾀｶﾀｶﾀ

checkList :: IO ()
checkList = do
  let xs = Cons 10 (Cons 20 (Cons 30 Nil)) :: List Int (List Int (List Int (List Int ())))
  print xs
-- {output}
-- Cons 10 (Cons 20 (Cons 30 Nil))

希「なるほど、こういう感じの動きやんね」

F-代数の準同型写像をHaskellで表す

にこ「モノイド、群、環には準同型写像ってあったじゃない」
希「あったなぁ。 代数の醍醐味やんな」

にこ「そうよね〜。 F-代数も代数って言われるだけあって、やはり準同型写像が定義されるの」
希「さすがやんな！」

にこ「あるFunctor Fと型A,Bに対して、(a, A)から(b, B)への準同型写像は…こんな(fmap f, f)よ」

  • a : F A -> A
  • b : F B -> B
  • instance Functor F
  • (fmap f, f) :: (F A -> F B, A -> B)

falg-homo

にこ「f . a = b . fmap fを満す必要があるわ」
希「なるほど。 こんな太い矢印が準同型写像(fmap f, f)…っていうイメージであっとる？」

falg-homo-thin

にこ「ええ、まさにそれね」

にこ「Haskellのコードで表現すると、こんな感じかしらね」

-- | f-代数aからf-代数bへの準同型写像
data FHomo f a b = FHomo
  { higher :: f a -> f b
  , lower  :: a -> b
  }

-- |
-- スマートコンストラクタ。
-- 準同型写像はある`Functor f`と`a -> b`から導出できる。
fhomo :: Functor f => (a -> b) -> FHomo f a b
fhomo f = FHomo
            { higher = fmap f
            , lower  = f
            }

にこ「試しに、さっきのList a-代数StringとIntの準同型写像を定義してみるわ」

-- | List a-代数StringからIntの準同型写像
homoStringToInt :: FHomo (List a) String Int
homoStringToInt = fhomo length

にこ「aを適当なXに固定したList X-代数で可換図式を書くと、こうね」

list-alg-homo

にこ「homoCharIntがちゃんと法則を満たしているかは、これでチェックできるわ」

-- |
-- `FHomo f a b`の満たすべき法則
-- （Haskell上で確認するために、特別にEq制約を追加）
homoLaw :: forall f a b. (Functor f, Eq b)
            => FHomo f a b  -- ^ 検査の対象
            -> f a          -- ^ 始点
            -> FAlgebra f a -- ^ `f a -> a`
            -> FAlgebra f b -- ^ `f b -> b`
            -> Bool
homoLaw FHomo{..} fa FAlgebra{morph = downToA} FAlgebra{morph = downToB} =
  let overWay  = lower . downToA  :: f a -> b
      underWay = downToB . higher :: f a -> b
  in overWay fa == underWay fa

希「こんな感じかな？」

list-alg-homo-thin

にこ「その通り♪」

希「確認してみるなー。 本当はQuickCheck使うべきだと思うけど、今回は堪忍してや〜」

checkFHomo :: IO ()
checkFHomo = do
  let answer = homoLaw homoStringToInt Nil && homoLaw homoStringToInt (Cons () "xyz")
  putStrLn $ "Is homoStringToInt a valid homomorphism?: " <> show answer
-- {output}
-- Is homoStringToInt a valid homomorphism?: True

にこ「おっけーね」
希「おっけーやんっ」

F-代数の圏

にこ「F-代数とその準同型写像は圏を為すわ」
希「スピリチュアルやね！」

にこ「さっき希が書いてくれたこれを使わせてもらうと」

falg-homo-thin

にこ「あるF-代数の圏の可換図式としては、ちょうどこんな感じに書けるわね」

falg-category

にこ「aはa : F A -> A、F-代数の片割れね。 bも同じ」

にこ「List a-代数の方はこんな感じ」

list-alg-category

F-始代数をHaskellで表す

にこ「あとはF-始代数っていうのがわかれば、ついにcatamorphismについての下地は完了かな」
希「ふふ、これまた圏論っぽい感じの言葉やんね〜」

にこ「F-始代数はF-代数の圏の始対象なの」
希「始対象…任意の対象への射がちょうど1つずつある対象やったよね」

initial-object

にこ「それそれ。 例えば空集合から任意の集合にちょうど1ずつの写像が定義されるから、集合と写像の圏だと空集合が始対象ね」
希「うんうん」

にこ「F-代数の圏で、このFixのような始対象 ― F-始代数 Fix F ― を考えてみましょう。 (a, A)と(b, B)はさっき使ったF-代数ね」

list-alg-initial-object

にこ「実際Fixは任意のfに対して、このように定義できるわ。 まずはF-始代数の性質を見てから、それをこのFix fが満たしていることを確認しましょ」

-- | Fix f = f (Fix f)
newtype Fix f = Fix
  { unFix :: f (Fix f)
  }

希「このFixって、あの再帰関数を作るときに使うfix関数3と関連あるんかな？」
にこ「ええ、その名前を踏襲しているわ。 fix関数もとい不動点コンビネータfixはfix(f) = f(fix(f))が成立するもの4として説明されるけど、FixはまさにFix f = f (Fix f)ね」

希「ぐぬぬぬ…ちょっとむずかしいなぁ…」
にこ「わかるわ…にこも最初見た時に直感が追いつかなかったわ…。 recursion schemeの型々はむずかしいわよね」

にこ「大丈夫。 F-始代数の特性が理解できたら、わかりやすいと思わ」

F-始代数の特性

にこ「F-始代数はLambekの定理でF O ~ Oになるような(o : F O -> O, O)よ」
にこ「今回の~はいわゆる『同型を除いて一意』ってやつね」
にこ「ここで証明は省くけど5、Lambekの定理はそれを説明するわ」

希「同型を除いて一意？」
にこ「うん。 例えば…集合の圏では圏論が集合の中身について言及しないから、別の一元集合を区別できないの。 それについて{x} ~ {y}って表したりするわ」

希「わかったようなわからんような…」
にこ「ここでは『圏論的に同じ対象』っていうゆるい理解でもいいと思うわ」
希「ありがとう、わかりやすいやんな！」

にこ「ともあれF-始代数は、F : C -> Cの圏CでF O ~ OなOね」

falg-initial-iso

Fixに対する直感

希「Fix fっていう型やばない？ まだようわからんけど、無限再帰して止まらなさそうな…」
にこ「なるほど、それはつまりこういうことかしら」

-- | Fix版の値構築子Identity（これは定義できる）
identity :: Fix Identity -> Fix Identity
identity x =
  (Fix :: Identity (Fix Identity) -> Fix Identity) $
    (Identity :: Fix Identity -> Identity (Fix Identity)) x

-- もとい
identity = Fix . Identity

-- |
-- 適当なFunctorのIdentity。
-- Identityは基底部がないので値が定義できない！
x :: Fix Identity
x = identity (identity (identity (...?)))

-- 脱identity
x = Fix (Identity (Fix (Identity (Fix (Identity (...?))))))

希「ああ、なるほど、多分それや！」
にこ「わかる。 にこも最初直感がついていかなくてね、同じ感覚に陥ったわー」

にこ「Fix Fのような型の値を定義するには再帰の基底部になる値が必要…というのを意識してみたら、にこはこれを直感に落とし込めたわ」
にこ「例えばFix Maybeに対するNothing :: Maybe aのような、F aのaがパラメタリック多相でも定まるようなものね」

希「ふむふむ。 パラメタリック多相はforall a. aな、型クラス制約のない多相型のことやったよね」
にこ「ええ、そうよ」

にこ「試しにFix Maybeの値をいくつか定義してみるわ。 『値構築子Fixはforall a. Maybe (Maybe (Maybe a))やforall b. List a (List a (List a b))のようなネストした型を、Fix MaybeやFix (List a)のようなフラットな型に落とすことができるもの』…っていうことを念頭に置くとわかりやすいかと思う」

-- | Fix版の値構築子Nothing
nothing :: Fix Maybe
nothing =
  (Fix :: Maybe (Fix Maybe) -> Fix Maybe)
    (Nothing :: Maybe (Fix Maybe))

-- もとい
nothing = Fix Nothing

-- | Fix版の値構築子Just
just :: Fix Maybe -> Fix Maybe
just x =
  (Fix :: Maybe (Fix Maybe) -> Fix Maybe) $
    (Just :: Fix Maybe -> Maybe (Fix Maybe)) x

-- もとい
just = Fix . Just
-- |
-- Fix版（フラット版）の`Just (Just (Just Nothing)) :: Maybe (Maybe (Maybe (Maybe a)))`。
-- 再帰の基底部`Nothing :: forall a. Maybe a`のおかげで、値が定義できた！
x :: Fix Maybe
x = just (just (just nothing))

-- 脱nothing, 脱just
x = Fix (Just (Fix Nothing))

y :: Fix Maybe
y = just (just nothing)

z :: Fix Maybe
z = just nothing

希「おお、値できたやん！ 」

にこ「Maybe (Fix Maybe) ∈ forall a. Maybe a」
にこ「」

catamorphismを導出する

にこ「そしてf-始代数Fix fは始対象なので、任意のf-代数に準同型写像…もとい射があるわ」
希「ああ、さっき書いてた図のてんてんやじるしかな？」
にこ「ええ、破線の矢印ね」

list-alg-initial-object

にこ「ということでHaskellのコードとしてはこんなもんね」ｶﾀｶﾀｶﾀ

-- | f-始代数から任意のf-代数への射
homoFixToA :: forall f a. FAlgebra f a => FHomo f (Fix f) a
homoFixToA = fhomo f
  where
    f :: Fix f -> a
    f (Fix x) = down $ fmap f x

希「うーん…？」

lower homoFixToA :: Fix f -> a
= f

希「うわぁ、fmap fでfが再帰しとるんやね…f (Fix x)のパターンマッチはunFixに置き換えるとして、こうやんね」

f (Fix x) = down $ fmap f x :: Fix f -> a
    ↓
f = down . fmap f . unFix :: Fix f -> a

希「ふむふむ」ｶｷｶｷｶｷ

unFix :: Fix f -> f (Fix f)

fmap f :: f (Fix f) -> f a
down   :: f a -> a

fmap f . unFix :: Fix f -> f a
down . fmap f :: f (Fix f) -> a

希「！ 型fと型aをFとXに固定して、こうやんな」ｶｷｶｷ

catamorphism-composition

希「homoFixToAはちょうどf = down . fmap f . unFixっていう合成で作られとるんやね」
にこ「飲み込みがはやいわね…その通りよ！」

にこ「その書いてくれたHaskの可換図式を拡張して、F-代数の圏の可換図式でこう書くとこうなって…前に書いた(unFix, Fix F)と(a, A)と(b, B)の可換図式にちょうど合致するわね」
にこ「んっしょ、元あった(fmap f, f) : (a, A) -> (b, B)はgっていう名前に退避して…っと」

list-alg-catamorphism

希「おー！」
にこ「そして任意のXに対して、実際こうね」

list-alg-catamorphism-forall

catamorphismで畳み込みを行う

まとめ

おまけ

F-代数の圏をCategoryインスタンスにしてみる

その他参考記事

Footnotes

  1. https://hackage.haskell.org/package/data-fix-0.2.0/docs/Data-Fix.html ↩ ↩2

  2. https://github.com/aiya000/catamorphism-with-nico ↩

  3. https://ja.wikibooks.org/wiki/Haskell/不動点と再帰 ↩

  4. https://ja.wikipedia.org/wiki/不動点コンビネータ ↩

  5. Lambekの定理の内容についてはこの記事がわかりやすいと思うわ => https://qiita.com/karrym/items/62c46a2c7640912a1a28#lambek%E3%81%AE%E5%AE%9A%E7%90%86 ↩

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment