プログラマのための簡単な型理論入門 - Qiita

はじめに 昨今のプログラミング言語では型が重要だってことは間違いない。 そして、型理論がその一翼を担っている。 しかし、型理論ってのはそれ専用の記法で書かれている。 焦るとまったく分けの分からない物と目に映るだろう。 例えば以下の式を見よう。 Γ |- t1 : T1 -> T2 Γ |- t2 : T1 -------------------------------------- Γ |- t1 t2 : T2 この式の意味は、t1の型がT1->T1でt2の型がT1の時、関数t1にt2を適用した値の型はT2になるという意味である。 と、書かれても訳の分からない事が書かれていると思うはずだ。 分かっている人からすると正しくない文章だとなるだろう。 なぜ、正しくないのか？ なぜ、難しいのか？ 難しいと感じるという事 実のところは難しいというのは、実は必要なら覚えるが必要でなさそうだから覚える