TypeScript 1.4について、 TypeScript 1.4.1 変更点 – Qiita という記事が目に留まった。で、その中の
直和型(Union Types)
という項目に引っかかりを感じた。

なぜ引っかかりを感じたかというと、TypeScriptに今回導入されたUnion Typesと、巷に言う直和型というのは、異なる概念であるからだ。

注意：以下の話は型理論の専門家でもないフツーの学生が適当に書いた程度の信憑性しかありません。

余積としての直和型

まず「直和型」(sum type)の定義だが、ここではTypeScriptの型と（一変数）関数のなす圏における余積(coproduct)とする。といっても、あまり細かいことは気にしない。

圏の余積はどういうものだったか思い出してみよう。対象 \(A\) と \(B\) に対する \(A\) と \(B\) の余積(coproduct) \(A\sqcup B\) とは、射 \(\mathrm{inl}\colon A\to A\sqcup B\) (left injection)と射 \(\mathrm{inr}\colon B\to A\sqcup B\) (right injection)があって、任意の対象 \(C\) と 射の組 \(f\colon A\to C, g\colon B\to C\) に対して次の図式を可換にする射 \(A\sqcup B\to C\) が一意的に存在するもののことであった。

数学における例を出すと、集合の非交和は集合の圏における余積となっている。

具体的なプログラミング言語における直和型の例としては、Haskellだと Either a b が a と bの直和型となっている。\(\mathrm{inl}\) は型構築子 Left :: a → Either a b、\(\mathrm{inr}\) は型構築子 Right :: b → Either a b である。

C言語のいわゆる「タグ付きunion」も直和型と言える。

注意してほしいのは、直和型は、一般には「左右どちらの値を持っているか知っている」という点である。たとえ \(A=B\) であっても、\(A\) と \(A\sqcup B(=A\sqcup A)\) は一般には別の型である。（注：ただし、\(A\) が始対象であれば \(A\) と \(A\sqcup A\) は同型になる）

部分型とunion type

型 B が型 A の部分型(subtype)であるとは、型 B の値が型 A の値としてもみなせるということである。

例えば、（適切な例と言えるかは自信がないが）C言語では int 型の値は double 型の値としてもみなせる（double 型の値を必要とする文脈で使える）。すなわち、int 型は double 型の部分型である。

あるいは、典型的なオブジェクト指向言語で class Derived : public Base という感じでクラスの継承関係があれば、Derived 型の値は Base 型の値としてもみなせる。すなわち、Derived 型は Base 型の部分型である。

部分型(subtype)の逆の関係をsupertype（しっくりくる訳語が浮かばなかった）という。例えば、TypeScriptでは、any はあらゆる型のsupertypeである。

このように、型システムに部分型(subtyping)が定まっていることを前提とすれば、TypeScriptに導入された union type というのは、以下の3条件を満たす型であると言える。（一方で、直和型は部分型に関係なく定義できる）

• A|B は A のsupertypeである。つまり、型 A をもつ値は型 A|B の値としてもみなせる。
• A|B は B のsupertypeである。つまり、型 B をもつ値は型 A|B の値としてもみなせる。
• C が A のsupertypeであると同時に B のsupertypeであるならば、C は A|B のsupertypeである。

特に、A と A 自身のunion type A|A はもとの A と全く同じ型になる。（直和型について、\(A\) と \(A\sqcup A\) が一般には別の型になることとは対照的だ）

数学で言う集合の和集合(union)と同じような感じだ。

順序集合になじみのある人向けの言葉で言えば、TypeScriptの型を、部分型関係(subtyping relation)を射として圏（前順序の圏）とみなしたときの余積である。

まとめ

直和型とunion typeというのは、どちらも、型を対象とする圏の余積にはなっているが、考えている圏が違う。なのでこれらは違う概念である。

↓読み手を混乱させる駄文

ただし、集合 \(A\) と \(B\) の共通部分が空の時に和集合 \(A\cup B\) は集合の直和（非交和）にもなっていた。同様に、型 A と型 B の「共通の値」が存在しないのであれば、union type A|B は直和型とみなすこともできるだろう。

が、TypeScriptには null や undefined という、「任意の型に当てはまる値」があるので、A|B は直和型にはならない。

逆に言えば、 null や undefined の存在を無視すれば、例えば number|string は number と string の直和型だとみなせる。

しかし、個々の場合に直和型になる場合があったとしても、一般にはunion typeは直和型ではないという結論に変わりはない。

↑読み手を混乱させる駄文

おまけ

じゃあTypeScriptでの直和型って何なのよ？っていうと、例えば次のような感じで実装できる。（深く考えていないのでマズい点があるかもしれない）