はじめに
昨今のプログラミング言語では型が重要だってことは間違いない。
そして、型理論がその一翼を担っている。
しかし、型理論ってのはそれ専用の記法で書かれている。
焦るとまったく分けの分からない物と目に映るだろう。
例えば以下の式を見よう。
Γ |- t1 : T1 -> T2 Γ |- t2 : T1
--------------------------------------
Γ |- t1 t2 : T2
この式の意味は、t1の型がT1->T1でt2の型がT1の時、関数t1にt2を適用した値の型はT2になるという意味である。
と、書かれても訳の分からない事が書かれていると思うはずだ。
分かっている人からすると正しくない文章だとなるだろう。
なぜ、正しくないのか？
なぜ、難しいのか？
難しいと感じるという事
実のところは難しいというのは、実は必要なら覚えるが必要でなさそうだから覚える必要がない物だと判断したということなのだ。必要ないから覚えたくないという拒絶をしているのである。
そのような判断をしているときに無理に読もうとすると眠くなる。
この眠りの魔法を解こう。
環境によって状況は変わる
さっきの式から Γ |- を取り除こう。邪魔な存在は消した方が分かりやすい。
t1 : T1 -> T2 t2 : T1
-------------------------
t1 t2 : T2
これでも、t1はT1を受け取ってT2を返し、t2はT1のときにt1にt2を適用した型はT2だと言う事が表せるし、何の問題も無いように思える。
以下の例はt1とt2がTestクラスの中にあって、殆ど同じ環境下にある。
殆どというのは、t2の環境にはargvという変数が追加されているので正しくは違う環境である。
class Test {
static String t1(int a) { return ""+a; }
static int t2 = 1;
static void main(String[] argv) {
String result = t1(t2);
}
}
この場合は、t1にt2を適用した場合の結果の型はStringである。
次の例はどうだろう？
class Test {
static String t1(int a) { return ""+a; }
}
class Test2 {
static int t1(int a) { return a; }
static int t2 = 1;
static void main(String[] argv) {
int result = t1(t2);
}
}
この場合の、Testのt1とTest2のt2を取り出した場合には、t1の型がintを受け取ってStringを返し、t2の型がintのとき、t1にt2を適用した結果の型はintになる。
t1 : T1 -> T2 t2 : T1
-------------------------
t1 t2 : T1
のようになってしまった。
環境が変われば、環境が同じなら正しい事も、環境が変われば正しくなくなるのである。
こういった環境の差からくる問題は良くある。
たとえば宗教や国レベルになると環境が違うので、常識が通じなくなって対立が起きたり争いが起きる。t2からすれば、argvは当たり前にあるかもしれないが、t1にとってargvは触る事が出来ない存在なのである。
環境の違いを意識する
これでは困るので、環境は同じであるという事を示したい。
環境は宗教に例えるなら神に相当する物である。同じ神を崇めるもの同士なら共通の価値観を共有するのでうまくのだ。
その為の記法が必要だ。環境を司る神といえばガイア(Γαῖα)がいる。
大地の神ガイア
ガイアの頭文字Γ(ガンマ)を使って環境を表そう。
最初の例を書くと以下のようになる。
Γ|- t1 : int->String Γ |- t2
----------------------------------
Γ,argv:String[] |- t1 t2 : String
後の例を書くと以下のようになる
Γ|- t1 : int->String Γ,t1:int->String |- t2
------------------------------------------------
Γ,t1:int->String,argv:String[] |- t1 t2 : int
これは型環境とか、文脈とか言う意味である。
神の領域と人間の領域を隔てる記号がTを横に倒したような|-という記号なのである。下を横に倒したと思うと分かりやすいのかもしれない。 環境を司る大地の神ガイアΓαῖαの元に項があるのだ。Γは文脈でもあるからHaskellでいえばモナドである。モナドはガイアに例える事が出来るだろう。
Γを神に例えたが、そんなにΓが凄い訳存在という訳ではない。
変数名から型を表すデータが入っているMapだ。
文字列から型を表すデータへの連想配列にすぎないのだ。Γは言語を作ったわけではなく、ただ環境を提供するだけである。
普通のプログラミング言語では、環境の中身を書く事はないのだけど、プログラミング言語の事を研究するような場合には、環境の中身を意識する必要があるのでこのような記法がある。
神を意識する必要のない人には神は必要ないけど、環境の違いを意識する為には神や国や言葉や法律を意識するのが良い。環境を同じにすれば話はスムーズに進むが、環境を同じにしたグローバル環境だけでは不便だ。複数の環境がある場合は、それは違う環境である事を示せば話はうまく進むのである。
まとめ
Γはガンマと読み、型環境を表す。
|-の左に型環境を書いて、右側に項を書く。
:は型を表す演算子で左側に項を右側に型を書く。
Γ |- t1 : T11 -> T12 Γ |- t2 : T11
--------------------------------------
Γ |- t1 t2 : T12
このような式は、眠りの魔法ではない。
世の中を見る為の素晴らしい式だ。
Γはガイアやモナドに例えられる。|-は下を横に倒した記号だと思えば想像がつきやすい。
只の型環境Γの元にt1という関数とt2という変数と型T11とT12という型があった場合には、t1にt2を適用した式の型はT12だということなのだ。