他言語の型システムに馴染みがある人向けのTypeScriptの型システムについてのメモです。個々の用語については『型システム入門』や適当な論文を参照してください。また、個々の型機能の詳細については TypeScript Documentation を参照してください。
合わせて読みたい: TypeScript: Handbook - TypeScript for Functional Programmers
- 部分型多相(subtype polymorphism)があります。
- 名前的部分型付け(nominal subtyping)ではなく、構造的部分型付け(structual subtyping)を採用しています1。クラス定義では一見、名前的部分型関係が導入されそうに見えますが型検査は構造的に行なわれます。
- パラメータ多相(parametric polymorphism。または総称型(generics))があります。2
- 型変数の変性(variance)があります。例えば、関数型は引数の型に関して反変(contravariant)で結果の型に関して共変(covariant)です(
--strictFunctionTypes
オプションを有効にした場合。このオプションを指定しない場合は、引数に関しては双変(bivariant)になります。これは不健全(unsound)です)3。- なお、
--strictFunctionTypes
を有効にした場合でも、メソッドやコンストラクタとして宣言した場合は、引数は依然として双変のままです。 4
- なお、
- 配列は共変です。
- 型変数の変性は
in
,out
で指定します。in
が反変、out
が共変、in out
とすると不変(invariant)です。変性を指定しない場合は型変数の使用位置から変性を推論します。 5 - 型変数の有界量化(bounded quontification)ができます6。ただし、下限境界を指定するための構文(Javaで言う
super
)はありません。 7 -
this
の型はF有界量化(F-bounded quantification)されています。8 - 合併型(union type)と交差型(intersection type)があります。9
- 型システムは不健全(unsound)です。10
- 型システムはチューリング完全です。ただし、処理系により再帰回数に制限が設けられています。
- conditional typeを使うと部分型関係を使って型レベルの分岐が書けます。11
- conditional typeの条件部で
infer T
と書くことで新しい型変数を導入し部分式で束縛できます12。導入した型変数は帰結部で参照できます。- また、条件部では同名の型変数を複数回指定することができます。複数回現れた型変数は、その型変数がすべて陰性位置(negative position)に現れていた場合は交差型で、すべて陽性位置(positive position)に現れていた場合は合併型で入力を合成した形で参照されます。陰性位置、陽性位置両方に現れる場合はすべてが同じ型に具体化されなければいけません。
- 例えば下記13の
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
の部分型です。 14 - いわゆる⊤型と⊥型があります。それぞれ名前は
unknown
とnever
です15 16。これらの型は、任意の型T
に対して、T <: unknown
かつT >: never
です。さらに、交差型と合併型に関してT & unknown = T
,T & never = never
,T | unknown = unknown
,T | never = T
です(&
や|
の左右を交換しても同じ)。 - 型を
any
にするとその部分の型検査を無効にできます。17 - プリミティブ型とオブジェクト型の区別があります。プリミティブ型には
string
,number
,boolean
,symbol
,bigint
,null
,undefined
があります。18 -
null
とundefined
はデフォルトではすべての型の部分型です。--strictNullChecks
オプションを指定すると、any
とunknown
以外には代入できなくなります。 19 - いわゆる
unit
型の名前はvoid
です。undefined
はvoid
の部分型です(return;
がundefined
を返すこととの整合性を取るため)。 20 -
object
型はすべてのオブジェクト型の上位型(super type)です。21 - 一方で、空のインタフェース
{}
は何らかのプロパティを参照できる型(オブジェクト型 + 「null
とundefined
を除いたプリミティブ型」)の上位型です(--strictNullChecks
オプションを有効にした場合)。 - 配列の部分型としてタプル型があります。例えば、
[string, number]
は長さ2で最初の要素がstring
, 次の要素がnumber
のタプル型です。タプル型[T1, T2, ...]
はArray<T1 | T2 | ...>
の部分型です。 22 - C#等の
enum
のように使えるenum
型があります。enum
型はnumber
の部分型です。 23 -
symbol
の部分型としてunique symbol
型があります。Symbol()
等の呼び出しが返す、既存の他のsymbol
と異なるsymbol
の型です。 24 -
--strictNullChecks
を有効にした場合の型の階層構造はこんな感じです。
- 代数的データ型はありません。下記のように、リテラル型と合併型を組み合わせて表現するイディオムがあります。 25
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)を持つインタフェースで表現します(関数型の合併型ではありません)。26
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)はありません27。おそらく、JavaのhighjやOCamlのhigherライブラリのような方法で模倣できるでしょう。
- 例えばfp-tsのHKTインタフェースは後者の方法にもとづいて実装されています(解説記事: TypeScriptで高カインド型(Higher kinded types) - Qiita)。
-
Function Parameter Bivariance / TypeScript: Handbook - Type Compatibility ↩
-
Optional variance annotations by ahejlsberg · Pull Request #48240 · microsoft/TypeScript ↩
-
Enable type parameter lower-bound syntax · Issue #14520 · microsoft/TypeScript ↩
-
Polymorphic this type / TypeScript: Handbook - Advanced Types ↩
-
A Note on Soundness / TypeScript: Handbook - Type Compatibility ↩
-
Type inference in conditional types / TypeScript: Handbook - Advanced Types ↩
-
Discriminating Unions / TypeScript: Handbook - Unions and Intersection Types ↩
-
Higher-kinded types / TypeScript: Handbook - TypeScript for Functional Programmers ↩