式の集まりとして構成されているプログラム*1を考えよう。 プログラムを実行すると、式が順番に実行されていって、最終的に何らかの結果が得られたり、あるいは行き詰まり状態になって何も得られなかったりする。
いま、「実行すると数値になる式」と「実行すると真偽値になる式」とを区別したいとしよう。 なぜ区別したいかはいったん忘れて、とにかく「両者の区別がきちんとなされているようにプログラムを書きたい」というモチベーションがあるような状況を考えてほしい。
このような区別の価値は、たとえば「実行すると真偽値になる式」にBoolのような名前を付けるだけで満足してしまうと、半減する。
そんなふうに名前を付けるだけでは、「…真偽値になる式」の部分にしか言及できないからだ。
つまり、「実行すると…」の部分によってもたらされるかもしれないありがたみが反故になってしまう。
いま欲しいのは、あくまでも「実行すると何になる式か」を論じられるような区別であって、式を実行した結果の値の性質による分類ではない。
幸い、式に対する規則の集まりを定義することで、この区別が実現できることがわかっている。 そのような規則を「型付け規則」と呼ぶ。 型付け規則によって割り当てられるものが「型」である。
型付け規則の集まりをうまく用意すると、式を実行したときに行き詰まり状態にならないことが実行しなくてもわかる、という素晴らしい結果が手に入ることが数学的に証明できる。 これが一般に「型安全性」と呼ばれる性質である。
ここまでの話で読み取ってほしいことが2つある。
- 型付けは、プログラムの式を素朴に分類するだけの話ではない
- 値の種類による分類は、プログラムの型安全性とはけっこう違う
言い換えると、型を「取りうる値の集合」として説明してしまうと、プログラムの型安全性について説明したことにならない*2。
もちろんこれは、「型を集合としては説明できない」という意味ではない。 「取りうる値の集合」としての型、「その集合の要素」としての式を実行して得られる値、「集合間の写像」としての関数、「部分集合」としての部分型といったきれいな対応はあるし、バリアント型やレコード型を集合の和や積に対応させることもできる。 実際、そのような対応は単なる比喩ではなく、型安全性の証明は歴史的には集合としての解釈で示されていたらしいし、特にTypeScriptでは、和や積や部分型といった型の構造を説明するのに集合が使われている。
しかし一般には、型の構造が説明できることと、型安全性が説明できることは、別の話である。 後者については、型を「値の集合」とみなすと情報が足りなくて、たとえば再帰的なプログラムの振る舞いを説明できない。 型が違うけど同じ仕方で振る舞う関数みたいなやつ（いわゆるジェネリクス）についても、型変数を集合に対応させること自体はできるだろうけど、その性質はやはり型を「値の集合」として説明するだけでは説明できない。
そもそも「集合」という概念自体がふんわり使われすぎているのも気になる*3。
「Javaとかのtypeとは違うよ、むしろsetだと思うとよいよ」みたいな説明ならともかく、「型は（取り得る値の）集合です」というだけでは、説明をしたことにならない気がする。
というわけで、「型は（取りうる値の）集合」といった一般向けの説明は、型安全性の話をしたいときには、あまり好ましくないのではないかと考えている。 いろいろわかったうえで「集合という直観」を説明に使いたいという気持ちはわかるものの、そこはこらえて、せめて型安全性について話をするときには上記のような世界観のほうをなんとか（この記事よりうまくかつ正確に）伝えてほしいなと思う。
「そうはいっても、型とは何かの説明、めんどくさいんだよな」という場合には、『型システムのしくみ』という本がありますので、「プログラミングにおける型が何かについては、ひとまずこの本を読んでください」の一言で済みます。 便利です。
型システムのしくみ ― TypeScriptで実装しながら学ぶ型とプログラミング言語www.lambdanote.com
なお、小難しいことを言うと、むしろ「集合は型の一種」というべきです。 具体的には、ホモトピー型理論に「同一視型」というのがあり、この「同一視型が命題である型」が「集合」と定義されます。 ホモトピー型理論と同一視型については、『n月刊ラムダノート「特集：計算とは何か」Vol.6, No.1(2026)』をご覧ください。
