Zenn
🔄

`Free f a` 型は `f + Const a` 函手の不動点と同型であるお話

2024/12/20に公開
Haskell
関数型プログラミング
圏論
math
tech

この記事の位置付け

みなさま、お疲れ様です！企画開発エンジニア の高瀬 (@Guvalif) です。この記事は、ドワンゴ Advent Calendar 2024 における、20 日目の記事です。

https://qiita.com/advent-calendar/2024/dwango

突然ですが、みなさん "型" は好きですか？

自分の場合は、「型を ｶﾞﾁ ｶﾞﾁ にして、モデルを純粋にして、自己ドキュメント化されたコードを書く」ことを意識できれば、大抵のことはなんとかなると思っている節があるので、型には足を向けて眠れません 🛌[1]

さて、そんな型に関して、先日こんな Post を 𝕏 上で目にしました：

https://x.com/yukikurage_2019/status/1866867774263529558

めちゃくちゃ興味深いことが書いてあるのに、Like ❤️ 数が少なすぎると思いませんか？(圧強め) ぜひ理解したいですよね？Step by Step で理解していきましょう！

Free f a 型ってどんなもの？

f を適当な Functor 型クラスのインスタンスとして、Free f a は次のような代数的データ型で表現することができます：

-- Functor (f :: * -> *) =>
data Free f a = Pure a
              | Free (f (Free f a))
--              ^^^^
--              この部分は "引数を 1 つ" 取るデータ構築子
--              なおかつ、データ構築子には `f (Free f a)` 型の値を渡すことができる

すなわち、Pure によって構築された値か、Free によって構築された値のいずれかを持てる 直和型 であり、かつ再帰的な型定義を持つものです。

本題から逸れるため深く解説はしませんが、Free f a において、f を適当に取り替えながら再帰的に構造を積み重ねることができるため、少なくとも 順次・反復 を代数的データ型として表現できることがわかります。もし Monad 型クラスのインスタンスにできれば[3]、>>= 演算子によって 分岐 も表現できるため、一種の DSL: Domain Specific Language として利用する例も作れたりします 💡

f + Const a 函手ってどんなもの？

f は既知なので、まずは Const a に着目すると、次のような函手で表現することができます：

-- `(Const a) x = a`, すなわち任意の対象を "a" にマッピングする
newtype Const a x = Const { getConst :: a }

instance Functor (Const a) where
    -- `fmap f = id`, すなわち任意の射を "恒等射" にマッピングする
    fmap _ (Const a) = Const a

端的に言えば、ある構造を、対象 a とそれに備わる恒等射 id_a の一点に潰すような函手です。

そして、f + Const a は 函手の直和 を意味し、Haskell では Data.Functor.Sum に定義が存在します。「函手の直和とは ...？🤔」と一瞬考えるかもしれませんが、Either の要領で 2 種類 ( InL と InR ) に値を振り分け、函手の適用をそれぞれに分配している[4]だけなので、そんなに難しいことは行っていないです 📝

函手の "不動点" ってどんなもの？

まず 不動点 とは、ある写像 f に対して、x^* = f(x^*) を満たすような x^* のことです。単項カインドも写像と捉えると、次の要領で不動点を表現することができます：

-- `out . In = id` より、`Fix f = f (Fix f)` という等式とみなせる
-- これより、`Fix f` は不動点の定義を満たす
newtype Fix f = In { out :: f (Fix f) }

さて、g = f + Const a とおいて、不動点 Fix g を具体的に計算してみましょう：

Fix g = g (Fix g)
      = (f + Const a) (Fix (f + Const a)) -- ※ 函手の直和に型を適用
      = InL (f (Fix (f + Const a)))
      | InR (Const a (Fix (f + Const a)))
      = InL (f (Fix (f + Const a)))
      | InR a                             -- ※ (Const a) x = a より

この最終結果に対して、Free f a となんらか関係を見出せれば、本記事のゴールに辿り着きます 🏃‍♂️🏃‍♀️

"同型" ってどういうこと？

まず 同型 とは、一対一対応を考えられる[5] ことです。つまり、次の 2 つの主張は等価です 💡

  • 「Free f a 型は f + Const a 函手の不動点と 同型 である」
  • 「Free f a 型と f + Const a 函手の不動点には、一対一対応を考えられる」

では実際に、式変形をしながら一対一対応を考えられるか見てみましょう：

-- `Fix g = Fix (f + Const a) = Free' f a` とおく，これより ...
Free' f a = Fix g
          = InL (f (Fix (f + Const a)))
          | InR a
          = InL (f (Free' f a))
          | InR a
          -- `InR = Pure`, `InL = Free` とおくと ...
          = Pure a
          | Free (f (Free' f a)) -- 完成！🎉

... というわけで、無事冒頭の Post に書かれた主張を示すことができました 🥳 (めでたしめでたし)

まとめ

型 (や Haskell) はどうしても抽象的な話題が多いように見えますが、一歩ずつ紐解けば意外とシンプルな主張であることも多いです。ところでこの記事を読んだら、なんだかもっと関連分野の勉強がしたくなってきましたよね？？(ﾎﾝﾏｶ？)

そんな社外のあなたに ...

関数型プログラミングのカンファレンスに来たら、きっといっぱい勉強できます 🚀 (ダイレクトマーケティング)

https://2025.fp-matsuri.org/

そんなドワンゴ社内のあなたに ...

#functional という Slack チャンネルで細々と呟いているので、ぜひ賑やかしにでも来てください 🫠 (2024-12-20 現在、13 人しか参加者がいなくてな ...)

脚注

  1. すべてのプログラミング言語に、Hoogle が用意されていたら良いのに ... ↩︎

  2. 本記事で扱う函手は、型とプログラムの圏における 自己函手 が正確です ↩︎

  3. 実際、これは可能 です ↩︎

  4. そのような実装が函手の定義を満たすかは、実際に計算して確かめてみても良いでしょう 💪 ↩︎

  5. 圏論的に正確な表現は、2 対象の間に射と逆射が備わっている ですが、入門 (？) 記事なので目を瞑ってください 🙏 ↩︎

GitHubで編集を提案

Discussion