0と1は違う -- 型システムの集合的意味論とか - 檜山正幸のキマイラ飼育記 (はてなBlog)

0と1は違う -- って、そんなこと当たり前だと思うでしょう。でも、意外に誤解していることがあるようなので、ここで注意しておきます。

内容：

もし 0 = 1 だったら
null問題
集合による意味論
配列の意味論
neverの意味論
undefinedの意味論
void, unit, emptyなどはどうなのか
もっと精密化するには

もし 0 = 1 だったら

0と1はだいぶ性質が違います。

a×0 = 0 （aがなんでも)
a + 0 = a （aがなんでも)

以上の等式は成立しますが、次は（普通は）成立しません。

a×1 = 1 （aがなんでも)
a + 1 = a （aがなんでも)

数のなかでも一番基本的なものは自然数 {0, 1, 2, ...} ですが、自然数を順番に作っていくには次のようにします。

0は自然数である。（まず零ありき！）
nが自然数なら、nの次の数 suc(n) も自然数である。
こうしてできた“数”だけが自然数である。

suc(0) が1なのですが、もし 0 = 1 ならば、suc(0) = 1 = 0 となり、自然数の全体は {0} となってしまいます。0 = 1 が支配する世界では自然数さえ作れません。

論理で、0 = 1 に対応する等式は false = true でしょう。真偽の区別がなくなると、論理システムは矛盾することになります。どんな命題も偽であると同時に真になります。つまり、そういう論理システムは崩壊・破綻しています。

このように、0と1を区別しないことは実に恐ろしいことなのです。にもかかわらず、プログラミングやデータ処理では、0と1がしばしば混同されています。

null問題

あるはずがないと思われる「0と1の混同」が起きる主な原因は、null（あるいはそれに類似の）概念の存在です。

nullは、「値がない」ことを意味する値としてしばしば使われます。しかし、nullという値はあるので、null型のデータ領域（データインスタンスの集合）は単元集合であり空集合ではありません。「値があるのに値がない」、あるいは「値がないのに値がある」という状況を作り出しています。

このことが、「0に相当する空集合」と「1に相当する単元集合」を区別しなかったり、曖昧にしておく習慣につながったのでしょう。しかし、空集合と単元集合の同一視や混同は、データ体系の整合性をメチャクチャにしてしまいます。例えば、型システムは（非形式的、暗黙であれ）推論機構を備えているので一種の論理システムとみなせます。そこで 0 = 1 が証明されると矛盾することになるので、その型システムは論理的に崩壊・破綻します。

集合による意味論

話を簡単にするために、nullと整数と配列だけの型システムを考えます。「null」はインスタンスと型の名前の両方に使うので注意してください。整数型はintegerと書きます。配列型は [integer, integer] とか [integer, [null, integer]] のような形で表すことにします。

型の表現（type expression, type term）と型のデータ領域を区別することにして、型表現Tのデータ領域を【T】と書くことにします。【-】は意味写像です、太い括弧記号はスコット・ブラケットと呼ばれるようです。

まず基本的な意味の定義は次のようになります。

【null】 = {null}
【integer】 = {..., -2, -1, 0, 1, 2, ...}

集合としての {null} をNull、集合としての {..., -2, -1, 0, 1, 2, ...} をIntegerと書けば：

【null】 = Null = {null}
【integer】 = Integer = {..., -2, -1, 0, 1, 2, ...}

なんだかバカみたいな等式ですが、ときに記号と意味を区別する必要があるので、こんな書き方をしているのです。

配列の意味論

配列型、例えば [integer, integer] の意味論はどうなるでしょう。配列項目の型たちから配列型を作る操作は型構成子なので、配列型構成子の意味論を次のように定めます。

【[T₁, ..., T_n]】 = 【T₁】× ... ×【 T_n】

ここで、記号×は集合の直積です。

例えば、次のようになります。

【[integer, integer]】 = 【integer】×【integer】 = Integer×Integer
【[integer, [null, integer]]】 = 【integer】×【[null, integer]】 = 【integer】×(【null】×【integer】) = Integer×(Null×Integer)

右辺は集合とその演算なので、お好みに応じていくらで厳密に定義できます。

f, g, hが次のようなプロファイルの関数だとしましょう。

f : integer→null
g : null→integer
h : integer→[integer, integer]

[f(1), g(null), h(10)] という配列式を考えると、この式の値の型は [nul, integer, [integer, integer]] となります。集合としての意味を計算すると次のようになります。



   【[null, integer, [integer, integer]]】

 = 【null】×【integer】×【[integer, integer]】

 = 【null】×【integer】×(【integer】×【integer】)

 = Null×Integer×(Integer×Integer)

neverの意味論

関数の「引数がない」、「戻り値がない」ということは通常次のように解釈できます。

fの引数のデータ領域がなんらかの単元集合のとき、その関数の引数はない（0引数）とみなす。
fの戻り値のデータ領域がなんらかの単元集合のとき、その関数の戻り値はないとみなす。

今のところ、我々の型システムにある単元集合はNullだけなので、次のように約束できます。

fの引数のデータ領域がNullのとき、その関数の引数はない（0引数）とみなす。f(null) を f() と書いてよい。
fの戻り値のデータ領域がNullのとき、その関数の戻り値はないとみなす。fの戻り値であるnullは無視してよい。

