TypeScriptの型メモ #TypeScript

他言語の型システムに馴染みがある人向けのTypeScriptの型システムについてのメモです。個々の用語については『型システム入門』や適当な論文を参照してください。また、個々の型機能の詳細については TypeScript Documentation を参照してください。

合わせて読みたい: TypeScript: Handbook - TypeScript for Functional Programmers

部分型多相（subtype polymorphism）があります。
名前的部分型付け（nominal subtyping）ではなく、構造的部分型付け（structual subtyping）を採用しています¹。クラス定義では一見、名前的部分型関係が導入されそうに見えますが型検査は構造的に行なわれます。
パラメータ多相（parametric polymorphism。または総称型（generics））があります。²
型変数の変性（variance）があります。例えば、関数型は引数の型に関して反変（contravariant）で結果の型に関して共変（covariant）です（--strictFunctionTypes オプションを有効にした場合。このオプションを指定しない場合は、引数に関しては双変（bivariant）になります。これは不健全（unsound）です）³。
- なお、--strictFunctionTypes を有効にした場合でも、メソッドやコンストラクタとして宣言した場合は、引数は依然として双変のままです。 ⁴
配列は共変です。
型変数の変性はin, outで指定します。inが反変、outが共変、in outとすると不変（invariant）です。変性を指定しない場合は型変数の使用位置から変性を推論します。 ⁵
型変数の有界量化（bounded quontification）ができます⁶。ただし、下限境界を指定するための構文（Javaで言う super）はありません。 ⁷
this の型はF有界量化（F-bounded quantification）されています。⁸
合併型（union type）と交差型（intersection type）があります。⁹
型システムは不健全（unsound）です。¹⁰
型システムはチューリング完全です。ただし、処理系により再帰回数に制限が設けられています。
conditional typeを使うと部分型関係を使って型レベルの分岐が書けます。¹¹
conditional typeの条件部で infer T と書くことで新しい型変数を導入し部分式で束縛できます¹²。導入した型変数は帰結部で参照できます。
- また、条件部では同名の型変数を複数回指定することができます。複数回現れた型変数は、その型変数がすべて陰性位置（negative position）に現れていた場合は交差型で、すべて陽性位置（positive position）に現れていた場合は合併型で入力を合成した形で参照されます。陰性位置、陽性位置両方に現れる場合はすべてが同じ型に具体化されなければいけません。
- 例えば下記¹³のFnnではinfer Tはどちらも陰性位置に現れるため、帰結部のTはXnnの右辺のT1, T2を交差型（&）で合成したものになります。
```
type T1 = { n : number }
type T2 = { s : string }

type Fnn<X> = X extends {
    f : (x: infer T) => number
    g : (x: infer T) => string
} ? T : never;

type Xnn = Fnn<{f: (x: T1) => number; g : (x: T2) => string}>
// => T1 & T2
```
- 同様に、下記Fppではどちらも陽性位置に現れるためT1, T2を合併型（|）で合成で合成したものになります。
```
type Fpp<X> = X extends {
    f : (x: number) => infer T
    g : (x: string) => infer T
} ? T : never;

type Xpp = Fpp<{f: (x: number) => T1; g : (x: string) => T2}>
// => T1 | T2
```
  - 下記のFnpの場合では、infer Tが陰性位置、陽性位置両方に現れますが、Xnpの右辺ではinfer Tに合致する型が異なるため（T1 ≠ T2）条件部が偽になり結果は代替部に指定したneverになります。Xnp_2ではinfer Tに合致する部分にはどちらもT1を指定しているので条件部は真になり結果はT1になります。
