「型は集合」って言いきらないほうがいいと思う - golden-luckyの日記

式の集まりとして構成されているプログラム*1を考えよう。 プログラムを実行すると、式が順番に実行されていって、最終的に何らかの結果が得られたり、あるいは行き詰まり状態になって何も得られなかったりする。 いま、「実行すると数値になる式」と「実行すると真偽値になる式」とを区別したいとしよう。 なぜ区別したいかはいったん忘れて、とにかく「両者の区別がきちんとなされているようにプログラムを書きたい」というモチベーションがあるような状況を考えてほしい。 このような区別の価値は、たとえば「実行すると真偽値になる式」にBoolのような名前を付けるだけで満足してしまうと、半減する。 そんなふうに名前を付けるだけでは、「…真偽値になる式」の部分にしか言及できないからだ。 つまり、「実行すると…」の部分によってもたらされるかもしれないありがたみが反故になってしまう。 いま欲しいのは、あくまでも「実行すると何に