[解決済み】代数的なデータ型の代数を悪用する - なぜこれが有効なのか？

質問

代数的なデータ型に対する「代数的」な表現は、数学のバックグラウンドを持つ人には非常に示唆に富むものに見えると思います。どういう意味か説明してみよう。

基本的な型を定義した上で

• 製品 •
• ユニオン +
• シングルトン X
• 単位 1

という略記を使用し X² に対して X•X と 2X に対して X+X などの代数的な表現を定義することができます。

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

と2分木があります。

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

さて、数学者としての私の最初の直感は、これらの式に夢中になり、次の式を解こうとすることです。 L と T . 代入を繰り返すことでもできますが、記法をひどく乱用して、自由に並べ替えられるように見せかける方がずっと簡単そうです。例えば、リンクリストの場合。

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

の冪級数展開を使っているところです。 1 / (1 - X) は、全く正当化されない方法で、興味深い結果を導き出しました。 L 型は Nil または、1つの要素を含むか、2つの要素を含むか、3つの要素を含むか、などです。

二分木でやるともっと面白くなる。

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

で行った)べき級数展開を使って、またもや ウルフラムアルファ ). これは、要素が1つの2分木、要素が2つの2分木（2番目の要素は左または右の枝にある）、要素が3つの5分木などが存在する、という（私にとって）明白ではない事実を表現しています。

そこで質問なのですが、私はここで何をしているのでしょうか？これらの操作は正当化されないように思えるが（ところで代数的データ型の平方根とはいったい何なのだろう）、賢明な結果をもたらす。2つの代数的データ型の商はコンピュータサイエンスにおいて何か意味があるのだろうか、それとも単なる表記上のトリックなのだろうか？

そして、おそらくもっと興味深いのは、これらのアイデアを拡張することは可能なのか、ということです。例えば、型に対する任意の関数を許容するような型の代数の理論はあるのだろうか、あるいは、型は冪級数表現を必要とするのだろうか？もし関数のクラスが定義できるのなら、関数の合成は何か意味があるのだろうか？

どうすれば解決するの？

免責事項：この多くは、⊥を考慮すると全くうまくいかないので、簡略化のために露骨に無視することにする。

最初のポイントをいくつか。

• なお、A+Bを表す言葉として、quot;union"はおそらく最適ではないでしょう--それは具体的には a 不一致 ユニオン の、型が同じでも両者は区別されるからです。ちなみに、より一般的な呼び方は、単に "和型" です。

• シングルトン型は、事実上、すべてのユニット型です。これらは代数的な操作のもとで同じように振る舞い、さらに重要なことに、存在する情報量はそのまま維持される。

• ゼロ型も欲しいところでしょう。Haskellはそれを Void . 型が0である値は存在せず、型が1である値も1つだけ存在する。

ここでまだ1つ大きな操作が抜けているのですが、それはまた後ほどご紹介します。

お気づきのように、Haskellはカテゴリー理論から概念を借りる傾向があり、上記はすべてそのように非常にわかりやすく解釈することができます。

• のオブジェクトA、Bが与えられたとき ハスク その積 A×B は、2つの投影を可能にする唯一の（同型までの）型である。 fst : A×B → A と スネーク : A×B → B, ここで、任意の型Cと関数が与えられると f : C → A となる。 g : C → B を定義すると、ペアリングは f &&& g : C → A×B このような fst ∘ (f &&& g) = f であり、同様に g . パラメトリック性は普遍的な性質を自動的に保証するものであり、私の微妙な名前の選び方でそのことがお分かりいただけると思います。その (&&&) 演算子が定義されています。 Control.Arrow ちなみに

• 上記の双対は、注入を伴う共積A+Bである inl : A → A+B および inr : B → A+B, ここで任意の型Cと関数が与えられると f : A → C となります。 g : B → C であれば、コペアリングを定義することができます。 f ||| g : A+B → C となり、明らかな同値が成立する。ここでもパラメトリック性が厄介な部分のほとんどを自動的に保証してくれる。この場合、標準的な注入は単に Left と Right であり、コペアリングは関数 either .

積型と和型の特性の多くは、上記から導き出すことができる。どんなシングルトン型でも、その末端オブジェクトは ハスク であり、空の型は初期オブジェクトである。

前述した欠落した操作に戻ると、alphaでは カルテシアン閉カテゴリ あなたは 指数オブジェクト であり、カテゴリの矢印に相当する。矢印は関数で、オブジェクトは種類 * で、その型は A -> B は、確かにBのように振る舞います。 ^A を、型の代数的操作の文脈で使うことができます。なぜそうなるのかが明らかでない場合は、次のような型を考えてみてください。 Bool -> A . 入力が2つしかない場合、この型の関数は、以下の型の2つの値に同型である。 A すなわち (A, A) . については Maybe Bool -> A のように、3つの入力が可能である。また、上のコペアリングの定義を代数的表記法に直すと、恒等式C ^A × C ^B = C ^A+B .

については なぜ というのは、上記の多くは、代数的な振る舞いを示すために、ある型の住民（その型を持つ異なる値）に言及しているからです。その観点を明示するために

• 製品タイプ (A, B) のそれぞれの値を表します。 A と B は、それぞれ独立にとられる。したがって、任意の固定値 a :: A という型の値が1つ存在します。 (A, B) の各住人に対して B . これはもちろんデカルト積であり、製品タイプの住民の数は要因の住民の数の積である。

• 和のタイプ Either A B のどちらかの値を表します。 A または B を、左右の枝を区別して表示します。前述の通り、これは不連続和であり、和型の住民の数は和集合の住民の数の和となる。

• 指数型 B -> A 型の値からのマッピングを表します。 B を型の値に変換します。 A . 任意の固定引数 b :: B の任意の値は A を代入することができます。 B -> A のコピーと同じ数の積に相当します。 A として B には住人がいるため、指数関数となる。

集合の標準的な和でなく不連続和があり、交差や他の多くの集合演算の明白な解釈がなく、集合のメンバーシップは通常気にしません（それはタイプチェッカーに任せます）。

一方、上記の構文では、多くの時間をかけて カウント 住民と 列挙 のように、ある型の取り得る値というのは、ここでは有用な概念である。その結果、すぐに 列挙型コンビナトリー リンク先のWikipediaを見ると、まず最初に、積や和の型と全く同じ意味で、quot;pairs" と "unions" を定義していることがわかります。 生成機能 そして、Haskellのリストと同一のquot;sequence"に対して、あなたが行ったのと全く同じテクニックを使って同じことを行います。

編集する あ、それから、このポイントを顕著に示すと思われる簡単なおまけがあります。コメントで、ツリー型に対して T = 1 + T^2 を導出することができます。 T^6 = 1 これは明らかに間違っている。しかし T^7 = T する を保持し、木と木の7タプルの間の双対射は直接構築することができます。 Andreas Blassのquot;Seven Trees in One"。 .

Edit×2: 他の回答で言及されている「ある型の派生物」の構造については、以下の記事もご参照ください。 同じ著者によるこの論文 は、このアイデアをさらに発展させ、除算の概念やその他の興味深いものを含んでいます。