```
type Fnp<X> = X extends {
    f : (x: infer T) => number
    g : (x: string) => infer T
} ? T : never;

type Xnp = Fnp<{f: (x: T1) => number; g : (x: string) => T2}>
// => never （∵T1 ≠ T2)
type Xnp_2 = Fnp<{f: (x: T1) => number; g : (x: string) => T1}>
// => T1
```
- また、下記のFpp2のfのyは陽性位置であるため（陰性位置の陰性位置なので極性が反転する）、結果はFppと同じ型になります。
```
type Fpp2<X> = X extends {
    f : (x: (y: infer T) => number) => number
    g : (x: string) => infer T
} ? T : never;

type Xpp2 =  Fpp2<{f: (x: (y: T1) => number) => number; g : (x: string) => T2}>
// => T1 | T2
```
シングルトン型（singleton type）があります（TypeScriptでの呼び名はリテラル型）。 number, string, boolean のリテラル値にその値と同名の型が付きます。例えば 42 の型は 42 です。 42 は number の部分型です。 ¹⁴
いわゆる⊤型と⊥型があります。それぞれ名前は unknown と never です¹⁵ ¹⁶。これらの型は、任意の型 T に対して、 T <: unknown かつ T >: never です。さらに、交差型と合併型に関して T & unknown = T, T & never = never, T | unknown = unknown, T | never = T です（& や | の左右を交換しても同じ）。
型を any にするとその部分の型検査を無効にできます。¹⁷
プリミティブ型とオブジェクト型の区別があります。プリミティブ型には string, number, boolean, symbol, bigint, null, undefined があります。¹⁸
null と undefined はデフォルトではすべての型の部分型です。 --strictNullChecks オプションを指定すると、 any と unknown 以外には代入できなくなります。 ¹⁹
いわゆる unit 型の名前は void です。 undefined は void の部分型です（return; が undefined を返すこととの整合性を取るため）。 ²⁰
object 型はすべてのオブジェクト型の上位型（super type）です。²¹
一方で、空のインタフェース {} は何らかのプロパティを参照できる型（オブジェクト型 + 「null と undefined を除いたプリミティブ型」）の上位型です（--strictNullChecks オプションを有効にした場合）。
配列の部分型としてタプル型があります。例えば、 [string, number] は長さ2で最初の要素が string, 次の要素が number のタプル型です。タプル型 [T1, T2, ...] は Array<T1 | T2 | ...> の部分型です。 ²²
C#等の enum のように使える enum 型があります。 enum 型は number の部分型です。 ²³
symbol の部分型として unique symbol 型があります。 Symbol() 等の呼び出しが返す、既存の他の symbol と異なる symbol の型です。 ²⁴
--strictNullChecks を有効にした場合の型の階層構造はこんな感じです。
代数的データ型はありません。下記のように、リテラル型と合併型を組み合わせて表現するイディオムがあります。 ²⁵
```
interface Some<T> { type: 'Some'; value: T; }
interface None { type: 'None'; }
type Option<T> = Some<T> | None;
```
occurrence typingがあります。上記の Option 型の値 obj に対して if (obj.type == 'Some') や switch (obj.type) { case 'Some': ... } のようにすると、分岐の中で型が詳細化されます。
いわゆるstratified type systemです。Coqで言う inject (xs: list A): Vec A (length xs) （長さなしリストから長さ付きリストへの変換）のような実行時の値に依存した型は書けません。というか依存型（dependent type）はありません。
オーバーロードされたメソッド/関数の型は複数の呼び出しシグネチャ（call signature）を持つインタフェースで表現します（関数型の合併型ではありません）。²⁶
```
interface PrimPrinter {
    (arg: number): string;
    (arg: string): string;
    (arg: boolean): string;
    (arg: null): string;
}
```
一般化代数データ型（GADTs, generalized algebraic data types）はありません。が、TypeScript で GADT っぽいの - Object.create(null) のように自前で型の等価性述語を持ち回れば表現できるようです。OCamlの第一級モジュールを使った表現法も参考になるかもしれません。
高階多相（higher-order polymorphism。別名: higher-kinded polymorphism, higher-kinded types）はありません²⁷。おそらく、JavaのhighjやOCamlのhigherライブラリのような方法で模倣できるでしょう。
- 例えばfp-tsのHKTインタフェースは後者の方法にもとづいて実装されています（解説記事: TypeScriptで高カインド型(Higher kinded types) - Qiita）。