この記事はTSG Advent Calendar 2020の14日目の記事です。昨日の記事はJP3BGYさんのPXE BootとIntel DCIを用いたLinux Debug環境でした。
カリー＝ハワード同型対応ってかっこいいけど、何のことだかよくわからない。わたくし昆布の現時点での（偏った）理解を、疑似コードを交えて説明していきます。ほぼ備忘録です。
直観主義論理（自然演繹）の命題とTypeScriptの型との間のカリー＝ハワード同型対応を考えます。
Wikipediaでは次のように書いてあります。
カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry-Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。
さらにWikipediaを読み進めていくと、なんでも、プログラムでの型と、論理での命題が対応するらしいことがわかります。その先を読むとどのように対応するのか分かりそうですが、かなり難しいことが書いてあって全然分かりません。
実は厳密な定式化では、カリー＝ハワード同型対応で論理と対応するのは、プログラムというよりはそれを抽象化したものである「型付きλ計算」のようです。残念ながらその話は一切理解しておりません（恥ずかしい……）。
ここでは、論理と具体的なプログラムとの対応を考えることにします。特に、「P₁, P₂,…が仮定されているとき、Qが証明できる」ことと「型P1, P2,…の変数がすでに定義されているとき、型Qの変数が定義できる」ことが等価になるようなPとP, QとQの対応を考えます。
普通は「P₁, P₂,…が仮定されているとき、Qが証明できる」と「型P1, P2,…の値が存在するとき、型Qの値が存在する」との対応を考えるようですが、「値が存在する」では捉えどころがないというか、確かめにくいので、このようにします。
せっかくなのでTSGが誇るAIの意見も聞いてみましょう。
AIの考えることは高度すぎて人間には分かりませんでした。
論理代表として直観主義論理（自然演繹）を、プログラミング言語代表としてTypeScriptを連れてきました。
直観主義論理は、無数の原子命題と、（否定「¬P」は「P→⊥」の略記とみなせるので省略して）3つの結合子「∧」「∨」「→」と、1つの特別な命題「⊥」からなっています。自然演繹という流儀では、これらは推論規則と呼ばれる7つの規則を満たします。
推論規則を「あの型の変数があればこの型の変数が作れる」関係に移すような命題と型の対応は下の表のようになります。
| 直観主義論理 | TypeScript |
|---|---|
| P∧Q | タプル |
| P∨Q | タグ付きunion |
| P→Q | 関数 |
| ⊥ | never |
それでは各推論規則の対応を見ていきます。
「PとQが仮定されているとき、P∧Qが証明できる」
これを「型Pと型Qの変数がすでに定義されているとき、型[P, Q]の変数が定義できる」と読み替えると、それが正しいことは下のように示せます。
const p: P = /* given */;
const q: Q = /* given */;
const conj: [P, Q] = [p, q];
「P∧Qが仮定されているとき、Pが証明でき、Qも証明できる」
これを「型[P, Q]の変数がすでに定義されているとき、型Pの変数が定義でき、型Qの変数も定義できる」と読み替えると、それが正しいことは下のように示せます。
const conj: [P, Q] = /* given */;
const p: P = conj[0];
const q: Q = conj[1];
「Pが仮定されているとき、P∨Qが証明でき、Q∨Pも証明できる」
これを「型Pの変数がすでに定義されているとき、型{type: 'P', content: P} | {type: 'Q', content: Q}の変数が定義でき、{type: 'Q', content: Q} | {type: 'P', content: P}の変数も定義できる」と読み替えると、それが正しいことは下のように示せます。
const p: P = /* given */;
const disj0: {type: 'P', content: P} | {type: 'Q', content: Q} = p;
const disj1: {type: 'Q', content: Q} | {type: 'P', content: P} = p;
「PからRを証明する方法があり、QからRを証明する方法があり、P∨Qが仮定されているとき、Rが証明できる」
これを「型Pの変数を使って型Rの変数を定義する方法があり、型Qの変数を使って型Rの変数を定義する方法があり、型P{type: 'P', content: P} | {type: 'Q', content: Q}の変数がすでに定義されているとき、型Rの変数が定義できる」と読み替えると、それが正しいことは下のように示せます。
const disj: {type: 'P', content: P} | {type: 'Q', content: Q} = /* given */;
var _r: R;
if (disj.type === 'P') {
/* 型Pの変数disjを使って型Rの変数_rを定義する */
}
else{
/* 型Qの変数disjを使って型Rの変数_rを定義する */
}
const r = _r;
もう少しスマートに書くと次のようになります。
const disj: {type: 'P', content: P} | {type: 'Q', content: Q} = /* given */;
const r: R = disj.type === 'P'
? /* 型Pの変数disjを使って作った型Rの値 */
: /* 型Qの変数disjを使って作った型Rの値 */;
「PからRを証明する方法があるとき、P→Qが証明できる」
これを「型Pの変数を使って型Qの変数を定義する方法があるとき、型(p: P) => Qの変数が定義できる」と読み替えると、それが正しいことは下のように示せます。
const impl: (p: P) => Q = (p: P) => {
/* 型Pの変数pを使って型Qの変数qを定義する */
return q;
};
もう少しスマートに書くと次のようになります。
const impl: (p: P) => Q = (p: P) => /* 型Pの変数pを使って作った型Qの値 */;
「PとP→Qが仮定されているとき、Qが証明できる」
これを「型Pと型(p: P) => Qの変数がすでに定義されているとき、型Qの変数が定義できる」と読み替えると、それが正しいことは下のように示せます。
const p: P = /* given */;
const impl: (p: P) => Q = /* given */;
const q: Q = impl(p);
「⊥が仮定されているとき、任意の命題が証明できる」
これを「型neverの変数がすでに定義されているとき、任意の型の変数が定義できる」と読み替えると、それが正しいことは下のように示せます。
const cont: never = /* given */
/*これより先のコードは、処理が辿り着きえないので、コンパイラが一切構わなくても理論上問題ない！*/
const hoge: hoge = piyopiyopiyo; // 定義できた……？
（実際は処理が辿り着きえない部分のコードも読まれ、そこに静的エラーがあればコンパイルは失敗するけど😭）
never型自体むずかしいですよね……。never型は、「どんな値もnever型ではない」という性質を持つものです。
「そんな型何に使うんだ」と思ってしまいますが、例えば、ある変数に値を代入する処理までプログラムが決して辿り着かないということを表したいとき、その変数をnever型にします。例として、上のコードの/* given */のところには(() => {while(true){}})()などを入れることができます。詳しくはTypeScript Deep Dive の記事を読んでください。
TypeScriptでカリー＝ハワード同型対応を探してみました。爆発律のあたりが消化不良ですよね……。
古典論理とカリー＝ハワード同型対応を見つけられる言語もあるようですが、TypeScriptでもできるのかはよく分かりません（多分できないのかな）。
以上は今後の課題としましょう。読んでくださってありがとうございました。
明日の記事はdomperorさんのネタがなかったらTeX/LaTeXアドベントカレンダーの記事をこっちと兼ねる。ネタがあったらもう一記事書くです。ぜひ読んでくださいね！
