部分型関係から考えるTypeScriptの`keyof`と`never`と`unknown`

はじめに

TypeScriptはkeyofという型演算子を備えています。名前からも類推できるように、keyofは直感的にはオブジェクトの型のキーを取り出す演算子です。例えば、以下のように使います。

type T = { a: number, b: string }
type Key = keyof T // "a" | "b"

型Tは"a"と"b"というキーを持つ型なので、keyof Tは"a" | "b"型になるというわけです。

では、keyof neverやkeyof unknownはどうなるでしょうか？

type KeyOfNever = keyof never // ???
type KeyOfUnknown = keyof unknown // ???

後に見るように、どんな型TをとってきてもneverはTの部分型であることと、Tはunknownの部分型であることがneverとunknownのそれぞれの特徴です。しかし、具体的にはどんな型なのでしょうか？そうした型のキーとは？ちょっと想像しにくいのではないでしょうか。

以下では、keyof neverとkeyof unknownのいい感じの定義を決めるための考え方を紹介していきます。例えば、指数関数を例としてみましょう。正の実数$a$に対して$a^0 = 1$と定めておくと、どんな実数$r, s$に対しても$a^{r+s} = a^r \cdot a^s$が成り立つ（いわゆる指数法則）ので嬉しいです。keyof neverとkeyof unknownに関しても、同様の説明が可能ということをこれから見ていきましょう。ただし、全体を通してanyは存在しないものとします。面倒なので。

本稿は次のような構成をとります。まず、部分型関係という概念について説明します。keyofのいい感じの定義は、この部分型関係に関わるものです。次に、keyofと少なからぬ関わりを持つ|と&というお馴染みの演算子を、部分型関係を使って定義します。そのあと、keyofの定義域と値域について確認します。とりわけ値域は、keyofと部分型関係の関係において重要な役割を果たします。そして、本丸のkeyof neverとkeyof unknownの定義を確認し、「部分型関係を逆転させるという性質を維持する」という観点でその定義の正当化を試みます。最後に、|、&、そしてkeyofと部分型関係の持つまた別の性質について触れます。

本稿の想定する読者は、TypeScriptの型システムをある程度使いこなせているプログラマーになります。各演算子や型の簡単な説明はありますが、見たことすらないという状態だと読み通すのは難しいかもしれません。

また、一つの謝辞として、Xのフォロワーからあるissueを紹介してもらったことが執筆のきっかけになったことを付言しておきます。

https://x.com/re_taro_/status/1834505254492062140

筆者自身、keyofの挙動についてしっかり考えたことがなかったのですが、このやりとりをきっかけに理解が深まりました。感謝

部分型関係

部分型関係は型同士の関係^[1]です。型Aが型Bの部分型(subtype)であるとき、Aに型付けられた項はBとしても型付けることが可能です。このとき、BをAの上位型(supertype)とも呼びます。

部分型関係は、TypeScriptの文脈では"assignability"という言葉で説明されることも多いです。例えば、以下のコードは型検査をパスします。

const a: { k1: number, k2: string } = { k1: 1, k2: 2 }
const b: { k1: number } = a // 割り当て(assign)可能

aをbに割り当てても安全なのは、bの型はk1キーがnumber型であることだけを要求しているので、他にどんなキーを持っていようが関係がないからです。TypeScriptコンパイラはbがk1を持つことしか知らないので、他のキーへのアクセスを許してくれません。

b.k1 // ok
b.k2 // type error!
b.foo // type error!

また、型の条件部に現れるextendsも部分型関係を表します。すなわち、A extends BはAがBの部分型であることを意味します。

type T = { k1: number, k2: string } extends { k1: number } ? true : false // true

{ k1: number, k2: string }は{ k1: number }の部分型なのでTはtrueとなります。

さらに、どんな型Tに対してもTはTの、つまり自分自身の部分型です。型が同じだったら割り当てられるのは当然ですね。

|と&と部分型関係

|と&というお馴染みの型演算子は、部分型関係に関わるある性質を持っています。すなわち、AとBを型としたとき、A | BはAとBの上位型であり、A & BはAとBの部分型である、という二つが成り立ちます。

むしろ、本稿の趣旨からすれば、こう説明するのが適切でしょう。|は与えた2つの型の上位型の中でも一番小さい型を返し、&は、2つの型の部分型の中でも一番大きい型を返すのが定義であると。ここでの「小さい」と「大きい」は部分型関係に対応しています。AがBの部分型ならAはBよりも小さい型であり、BはAよりも大きい型です。

なんだか小難しい説明になってしまったので、具体例を示しましょう。

