代数的データ型と Combinatorial Species
これは「Haskell Advent Calendar 2024」9日目の記事です。
代数的データ型は簡潔性を保ちながら型安全で表現力豊かなプログラムを記述するため欠かせない存在です。代数的データ型の原型は1966年にLandinが提案したISWIMに見られます。その後、1977年にNPLという関数型プログラミング言語に実装され、Standard MLやMiranda、Haskellに実装されていきました[1]。Haskellにおいて代数的データ型は型の 直和 と 直積 が表現でき、再帰的な定義 (再帰データ型)も可能です。
-- 直和型(Either a b と等価)
data Sum a b = A a | B b
-- 直積型(タプル (a, b) と等価)
data Product a b = Product a b
-- 再帰データ型の例
data List a = Nil | Cons a (List a)
この直和と直積という演算を持っていることが代数的データ型が "代数的" と呼ばれる所以ですが、これらの操作が本当に和と積に対応していることを直感的に理解することは可能でしょうか?例えばryota-ka氏の『代数的データ型と初等代数学』では基本的な代数的データ型に
型 | 集合 | 要素の数 |
---|---|---|
data Void |
||
data One = One |
||
type Two = Sum One One |
||
data Maybe a = Nothing | Just a |
||
data Sum a b = A a | B b |
||
data Product a b = Product a b |
||
a -> b |
(ここで
本稿ではこの
- 型から
- 集合に対応付け
- 要素の数を数える
という翻訳の流れを参考に、集合ではなく Combinatorial Species という概念を考えることで、代数的データ型に対するまた別の見方ができることを紹介したいと思います。
Combinatorial Species
有限集合を対象とし全単射を射とするような圏
例えば集合にその部分集合族を対応させるような関手は Combinatorial Species の例です。他にも集合にその要素を頂点とするグラフ全ての集合を対応させる関手や集合にその要素をノードとする木構造全ての集合を対応させる関手も Combinatorial Species と考えることができます。
Combinatorial Species
Combinatorial Species
を対応付けることができ、この多項式は 母関数(指数型母関数) と呼ばれます。ここで
例えば
となります。
代数的データ型の翻訳
Haskell の代数的データ型を Combinatorial Species に対応付ける 方法を考えてみましょう。Combinatorial Species は関手なので例えば次のような Functor
にできる一般的な型を考えましょう。
data F a = A | B1 a | B2 a | C a a | D a a a
この型 F
に対応する Combinatorial Species
- 空集合に対しては1点集合
を対応させA - 1点集合に対しては、その集合でラベル付けられた構造
を持つ2点集合を対応させB_1, B_2 - 2点集合に対しては、その集合でラベル付けられた構造
を持つ2点集合を対応させ(構造は1つですがラベルの組み合わせが2通りあるので2点集合)C - 3点集合に対しては、その集合でラベル付けられた構造
を持つ6点集合を対応させ(構造は1つですがラベルの組み合わせが6通りあるので6点集合)D - それ以外の集合に対しては空集合を対応させる
ような関手を考えることとします。
この
となります。
なんとなく翻訳のルールは分かるかもしれませんが、議論を明確にするためにここからは基本的な型とそれに対応する Combinatorial Species を定義し、それらを代数的に組み合わせることでより複雑な対応をカノニカルに構築していく方法を考えたいと思います。
Regular Species
まず最も基本的な型は値コンストラクタを持たない型でしょう。
data Void a -- 実装は空
この型に対応する Combinatorial Species は 任意の集合を空集合に対応付ける関手 で、その母関数は
となります。この Combinatorial Species を
次に基本的な型として以下のような1つの値コンストラクタを持つような型を考えます。
data One a = One
この型に対応する Combinatorial Species は 空集合を1点集合に対応付けそれ以外の集合を空集合に対応付ける関手 で、その母関数は
となります。この Combinatorial Species を
Combinatorial Speceis との対応を考えるためにここでの代数的データ型は型変数 a
を取る形になっていましたが、型 Void a
と One a
における a
は幽霊型であり Void a
は Data.Void
の Void
, One a
はUnit型 ()
に同型です。ですので型変数がない代数的データ型についても Void a
, One a
と同型な型の組み合わせと考えることにより Combinatorial Species との対応を考えることができます。
最後に次のような型を考えます。
data X a = X a
この型に対応する Combinatorial Species は 1点集合を1点集合に対応付けそれ以外の集合を空集合に対応付ける関手 で、その母関数は
となります。この Combinatorial Species を
ここからは代数的データ型の直和と直積に対応する Combinatorial Speceis の演算を考えます。
まずは以下のような 代数的データ型 f
と g
の直和 を表す型を考えます。
data Sum f g a = Inl (f a) | Inr (g a)
Sum f g a
に対応する Combinatorial Speceis は、 f
と g
に対応する Combinatorial Speceis の直和です。Combinatorial Speceis
に写すような関手です(射の対応についても素直に定義します)。定義より
次に以下のような 代数的データ型 f と g の直積 を表す型を考えます。
data Product f g a = Product (f a) (g a)
Product f g a
に対応する Combinatorial Speceis は、 f
と g
に対応する Combinatorial Speceis の 種積 (Species Product) と呼ばれる掛け算です。Combinatorial Speceis
と写すもので、和は集合
ここで一旦これまでに定義した Combinatorial Species
まず
type Two a = Sum One One a
という型を考えましょう。この型は以下のように Bool
と同型であることが分かります。
twoToBool :: Two a -> Bool
twoToBool (Inl One) = False
twoToBool (Inr One) = True
boolToTwo :: Bool -> Two a
boolToTwo False = Inl One
boolToTwo True = Inr One
Two a
は2つの One a
の直和なので対応する Combinatorial Species
となります。この Combinatorial Species
次に
type Succ a = Sum One X a
という型を考えましょう。この型は以下のように Maybe a
と同型であることが分かります。
succToMaybe :: Succ a -> Maybe a
succToMaybe (Inl One) = Nothing
succToMaybe (Inr (X a)) = Just a
maybeToSucc :: Maybe a -> Succ a
maybeToSucc Nothing = Inl One
maybeToSucc (Just a) = Inr (X a)
Succ a
に対応する Combinatorial Species は
です。
ここで Combinatorial Species
となります。ここで
Haskellの型としても以下のような合成を対応付けます。
data Compose f g a = Compose (f (g a))
これを使って Compose Succ Two a
という型を考えると、この型は Maybe Bool
に同型であり、対応する Combinatorial Species は
他にも種積の例として Product Two X a
に対応する Combinatorial Species は Product X X a
に対応する Combinatorial Species は
ところでHaskellの代数的データ型では再帰的な定義が可能でした。例えば標準的なリストの型
data List a = Nil | Cons a (List a)
に対応する Combinatorial Species を考えることはできるでしょうか?このような再帰データ型の定義は型の最小不動点を取る操作と考えることができます。
これまでの考え方に基づくとこの List a
に対応する Combinatorial Species
という同型対応が成り立つはずです。実は Combinatorial Species には Implicit Species Theorem [3]という定理がありこのような式を満たす Combinatorial Species の存在が保証されています。この定理によって存在が保証される Combinatorial Species を データ型の最小不動点に対応する Combinatorial Species と考えることにしましょう。上記式から
と書けることが分かります。
以上における Combinatorial Species
代数的データ型の微分
Combinatorial Species には 微分 という操作を考えることができます。Combinatorial Species
つまり
いくつかの例を見てみましょう。
まず Combinatorial Species
です。
次に Combinatorial Species
そして Combinatorial Species
今度は直和の微分を考えてみましょう。定義より
となるので Combinatorial Species
次に種積の微分は定義より
となりライプニッツ則が成り立つことが分かります。2行目から3行目へは
更に合成の微分は
となり合成関数の微分法が成り立つことが分かります。2行目から3行目は
これらの例と母関数の対応を考えることにより Combinatorial Species の微分の母関数は元の母関数の微分に対応する ことも分かるでしょう。
さてこの Combinatorial Species の微分を用いて 代数的データ型の微分 を考えましょう。すなわち代数的データ型の微分を元の代数的データ型に対応する Combinatorial Species を微分した Combinatorial Species に対応する代数的データ型とするのです。
例えば List a
に対応する Combinatorial Species
となり List a
の微分は (List a, List a)
に同型な型であることが分かります。実はこれは List a
の Zipper と同じ型になっており、一般にデータ型の Zipper を得る操作はデータ型を微分していると解釈することができます[5]。
まとめ
以上の話より以下のような対応表が書けることが分かりました。
型 | Combinatorial Species | 母関数 |
---|---|---|
data Void |
||
data One = One |
||
type Two = Sum One One |
||
data Maybe a = Nothing | Just a |
||
data Sum a b = A a | B b |
||
data Product a b = Product a b |
||
data Compose f g a = Compose (f (g a)) |
||
データ型Fの微分 |
代数的データ型に対応する多項式を Combinatorial Species を経由してから母関数として得ることで ラベル付けられた構造の集合という直感的なイメージを持ちながら微分といった深い構造にも言及できるようになる のが、Combinatorial Species として考えることの面白さの一つかと思います。
この解釈の欠点を挙げるとすれば関数の型 a -> b
に言及できていないことがあるかもしれません。定数から定数への対応なら同型対応を使ってなんとか考えられるかもしれませんが、一般には対応する母関数の演算が
他にも Combinatorial Species には色々な拡張が考えられており、複数の引き数を取れるにように拡張した Multisort Species(Implicit Species Theorem を厳密に述べるためにも必要。偏微分も定義できる)や、足し算だけでなく引き算も考えられるように拡張した Virtual Species や[6]、Combinatorial Species の左Kan拡張として Analytic Functor (ドメインが有限集合の圏
最後に、もし今回の話に興味があれば以下の文献を読むのがおすすめです。
挿絵イラスト: Loose Drawing
\読んでいただきありがとうございました!/
この記事が面白かったら いいね♡ をいただけると嬉しいです☺️
バッジを贈っていただければ次の記事を書くため励みになります🙌
-
基本的な型を考えている限り型を集合と捉えることはうまくいきますが、例えば
T a = (a -> Bool) -> Bool
という関手の不動点を考えると濃度に関する議論がうまくいかなくなるといった例外があり(Polymorphism is not set theoretic)一般的には型と集合は異なるものです ↩︎ -
A quick introduction to species, operads, and closed multicategories ↩︎
Discussion