TypeScript 4.9.5 での話です。例えば次のようなコードを試してみます。
type Foo<X> = X extends (0 | 1) ? number : string; var x: Foo<null> = 1; // NG var y: Foo<null> = ""; // OK
これは、null extends (0 |1)ではないことを意味します。型を集合と解釈して*1 $`\{\mathrm{null}\} \subseteq \{0, 1\}`$ ではない、と。なるほど。
type Foo<X> = X extends (0 | 1) ? number : string; var x: Foo<0> = 1; // OK var y: Foo<0> = ""; // NG
こっちは、0 extends (0 |1)であることを意味します。$`\{0\} \subseteq \{0, 1\}`$ である、と。そりゃそうですね。
ところが、
type Foo<X> = X extends (0 | 1) ? number : string; var x: Foo<never> = 1; // NG var y: Foo<never> = ""; // NG
えっ、コレどういうこと？ $`\{\} \subseteq \{0, 1\}`$ じゃないの？ さっぱり理解できない。
twitterでつぶやいたら、@qnighy（Masaki Hara）さんに事情を教えていただきました。型の表現をそのまま解釈してはダメで、隠れた独自のルールがあるそうです。その独自のルールを勘案すれば、TypeScriptトランスパイラの挙動は辻褄があってるそうです。
僕の推測による*2、この隠れた独自のルールとメカニズム、それがもたらす効果を、簡素化したモデルで説明します。$`\newcommand{\For}{\text{For } }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\kin}[1]{\mathcal{#1} }
\newcommand{\kinf}[1]{\mathscr{#1} }
`$
内容：
発端と概要
TypeScriptでは与えられた型から別な型を作り出す手順を書けます。例えば：
type Bar<X> = null | X | Array<X> | Array<[X, string?]>;
型変数Xに何か具体的な型を入れれば、例えばBar<number>とすれば、それを具体的な型として使えます。
Foo<X>とかBar<X>は、型を渡されると型を返す関数とみなせます。すべての型からなる型宇宙〈type universe〉を概念的に $`{\bf Type}`$ と表すと、次のようなプロファイル（引数型と戻り型の仕様）を持つ関数〈写像〉を考えることになります。
$`\quad F:{\bf Type} \to {\bf Type}`$
このプロファイルの関数を型構成子とか総称型と呼びますが、ここではより直接的に型関数〈type function〉と呼びましょう。関数を演算子記号で書くときは型演算〈type operation〉とも呼びます
型のあいだに合併演算 $`\cup`$ （TypeScriptでは|）が定義されているとして、型関数 $`F`$ が次の条件を満たすとき、合併分配的〈union distributive〉と呼ぶそうです。
$`\For X, Y\in {\bf Type}\\
\quad F(X \cup Y) = F(X) \cup F(Y)`$
TypeScriptでは、条件付き型〈conditional type〉*3（と呼ばれる型関数）に、合併分配的であることを要求しているのだと、Masaki Haraさんに教わりました。
ちょっと考えただけだと、型のif-then-else構文である条件付き型と合併分配的であることが整合するとは思えません。なんらかのトリックが必要です。そのトリック（だと僕が想定するもの）を述べます。
オモチャの型システム
実際の型システムでは話が複雑になるので、オモチャ模型〈toy model〉で考えます。オモチャの世界では、値は自然数だけを考えます。型は自然数の有限集合とします。関数（普通の関数）は、自然数の有限集合から自然数の有限集合への関数です。
オモチャの世界では、型も関数も具体的に列挙して表示できます。型 $`\{1, 2, 3\}`$ から 型 $`\{11, 100, 123\}`$ への関数 $`f:\{1, 2, 3\} \to \{11, 100, 123\}`$ の列挙表示は、
$`\quad f = \{1 \mapsto 123, 2\mapsto 123, 3\mapsto 11\}`$
とか書けます。
集合 $`U`$ のすべての有限部分集合〈finite subset〉からなるベキ集合〈powerset〉を $`\mrm{FinPow}(U)`$ と書くことにします。すると、オモチャの世界のすべての型の集合は $`\mrm{FinPow}({\bf N})`$ と書けます。$`{\bf N}`$ はすべての自然数（すべての値）からなる集合です。空集合も $`{\bf N}`$ の有限部分集合＝型であることに注意してください。オモチャの世界の型関数は、次の形をしています。
$`\quad F: \mrm{FinPow}({\bf N}) \to \mrm{FinPow}({\bf N})`$
例えば、
$`\For X\in \mrm{FinPow}({\bf N})\\
\quad F(X) := \text{if }0\in X\text{ then } \{\} \text{ else }X`$
これは、ゼロを含む有限部分集合は空集合にしてしまい、そうでないならそのまま元の型を返す関数です。if-then-elseを、疑問符とコロンの三項演算子にして、空集合を $`\text{never}`$ と書くと少しTypeScriptに近い構文になります。
$`\For X\in \mrm{FinPow}({\bf N})\\
\quad F(X) := 0\in X \;?\; \text{never} : X`$
型の型をカインド〈kind〉と呼ぶことにします。オモチャの世界のカインドは、$`\mrm{FinPow}({\bf N})`$ の有限部分集合としましょう。したがって、すべてのカインドからなるカインド宇宙〈kind universe〉は $`\mrm{FinPow}(\mrm{FinPow}({\bf N}) )`$ です。
オモチャの型宇宙とオモチャのカインド宇宙は次のように略記します。
$`\quad {\bf Type} := \mrm{FinPow}({\bf N})\\
\quad {\bf Kind} := \mrm{FinPow}(\mrm{FinPow}({\bf N}))
`$
ここから先、オモチャの世界で考えます。$`{\bf Type}, {\bf Kind}`$ は上記の意味で使います。
文字種の使用法の約束
簡素化したオモチャの世界でも、色々な種類のモノが登場します。ゴッチャになりがちなので、文字種（フォント）を変えて区別しましょう。
- 型はイタリック体大文字の $`A, B`$ などで表す。
- 型を受け取って型を返す型関数はイタリック体大文字の $`F, G`$ などで表す。
- カインド（型の集合）はカリグラフィー体大文字の $`\kin{A}, \kin{B}`$ などで表す。
- カインドを受け取って型を返す関数（後で出てくる）はスクリプト体大文字の $`\kinf{F}, \kinf{G}`$ などで表す。
束縛変数（例えば引数変数〈ラムダ変数〉）はアルファベットの後ろのほう $`X, Y`$ などを使うこともあります（それほど強く意識してないけど）。
型関数は合併分配的とは限らない
型関数 $`F:{\bf Type} \to {\bf Type}`$ があるとき、それが合併分配的だとは限りません。例えば、冒頭の例Fooに類似した次の型関数 $`\mrm{Baz}`$ を考えます。
$`\For X \in {\bf Type} = \mrm{FinPow}({\bf N})\\
\quad \mrm{Baz}(X) := \text{if }X \subseteq \{0, 1\}\text{ then } \{1\} \text{ else }\{2\}
`$
$`X = \{1, 2\}`$ のケースを考えてみると：
$`\quad \mrm{Baz}(\{1, 2\}) = \{2\}\\
\quad \mrm{Baz}(\{1\}) = \{1\}\\
\quad \mrm{Baz}(\{2\}) = \{2\}
`$
です。次が成立しているでしょうか？
$`\quad \mrm{Baz}(\{1\} \cup \{2\}) = \mrm{Baz}(\{1\}) \cup \mrm{Baz}(\{2\})`$
ダメですねー。
もし、「型関数 $`\mrm{Baz}`$ をなんとかして合併分配的にしろ」と言われたらどうでしょう。もともと合併分配的ではないので何か加工変形しないといけません。加工変形したモノを $`\mrm{Baz}'`$ として、それが合併分配的（合併分配性を持つ）ならいいとしましょう（それ以外の対処はない）。
$`\For X, Y \in {\bf Type} = \mrm{FinPow}({\bf N})\\
\quad \mrm{Baz}'(X \cup Y) = \mrm{Baz}'(X) \cup \mrm{Baz}'(Y)
`$
カインド引数の型値関数を使う
型関数 $`F:{\bf Type} \to {\bf Type}`$ は、前節の $`\mrm{Baz}`$ のように、合併分配性を持たない型関数だとします。いったん、カインドを引数とする関数 $`\kinf{F}: {\bf Kind} \to {\bf Type}`$ を作ります。その動機を説明します。
我々が欲しいのは、
$`\quad F(A \cup B) = F(A)\cup F(B)\\
\quad F(A \cup B \cup C) = F(A)\cup F(B) \cup F(C)
`$
のような等式です。しかし、これは成立しない（反例がある）のは分かっている、無理なんです。ならば、合併記号の解釈を変えて次のような等式に目標を切り替えます。
$`\quad F(\{A, B\}) = F(A)\cup F(B)\\
\quad F(\{A, B, C\}) = F(A)\cup F(B) \cup F(C)
`$
引数は型の集合、つまりカインドです。となると、元の $`F`$ とは別物ですから、名前〈記号〉も変えて：
$`\quad \kinf{F}(\{A, B\}) = \kinf{F}(A)\cup \kinf{F}(B)\\
\quad \kinf{F}(\{A, B, C\}) = \kinf{F}(A)\cup \kinf{F}(B) \cup \kinf{F}(C)
`$
$`\kinf{F}`$ のプロファイルは、
$`\quad \kinf{F}: {\bf Kind}\to {\bf Type}`$
です。
与えられた型関数 $`F`$ からカインド宇宙 $`{\bf Kind}`$ 上の関数 $`\kinf{F}`$ を次のように作ります。
$`\For \kin{A} = \{A_1, \cdots, A_n\} \in {\bf Kind}\\
\quad \kinf{F}(\kin{A}) := F(A_1) \cup \cdots \cup F(A_n) \;\in {\bf Type}
`$
特に空カインド $`\emptyset = \{\}`$ に対しては：
$`\quad \kinf{F}( \{\} ) := \{\} \;\in {\bf Type}`$
空集合はこの世にひとつしかないのですが、分かりやすさのために便宜上、
- $`{\bf Type} = \mrm{FinPow}({\bf N})`$ の要素である空集合を $`\mrm{never}`$ とも書く。
- $`{\bf Kind} = \mrm{FinPow}(\mrm{FinPow}({\bf N}) )`$ の要素である空集合を $`\mrm{Never}`$ とも書く。
そうすると：
$`\quad \kinf{F}( \mrm{Never}) := \mrm{never} \;\in {\bf Type}`$
このように定義した $`\kinf{F}`$ では次が成立します。成立するように作っているからです。
$`\For \kin{A}, \kin{B} \in {\bf Kind}\\
\quad \kinf{F}(\kin{A} \cup \kin{B} ) = \kinf{F} (\kin{A}) \cup \kinf{F}(\kin{B} ) \;\in {\bf Type}
`$
$`F`$ から $`\kinf{F}`$ を作る方法は、思いつきとかヒラメキではなくて、$`\mrm{FinPow}`$ が集合圏上のモナドになっていることを利用しています（クライスリ拡張しているだけ）。
型関数に戻す
$`\kinf{F}`$ は望ましい性質を持ちます。が、もはや型関数ではなくて、カインド引数を受け取って型を返す関数です。「別にそれでもいいから、そのまま使おう」というのもひとつの考え方です。
例えば、カインド $`\{A_1, \cdots, A_n\}`$ の構文糖衣として $`A_1 \mid \cdots \mid A_n`$ を使うことにすれば：
$`\quad \kinf{F}( A_1 \mid \cdots \mid A_n ) := F(A_1) \cup \cdots \cup F(A_n) \;\in {\bf Type}\\
\quad \kinf{F}( \mrm{Never}) := \mrm{never} \;\in {\bf Type}`$
プログラミング言語レベルでは、処理系が、ユーザーに気づかれないうちに次の細工をしたらどうでしょう。
- もとの名前 $`F`$ で $`\kinf{F}`$ を参照する。
- $`{\bf Kind}`$ の合併演算と $`{\bf Type}`$ の合併演算に同じ記号をオーバーロードする。
- $`{\bf Kind}`$ の空集合（空カインド）と $`{\bf Type}`$ の空集合（空型＝ネバー型）を同じ記号で表す（もともと同じモノなのでオーバーロードではないです）。
すると、ユーザーには次が成立しているように見えます。
$`\quad F( A_1 \mid \cdots \mid A_n ) = F(A_1) \mid \cdots \mid F(A_n) \;\in {\bf Type} \\
\quad F( \mrm{never}) = \mrm{never} \;\in {\bf Type}`$
一見メデタイようですが、問題があります。$`F`$（ほんとは $`\kinf{F}`$）に渡す引数は、型を `$`\mid`$` で区切って並べた形ですが、次の3つの呼び出しは異なる型を返すかも知れません。
- $`F(\{1, 2, 3\})`$
- $`F(\{1\} \mid \{2, 3\})`$
- $`F(\{1\} \mid \{2\} \mid \{3\})`$
うれしくないなー。
別な方法として、ユーザーが指定した型を処理系が幾つかの型の合併の形に分解します。分解の仕方は前もって一通りに決めておきます。例えば、
$`\quad \{1, 2, 3\} \mapsto \{1\} \mid \{2\} \mid \{3\} \mapsto \{ \{1\} , \{2\} ,\{3\} \}`$
型から作られたカインドに対して $`\kinf{F}`$ を適用します。
つまり、次のような型関数 $`F'`$ を定義するのです。
$`\For A \in {\bf Type}\\
\quad F'(A) := \kinf{F}(\mathsf{D} (A))
`$
ここで $`\mathsf{D}`$ は、渡された型をカインドにする関数です。以下の $`\bigcup`$ はカインド（実体は集合の集合）の要素である集合達の総合併を取る演算です。
$`\quad \mathsf{D} : {\bf Type} \to {\bf Kind}\\
\For A \in {\bf Type}\\
\quad \bigcup( \mathsf{D}(A) ) = A
`$
TypeScriptの場合はおそらく、ユーザーが指定した型を標準的なカインド（幾つかの型の合併の形）に分解して、合併分配性を持つ $`\kinf{F}`$ に渡して結果を得ているのでしょう。これはつまり、ユーザーが書いた $`F`$ を $`F'`$ に加工変形してから使っています。
僕のように「意図してない挙動だぞ」と思うのは、加工変形してから使われることを知らないからでしょう。加工変形することがまさに「隠れた独自のルール」です。
