[paper][林晋][type_theory][computer_science][software_science][IPSJ][programming_language][programming][logic][functional_programming][applied_mathematics] >ほとんどの高級プログラミング言語は，型の概念をもっている． たとえば，Pascal，Cらでは変数を宣言するときには，その型を指定しなければならない． これらの言語では変数は，概念的にはメモリの一部分の指定された場所を表す名前であり，コンパイルを行う際，それぞれの変数に，どれだけも広さの場所を割りふるべきかを知らねばならないので変数の型により，必要な広さを計算しなければならないからである． これに反して，LISPや関数型言語では，変数はデータ(値)を表す名前であり，データは，S式や関数のようにサイズに制限がないのでヒープ上におかれ，変数には，そのデータへのポインタのみがおかれる． このため上記のような変数の型宣言を行う必要はない． このため，関数型言語での型の使われ型は，CやPascalでの型の使われ方とは，かなり異なっている． …

関数型言語における型理論 http://ci.nii.ac.jp/naid/110002718057/