代数データ型の「代数的」表現は、数学のバックグラウンドを持つ人にとっては非常に示唆に富んでいるように見えます。私が何を意味しているか説明してみたいと思います。
基本的なタイプを定義した
- 製品
• - 連合
+ - シングルトン
X - ユニット
1
X²そして、の略記X•Xとなど2Xの略記を使ってX+X、例えば連結リストの代数式を定義することができる。
data List a = Nil | Cons a (List a)↔L = 1 + X • L
バイナリツリー:
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 つの要素を持つバイナリ ツリーが 1 つだけ存在し、2 つの要素を持つバイナリ ツリーが 2 つ存在し (2 番目の要素は左のブランチまたは右のブランチに存在する可能性があります)、3 つの要素を持つバイナリ ツリーが 5 つ存在するなど、(私にとっては) 自明ではない事実を表しています。
そこで私の質問は、ここで何をしているのでしょうか? これらの操作は不当に思えますが (そもそも代数データ型の平方根とは正確には何でしょうか?)、理にかなった結果につながります。2 つの代数データ型の商はコンピューター サイエンスにおいて意味があるのでしょうか、それとも単なる表記上のトリックなのでしょうか?
そして、おそらくもっと興味深いのは、これらのアイデアを拡張できるかどうかです。たとえば、型上の任意の関数を許可する型の代数の理論はありますか、それとも型にはべき級数表現が必要ですか? 関数のクラスを定義できる場合、関数の合成には意味がありますか?
ベストアンサー1
免責事項: ⊥ を考慮すると、この多くは実際には正しく機能しないため、簡単にするためにこれをあからさまに無視します。
最初のポイントをいくつか挙げます。
ここで「結合」はおそらくA+Bを表す最適な用語ではないことに注意してください。これは具体的には分離した連合2 つのタイプは同じであっても両側が区別されるため、2 つのタイプは区別されます。参考までに、より一般的な用語は単に「合計タイプ」です。
シングルトン型は、実質的にはすべてユニット型です。代数操作では同じように動作し、さらに重要なことは、存在する情報量が保持されることです。
おそらくゼロ型も必要でしょう。Haskell はそれを として提供します
Void。型が 1 の値が 1 つあるのと同じように、型が 0 の値は存在しません。
ここではまだ 1 つの主要な操作が欠落していますが、これについては後ほど説明します。
おそらくお気づきかと思いますが、Haskell はカテゴリー理論から概念を借用する傾向があり、上記のすべては次のように非常に簡単に解釈できます。
Hask内のオブジェクト A と B が与えられた場合、それらの積 A×B は、2 つの射影fst : A×B → A とsnd : A×B → B を可能にする唯一の型です (同型性を除いて)。ここで、任意の型 C と関数f : C → A, g : C → B が与えられた場合、 fst ∘ (f &&& g) = fとなるようなペアリングf &&& g : C → A×B を定義できます。 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。
積型と和型の多くの特性は、上記から導き出すことができます。任意のシングルトン型はHaskの終端オブジェクトであり、任意の空型は初期オブジェクトであることに注意してください。
前述の行方不明の手術に戻ると、デカルト閉カテゴリあなたが持っている指数オブジェクトこれらはカテゴリの矢印に対応します。矢印は関数で、オブジェクトは種類 を持つ型であり*、型 は型の代数的操作のコンテキストではA -> B実際に B ABool -> Aとして動作します。なぜこれが成り立つのか明らかでない場合は、型 について考えてみましょう。可能な入力が 2 つしかない場合、その型の関数は型 の 2 つの値A、つまりと同型です(A, A)。 については、可能な入力が 3 つあるなどです。また、上記の共対定義を代数表記法を使用して言い換えると、恒等式 C A × C B = C A+BMaybe Bool -> Aが得られることに注意してください。
これがすべて理にかなっている理由、特に冪級数展開の使用が正当化される理由については、上記の多くは代数的動作を示すために型の「居住者」(つまり、その型を持つ個別の値) を参照していることに注意してください。この観点を明確にするために、次のことを行います。
積型は、とから独立して取られた
(A, B)各値を表します。したがって、任意の固定値 に対して、の各要素に対して型の値が 1 つあります。これはもちろん直積であり、積型の要素の数は要素の要素の数の積です。ABa :: A(A, B)B和型は、左のブランチと右のブランチが区別された、またはの
Either A Bいずれかの値を表します。前述のように、これは互いに素な和集合であり、和型の居住者数は、加数の居住者数の合計です。AB指数型は、型の値から型の値へ
B -> Aのマッピングを表します。任意の固定引数に対して、任意の の値を割り当てることができます。型の値は、各入力に対してそのようなマッピングを 1 つ選択します。これは、の個数と同じ数の のコピーの積に相当し、これが累乗になります。BAb :: BAB -> AAB
最初は型をセットとして扱いたくなりますが、このコンテキストでは実際にはあまりうまく機能しません。セットの標準的な結合ではなく、非結合の結合があり、交差や他の多くのセット演算の明確な解釈がなく、通常はセットのメンバーシップを気にしません (型チェッカーに任せます)。
一方、上記の構造では、居住者の数を数えることに多くの時間を費やしており、型の可能な値を列挙することはここでは便利な概念です。これはすぐに次のことにつながります。列挙的組合せ論リンク先のWikipediaの記事を参照すると、まず「ペア」と「ユニオン」を積和型と全く同じ意味で次のように定義していることがわかります。生成関数次に、Haskell のリストと同一の「シーケンス」に対して、まったく同じ手法を使用して同じことを行います。
編集:ああ、ここでポイントを非常によく示していると思うちょっとしたおまけがあります。コメントで、ツリー型の場合はT = 1 + T^2恒等式 を導出できると述べていましたがT^6 = 1、これは明らかに間違っています。ただし、T^7 = T は成り立ち、ツリーとツリーの 7 組の間の一対一表現を直接構築できます。cf.アンドレアス・ブラスの「Seven Trees in One」。
編集×2:他の回答で言及されている「型の派生」構造については、次の記事もご覧ください。同じ著者によるこの論文これは、分割の概念やその他の興味深いものを含め、アイデアをさらに発展させたものです。