TypeScriptの型メモ

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

合わせて読みたい: [TypeScript: Handbook - TypeScript for Functional Programmers](https://www.typescriptlang.org/docs/handbook/typescript-in-5-minutes-func.html)

* 部分型多相（subtype polymorphism）があります。
* 名前的部分型付け（nominal subtyping）ではなく、構造的部分型付け（structual subtyping）を採用しています[^subtyping]。クラス定義では一見、名前的部分型関係が導入されそうに見えますが型検査は構造的に行なわれます。
* パラメータ多相（parametric polymorphism。または総称型（generics））があります。[^generics]
* 型変数の変性（variance）があります。例えば、関数型は引数の型に関して反変（contravariant）で結果の型に関して共変（covariant）です（`--strictFunctionTypes` オプションを有効にした場合。このオプションを指定しない場合は、引数に関しては双変（bivariant）になります。これは不健全（unsound）です）[^function-parameter-bivariance]。
    * なお、`--strictFunctionTypes` を有効にした場合でも、メソッドやコンストラクタとして宣言した場合は、引数は依然として双変のままです。 [^strict-function-types-for-methods]
* 配列は共変です。
* 型変数の変性は`in`, `out`で指定します。`in`が反変、`out`が共変、`in out`とすると不変（invariant）です。変性を指定しない場合は型変数の使用位置から変性を推論します。 [^optional-variance-annotations]
* 型変数の有界量化（bounded quontification）ができます[^generic-constraints]。ただし、下限境界を指定するための構文（Javaで言う `super`）はありません。 [^lower-bound]
* `this` の型はF有界量化（F-bounded quantification）されています。[^f-bounded]
* 合併型（union type）と交差型（intersection type）があります。[^union-and-intersection]
* 型システムは不健全（unsound）です。[^unsound]
* 型システムはチューリング完全です。ただし、処理系により再帰回数に制限が設けられています。
* conditional typeを使うと部分型関係を使って型レベルの分岐が書けます。[^conditional-type]
* conditional typeの条件部で `infer T` と書くことで新しい型変数を導入し部分式で束縛できます[^infer]。導入した型変数は帰結部で参照できます。
    * また、条件部では同名の型変数を複数回指定することができます。複数回現れた型変数は、その型変数がすべて陰性位置（negative position）[^polarity]に現れていた場合は交差型で、すべて陽性位置（positive position）に現れていた場合は合併型で入力を合成した形で参照されます。陰性位置、陽性位置両方に現れる場合はすべてが同じ型に具体化されなければいけません。
    * 例えば下記[^infer-example]の`Fnn`では`infer T`はどちらも陰性位置に現れるため、帰結部の`T`は`Xnn`の右辺の`T1`, `T2`を交差型（`&`）で合成したものになります。
      ```typescript
      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`を合併型（`|`）で合成で合成したものになります。
      ```typescript
      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`になります。
      ```typescript
      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`と同じ型になります。
      ```typescript
      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` の部分型です。 [^literal-type]
* いわゆる⊤型と⊥型があります。それぞれ名前は `unknown` と `never` です[^unknown] [^never]。これらの型は、任意の型 `T` に対して、 `T <: unknown` かつ `T >: never` です。さらに、交差型と合併型に関して `T & unknown = T`, `T & never = never`, `T | unknown = unknown`, `T | never = T` です（`&` や `|` の左右を交換しても同じ）。
* 型を `any` にするとその部分の型検査を無効にできます。[^any]
* プリミティブ型とオブジェクト型の区別があります。プリミティブ型には `string`, `number`, `boolean`, `symbol`, `bigint`, `null`, `undefined` があります。[^object-and-primitive]
* `null` と `undefined` はデフォルトではすべての型の部分型です。 `--strictNullChecks` オプションを指定すると、 `any` と `unknown` 以外には代入できなくなります。 [^null-and-undefined]
* いわゆる `unit` 型の名前は `void` です。 `undefined` は `void` の部分型です（`return;` が `undefined` を返すこととの整合性を取るため）。 [^void]
* `object` 型はすべてのオブジェクト型の上位型（super type）です。[^object]
* 一方で、空のインタフェース `{}` は何らかのプロパティを参照できる型（オブジェクト型 + 「`null` と `undefined` を除いたプリミティブ型」）の上位型です（`--strictNullChecks` オプションを有効にした場合）。
* 配列の部分型としてタプル型があります。例えば、 `[string, number]` は長さ2で最初の要素が `string`, 次の要素が `number` のタプル型です。タプル型 `[T1, T2, ...]` は `Array<T1 | T2 | ...>` の部分型です。 [^tuple]
* C#等の `enum` のように使える `enum` 型があります。 `enum` 型は `number` の部分型です。 [^enum]
* `symbol` の部分型として `unique symbol` 型があります。 `Symbol()` 等の呼び出しが返す、既存の他の `symbol` と異なる `symbol` の型です。 [^unique-symbol]
* `--strictNullChecks` を有効にした場合の型の階層構造はこんな感じです。<br /> ![](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2215/c0d385a0-3645-1568-5a81-2be4daa2673f.png "TypeScriptの型階層")
* 代数的データ型はありません。下記のように、リテラル型と合併型を組み合わせて表現するイディオムがあります。 [^discriminating-unions]
  ```typescript
  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）を持つインタフェースで表現します（関数型の合併型ではありません）。[^overload]
  ```typescript
  interface PrimPrinter {
      (arg: number): string;
      (arg: string): string;
      (arg: boolean): string;
      (arg: null): string;
  }
  ```
* 一般化代数データ型（GADTs, generalized algebraic data types）はありません。が、[TypeScript で GADT っぽいの - Object.create(null)](https://susisu.hatenablog.com/entry/2020/05/03/020854) のように自前で型の等価性述語を持ち回れば部分的には表現できるようです（存在型の表現にはもう一工夫必要そうですが）。[OCamlの第一級モジュールを使った表現法](https://ocaml.org/releases/3.12/htmlman/manual021.html#toc81)も参考になるかもしれません。
* 高階多相（higher-order polymorphism。別名: higher-kinded polymorphism, higher-kinded types）はありません[^higher-kinded-types]。おそらく、Javaの[highj](https://github.com/highj/highj)やOCamlの[higher](https://github.com/ocamllabs/higher)ライブラリのような方法で模倣できるでしょう。
    * 例えば[fp-ts](https://gcanti.github.io/fp-ts/)のHKTインタフェースは後者の方法にもとづいて実装されています（解説記事: [TypeScriptで高カインド型(Higher kinded types) - Qiita](https://qiita.com/kgtkr/items/281b634987220d1d1ed5)）。

[^subtyping]: [TypeScript: Handbook - Type Compatibility](https://www.typescriptlang.org/docs/handbook/type-compatibility.html)
[^unsound]: [A Note on Soundness / TypeScript: Handbook - Type Compatibility](https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness)
[^generics]: [TypeScript: Handbook - Generics](https://www.typescriptlang.org/docs/handbook/generics.html)
[^overload]: [Overloads / TypeScript: Handbook - Functions](https://www.typescriptlang.org/docs/handbook/functions.html#overloads)
[^f-bounded]: [Polymorphic this type / TypeScript: Handbook - Advanced Types](https://www.typescriptlang.org/docs/handbook/advanced-types.html#polymorphic-this-types)
[^union-and-intersection]: [TypeScript: Handbook - Unions and Intersection Types](https://www.typescriptlang.org/docs/handbook/unions-and-intersections.html)
[^conditional-type]: [Conditional Types / TypeScript: Handbook - Advanced Types](https://www.typescriptlang.org/docs/handbook/advanced-types.html#conditional-types)
[^infer]: [Type inference in conditional types / TypeScript: Handbook - Advanced Types](https://www.typescriptlang.org/docs/handbook/advanced-types.html#type-inference-in-conditional-types)
[^polarity]: 関数の矢印の左側を陰性位置、右側を陽性位置と呼び、この陰性/陽性のことを極性（polarity）と呼びます。例えば、 `X => Y` であれば、Xは陰性位置であり、Yは陽性位置です。また、関数を入れ子にすると陰性位置では極性が反転します。 `(A => B) => (C => D)`であれば、A, Bは極性が反転し、Aは陰性×陰性で陽性、Bは陰性×陽性で陰性になります。`C => D`は陽性位置に現れるため極性はそのままで、Cは陰性、Dは陽性となります。
[^infer-example]: [Playground Link](https://www.typescriptlang.org/play?#code/C4TwDgpgBAKgjFAvFA3lAdlAXBgrgWwCMIAnKAXwFgAoUSWAJiVSgGds3gSBLdAcwo0adaADF06ADwANAHzNpUCAA9gEdABN2KGlD1QAZhwAUynLwOlYASiTz0BYiQDcu-QJynz6S2Ri3EeVYuXj4acigAflgOdAgAN1JXamFwaGkJZnEpFANPM1g4APtHJKgPKC9GYs4efnJZGgB6JrtCqAAyRiFaNKhRMDAZeWRFFTVNbTc9I3ycByJSGosrGGnykwLgur5ln1XwqJj5hKTU+mlBrMHJXLm8RZIa+GcN++3Q54YG5tbA9oAPt0Ur16OIhnIFEpVOotKh1rNKgUVn4agsnMl9G8kTgPvw9r5YIdojBYqcXOd0ugwFlqbc8jjCmjSi5sVU8bs2jBvo1qC02nFEmRABD-gFYieBQQAGRNVKVAMmAAPpMZDg+n3eDMx6vCrskL4rlwH58v7yeA9ET9QYMYZQ8awqbULGIqrGEDeQn+AUszVOdY6rZ6zn-FFE6gRElkoXJC2XMDKvQDONqxmunAar2PH1lf24wNfI38-4SoHcmhAA)
[^literal-type]: [TypeScript: Handbook - Literal Types](https://www.typescriptlang.org/docs/handbook/literal-types.html)
[^unknown]: [Unknown / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#unknown)
[^never]: [Never / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#never)
[^any]: [Any / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#any)
[^object-and-primitive]: [Object / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#object)
[^null-and-undefined]: [Null and Undefined / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#null-and-undefined)
[^discriminating-unions]: [Discriminating Unions / TypeScript: Handbook - Unions and Intersection Types](https://www.typescriptlang.org/docs/handbook/unions-and-intersections.html#discriminating-unions)
[^lower-bound]: [Enable type parameter lower-bound syntax · Issue #14520 · microsoft/TypeScript](https://github.com/Microsoft/TypeScript/issues/14520)
[^optional-variance-annotations]: [Optional variance annotations by ahejlsberg · Pull Request #48240 · microsoft/TypeScript](https://github.com/microsoft/TypeScript/pull/48240)
[^function-parameter-bivariance]: [Function Parameter Bivariance / TypeScript: Handbook - Type Compatibility](https://www.typescriptlang.org/docs/handbook/type-compatibility.html#function-parameter-bivariance)
[^strict-function-types-for-methods]: [TypeScript: Documentation - TypeScript 2.6](https://www.typescriptlang.org/docs/handbook/release-notes/typescript-2-6.html#note)
[^void]: [Void / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#void)
[^generic-constraints]: [Generic Constraints / TypeScript: Handbook - Generics](https://www.typescriptlang.org/docs/handbook/generics.html#generic-constraints)
[^object]: [Object / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#object)
[^higher-kinded-types]: [Higher-kinded types / TypeScript: Handbook - TypeScript for Functional Programmers](https://www.typescriptlang.org/docs/handbook/typescript-in-5-minutes-func.html#higher-kinded-types)
[^tuple]: [Tuple / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#tuple)
[^enum]: [Enum / TypeScript: Handbook - Basic Types](https://www.typescriptlang.org/docs/handbook/basic-types.html#enum)
[^unique-symbol]: [unique symbol / TypeScript: Handbook - TypeScript 2.7](https://www.typescriptlang.org/docs/handbook/release-notes/typescript-2-7.html#unique-symbol)