以上は約束により「ないとみなす」のですが、関数の戻り値がほんとにないことがあります。常に例外を発生させる関数とoneway呼び出しの関数です。詳しくは次を参照してください。

void型とunit型とoneway呼び出し

「戻り値がほんとにない」ことを表すためにnever型を導入します。

【never】 = {} = Never

neverがnullとはまったく違った型であることを見るために、関数kが常に例外を引き起こすとします。つまり、k : integer→never とします。

このとき、[f(1), k(3), h(10)] という式を考えます（fとhは前の例と同じとする）。この配列式の型は、[null, never, [integer, integer]] です。その意味を計算すると：



   【[null, never, [integer, integer]]】

 = 【null】×【never】×【[integer, integer]】

 = 【null】×【never】×(【integer】×【integer】)

 = Null×Never×(Integer×Integer)

と、こうなります。

ここで、Neverは空集合であったことを思い出してください。空集合の記号は、ギリシャ文字ファイφに似た記号や太い0とか、零に似た形が採用されます。それは、0×a = 0×a = 0 を想起しやすくするためです。



   Null×Never×(Integer×Integer)

 = Null×0×(Integer×Integer)

 = 0

配列のどこであれ、neverが出現すると全体の型もneverとなり、データ領域は空集合となります。これは、常に例外を発生させる関数を含んだ式は、ほんとに戻り値を持てないことに対応します。

undefinedの意味論

JavaScritでは、null型とは別にundefined型があります。Firebugで実験してみます。



>>> a = [3,,10]

[3, undefined, 10]

>>> a[0]

3

>>> a[1]

undefined

>>> a[2]

10

>>> a[3]

undefined



>>> b = {x:5, y:-1}

Object { x=5, y=-1}

>>> b.x

5

>>> b.y

-1

>>> b.a

undefined

>>> b.foo

undefined

undefined型のデータ領域も単元集合です。null型と用途が少し違うのですが、undefined型もシングルトン型であり、null型と似ています。しかし、never型とはまったく違います。never型とundefine型の混同は、0と1の混同そのものです。

undefinedの主な用途は、配列の範囲外インデックスや穴あきインデックス（上の例では a[1]）に対する値、あるいは、オブジェクトデータの定義されてないプロパティの値として使うことです。「そこに値がない」ことを意味しますが、「値がないことを表す値がある」わけで、「ほんとに値がないこと」とは違います。

配列項目やオブジェクプロパティに「値がない」ことを示すために、例外を発生させることもできます。その場合は、never型が登場しますが、部分関数を使った意味論が必要になり、事情が複雑になります。配列インデックスとオブジェクトプロパティ名によるアクセスを単純な意味論で済ませるためには、undefinedの導入は良い方法です。

undefinedを新たに導入せずにnullで済ませることもできたと思います。配列項目の非存在とオブジェクトプロパティの非存在に別な未定義値を使うこともできたでしょう。そこらへんの選択に、絶対的な基準はないと思われます。

void, unit, emptyなどはどうなのか

空集合はこの世に1個しかありませんが、単元集合はいくらでもあります。集合的な0は絶対的・一意的に決まりますが、集合的な1は無数にあり、なにを選んでもいい、という状況です。

JavaScriptには、null型とundefined型がありますが、その他のプログラミング言語ではvoid型、unit型など（と呼ばれる型）があります。これらはシングルトン型で、なにか特殊な1個の要素を持ちます。unit型（と呼ばれる型）は、多くの場合 () と書かれる要素を持ちます。これは、形の上からは長さ0のタプルやリストです。Lispのnilは、長さ0のリスト()も兼ねていましたし、falseも兼ねていました -- unit型値の表記はnilが起源でしょうか。

emptyが、empty listやempty objectの単元集合を表すならシングルトン型でしょうし、ほんとのempty setならnever型と同じくデータインスタンスを1つも持たない型となるでしょう。emptyという言葉の曖昧性からわかるように、「空なモノが1個」と「なにもない」の区別はけっこう難しいのです。「空なモノが1個」は、例えば {0} のようなもので、「なにもない」は、{} のようなものです。{0} と {} は等しくありません、どうやっても同型にさえなりません。まったくの別物なのです。

もっと精密化するには

配列型（タプル型、リスト型）とオブジェクト型（入れ子を許すレコード型）に関する議論を簡単にしたいなら、undefined型を導入して、未定義な場所でも特殊な値を持つと考えるのが良いと思います。しかし、未定義をundefined値に還元しないとなると、話はややこしくなります。

「未定義な遷移の解釈 -- 3つの立場」において、未定義の解釈がいくつもあることを述べました。3つ以上の立場があるかもしれません。未定義値（undefined値）を返せる未定義と未定義値も返せない未定義（例外や無限走行）に分けると精密になりますが、型システムやプログラムの意味論は複雑になります。

未定義の定式化にはいろいろな方法がありますが、配列インデックスやプロパティ名の集合上のバンドルとセクションを考えることになるでしょう。部分的にしか定義されないセクションと、特殊な値を使って全域に延長したセクションを区別する必要があります。部分的なセクションを全域に延長できるかどうかは自明ではありません。結局は、計算可能性から導かれるある種の位相を使った層（sheaf）の話になってしまいますね。あー、0 ≠ 1 は難しい。