7 に答える
免責事項：⊥を説明するとき、これの多くは実際には正しく機能しないので、簡単にするためにそれを露骨に無視します。
いくつかの最初のポイント：
ここでは、「和集合」はおそらくA + Bの最良の用語ではないことに注意してください。これは、タイプが同じであっても2つの辺が区別されるため、具体的には2つのタイプの非交和です。価値のあるものとして、より一般的な用語は単に「合計タイプ」です。
シングルトンタイプは、事実上、すべてのユニットタイプです。それらは代数的操作の下で同じように動作し、さらに重要なことに、存在する情報の量は依然として保持されます。
おそらくゼロタイプも必要です。Haskellはそれをとして提供してい
Voidます。タイプが1の値が1つあるのと同じように、タイプがゼロの値はありません。
ここにはまだ1つの主要な操作がありませんが、すぐに戻ります。
おそらくお気づきかもしれませんが、Haskellは圏論から概念を借りる傾向があり、上記のすべてはそのように非常に単純な解釈を持っています：
HaskのオブジェクトAとBが与えられると、それらの積A×Bは2つの射影を可能にする一意の（同型までの）タイプです。fst：A×B→Aとsnd：A×B→B、任意のタイプCと関数f：C→A、g：C→Bペアリングf &&& g：C→A×Bをfst∘（f &&& g） = fと定義でき、 gについても同様です。パラメトリシティは普遍的な特性を自動的に保証し、私の微妙ではない名前の選択があなたにアイデアを与えるはずです。ちなみに、
(&&&)演算子はで定義さControl.Arrowれています。上記の二重は、注入がinl：A→A + Bおよびinr：B→A+Bの余積A+Bです。ここで、任意のタイプCおよび関数f：A→C、g：B→Cが与えられると、次のことができます。コペアリングfを定義する||| g：明らかな同等性が成り立つようにA+B→C。繰り返しますが、パラメトリシティはトリッキーな部分のほとんどを自動的に保証します。この場合、標準の注入は単純
LeftでRightあり、コペアリングは関数eitherです。
productおよびsumタイプのプロパティの多くは、上記から導き出すことができます。シングルトンタイプはHaskのターミナルオブジェクトであり、空のタイプは初期オブジェクトであることに注意してください。
前述の欠落している操作に戻ると、デカルト閉圏には、カテゴリの矢印に対応する指数オブジェクトがあります。私たちの矢印は関数であり、私たちのオブジェクトは種類のある型であり、型の代数的操作のコンテキストでは、*型A -> Bは実際にBAとして動作します。これが当てはまる理由が明らかでない場合は、タイプを検討してください。可能な入力が2つしかない場合、そのタイプの関数は、タイプの2つの値と同型です。3つの可能な入力があります。また、代数表記を使用するために上記のコペアリング定義を言い換えると、アイデンティティCA×CB = Cが得られることに注意してください。Bool -> AA(A, A)Maybe Bool -> AA+B。
これがすべて理にかなっている理由、特にべき級数展開の使用が正当化される理由については、上記の多くがタイプの「住民」（つまり、そのタイプを持つ個別の値）を順番に参照していることに注意してください代数的振る舞いを示すため。その視点を明確にするには：
製品タイプは、と
(A, B)からそれぞれの値を表し、独立して取得されます。したがって、任意の固定値に対して、の住民ごとにタイプの値が1つあります。これはもちろんデカルト積であり、製品タイプの住民の数は、因子の住民の数の積です。ABa :: A(A, B)B合計タイプは、またはのいずれか
Either A Bからの値を表し、左右の分岐が区別されます。前述のように、これは非交和であり、合計タイプの住民の数は、被加数の住民の数の合計です。AB指数型は、型の値
B -> Aから型の値へのマッピングを表します。任意の固定引数に対して、任意の値を割り当てることができます。タイプの値は、入力ごとにそのようなマッピングを1つ選択します。これは、住民と同じ数のコピーの積に相当するため、べき乗になります。BAb :: BAB -> AAB
最初は型を集合として扱いたくなりますが、このコンテキストでは実際にはうまく機能しません。標準の集合の和集合ではなく非交和があり、共通部分や他の多くの集合演算の明確な解釈はありません。通常、メンバーシップの設定については気にしません（タイプチェッカーに任せます）。
一方、上記の構造は、住民のカウントについて多くの時間を費やしており、タイプの可能な値を列挙することは、ここでは有用な概念です。それはすぐに数え上げの組み合わせ論につながります。リンクされたウィキペディアの記事を参照すると、最初に行うことの1つは、製品や合計のタイプとまったく同じ意味で「ペア」と「ユニオン」を定義することです。次に、関数を生成し、Haskellのリストとまったく同じ手法を使用して、「シーケンス」に対して同じことを行います。
編集：ああ、そしてこれが私がポイントを印象的に示していると思う簡単なボーナスです。コメントで、ツリータイプのT = 1 + T^2場合、IDを導出できると述べましたT^6 = 1が、これは明らかに間違っています。ただし、それT^7 = T は成り立ち、木と7タプルの木の間の全単射を直接構築することができます。アンドレアスブラスの「1本の7本の木」。
編集×2：他の回答で言及されている「タイプの導関数」構造の主題については、分割の概念やその他の興味深いものを含め、アイデアをさらに発展させた同じ著者からのこの論文を楽しむこともできます。
二分木は、型の半環の方程式によって定義されT=1+XT^2ます。構成により、T=(1-sqrt(1-4X))/(2X)は複素数の半環で同じ方程式によって定義されます。したがって、代数構造の同じクラスで同じ方程式を解いていることを考えると、いくつかの類似点が見られても実際には驚くべきことではありません。
問題は、複素数の半環の多項式について推論するとき、通常、複素数が環または体を形成するという事実を使用するため、半環には適用されない減算などの演算を使用していることに気付くことです。しかし、方程式の両辺をキャンセルできるルールがあれば、多くの場合、引数から減算を削除できます。これは、フィオーレとレンスターが環に関する多くの議論を半環に転用できることを証明したようなものです。
これは、環に関する多くの数学的知識を確実に型に移すことができることを意味します。その結果、複素数またはベキ級数 (正式なベキ級数のリング内) を含むいくつかの引数は、完全に厳密な方法で型に引き継がれる可能性があります。
しかし、これ以上の話があります。2 つの累乗級数が等しいことを示すことによって、2 つの型が等しい (たとえば) ことを証明することは 1 つのことです。ただし、ベキ級数の項を調べて、型に関する情報を推測することもできます。ここでの正式な声明がどうあるべきかわかりません。(密接に関連しているが、種は型と同じではないいくつかの研究については、組み合わせ種に関するBrent Yorgey の論文をお勧めします。)
私がまったく驚くべきことは、あなたが発見したことが微積分に拡張できるということです. 微積分に関する定理は、型の半環に移すことができます。実際、有限差分に関する議論でさえも転用することができ、数値解析からの古典的な定理が型理論で解釈されていることがわかります。
楽しむ！
繰り返し関係を拡大しているだけのようです。
L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
= 1 + X + X^2 + X^3 + X^4 ...
T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
= 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...
また、型に対する演算の規則は算術演算の規則と同じように機能するため、再帰関係を展開する方法を理解するのに代数的手段を使用できます (明らかではないため)。
Algebra of Communicating Processes (ACP) は、同様の種類のプロセスの式を扱います。選択とシーケンスの演算子として加算と乗算を提供し、関連するニュートラル要素を備えています。これらに基づいて、並列処理や中断など、他の構造の演算子があります。http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processesを参照してください。「A Brief History of Process Algebra」という名前の論文もオンラインにあります。
ACP を使用してプログラミング言語を拡張する作業を行っています。昨年 4 月、Scala Days 2012 で研究論文を発表しました。http://code.google.com/p/subscript/で入手できます。
カンファレンスで、バッグの並列再帰仕様を実行するデバッガーのデモを行いました。
バッグ = A; (バガ&ア)
ここで、A と は入出力アクションを表します。セミコロンとアンパサンドは、シーケンスと並列処理を表します。前のリンクからアクセスできる SkillsMatter のビデオを参照してください。
より匹敵するバッグ仕様
L = 1 + X•L
だろう
B = 1 + X&B
ACP は、公理を使用して、選択と順序の観点から並列処理を定義します。ウィキペディアの記事を参照してください。バッグのアナロジーは何に使うのだろう
L = 1 / (1-X)
ACP スタイルのプログラミングは、テキスト パーサーと GUI コントローラーに便利です。などの仕様
searchCommand = クリック (検索ボタン) + キー (Enter)
cancelCommand = クリック (キャンセル ボタン) + キー (エスケープ)
「クリック」と「キー」という 2 つの絞り込みを暗黙的にすることで、より簡潔に書き留めることができます (Scala が関数で許可しているように)。したがって、次のように書くことができます。
searchCommand = 検索ボタン + Enter
cancelCommand = cancelButton + エスケープ
右側には、プロセスではなくデータであるオペランドが含まれるようになりました。このレベルでは、どのような暗黙の洗練がこれらのオペランドをプロセスに変えるかを知る必要はありません。それらは必ずしも入力アクションに絞り込まれるとは限りません。出力アクションは、テスト ロボットの仕様などにも適用されます。
プロセスは、この方法でデータをコンパニオンとして取得します。したがって、私は「項目代数」という用語を作りました。