type U = string | number
let u: U = "hello"
u = 3
type Left = { a: string }
type Right = { b: string }
type I = Left & Right // { b: string }
declare const i: I
const left: Left = i
const right: Right = i

型Uはstringかnumberを要求するので、stringの値もnumberの値も代入していいのは当然でしょう。そして、stringとnumberの上位型はstring | numberだけではありません。string | number | Dateやstring | number | booleanもそうですし、列挙しきれません。しかしそれらはどれも、string | numberの上位型なので、string | numberが一番小さいのです。

また、ここの型Iは{ a: string, b: string }と等価です。これに対しても|と同様の説明が可能です。LeftとRightの部分型は{ a: string, b: string }だけではありません。{ a: string, b: string, c: string }もそうです。しかし、一番大きい型が{ a: string, b: string }なのはこれまでの説明から納得いただけるかと思います。

keyof

さて、前置きがすでに難しい気がしてましたが、本題のkeyofです。

定義域と値域

keyofはどんな型でも受け取れる型演算子なので、定義域はTypeScriptの型全体の集合になります。他方、値域はstring | number | symbol^[2]の部分型の集合になります。というのも、t, keyを項としたとき、t[key]という構文が許されるのはkeyの型がstring | number | symbolの部分型のときだからです。つまり、TypeScriptにおいてはt[true]などは不正な表現ということになります（なお、JavaScriptでは許されています）。

ここではとりわけ値域が重要です。なぜなら、keyofは部分型関係を逆転させるという性質を持っており、それがkeyof neverとkeyof unknownの定義に関わるからです。

部分型関係の逆転

「keyofが部分型関係を逆転させる」とはすなわち、AがBの部分型であるとき、keyof Bはkeyof Aの部分型であることを意味します。例えば、{ a: number, b: string }は{ a: number }の部分型なので、keyof { a: number }はkeyof { a: number, b: string }の部分型となります。keyof { a: number }は"a"型で、keyof { a: number, b: string }は"a" | "b"型です。確かに逆転しています！

keyof neverとkeyof unknown

さて、核心に辿り着きました。keyof neverとkeyof unknownはどうなるでしょうか？この「部分型関係を逆転させる」という法則を維持する定義にしたいのです。

本稿の冒頭で述べたように、どんな型Tに対してもneverはTの部分型です。つまり、それを逆転させるためには、どんなTに対してもkeyof neverはkeyof Tの上位型となるように定めるべきです。keyofの値域はstring | number | symbolの部分型の集合だったことを思い出してください。そう、keyof neverはstring | number | symbolとなるのです！

では、keyof unknownはどうでしょうか？unknownはどんな型Tに対してもTの上位型です。よって、keyof unknownはkeyof Tの部分型となるわけです。すなわち、keyof unknownはneverとなります。

type KeyOfNever = keyof never // string | number | symbol
type KeyOfUnknown = keyof unknown // never

|と&とkeyof

最後に、keyofがもう一つの性質を持っていることに簡単に触れておきます。どんな型A, Bに対しても以下が成り立ちます^[3]。

keyof A | keyof B = keyof (A & B)

keyof neverとkeyof unknownの定義はこの性質も維持します。A、Bにneverとunknownを当てはめてみて、これが実際に成り立っていそうなことをお手元で確認してみてください^[4]。

終わりに

以上、部分型関係を手がかりとしたkeyofの解釈を試みました。読者の中には、「こういう性質を満たしたからといって何が嬉しいのか？」という疑問を持った方もいらっしゃるかもしれません。その疑問は全く正当だと思います。冒頭で紹介したissueにおいて、「最初はkeyof neverをneverとして定義したが多くの問題が発生した」というような旨が書かれていますが、それらが具体的にどんな問題なのかは調べられていませんし、筆者も具体例を述べることは正直のところできません。また、「こうした性質は純粋に数学的な関心事であり、現場のプログラマにとってはどうでもよい」という主張にも正面切って反論する材料を持ち合わせていません^[5]。ただ、「演算子がある法則に沿うように定義されていると理解することで、挙動を予想しやすくなる」というメリットはあるのではないかと考えています。これは疑いなく実践的なメリットではないでしょうか。

脚注

1. ここで言う「関係」は数学的な意味での関係ですが、「親子関係」のような日常的な意味で理解してもさしあたり問題ないと思います。

2. このエイリアスとして、PropertyKey型がグローバルに利用できます。

3. これはTypeScriptの式ではなく、メタ的なものであることに注意してください

4. 一般的な法則が成り立っていることをコードから確認する術はありません。我々にできるのは、個々の具体例に対して成立していることを確認することだけです。

5. Array.prototype.everyの空配列に対する挙動について話題になったことが思い出されます https://zenn.dev/ncdc/articles/e110ec7d92a8a1