去年、TypeScriptの型についての小説を書いて、そのまま放置していた。せっかくなので、少し直して公開しておこうと思う。
プログラミング初心者、TypeScriptの初心者の読者を想定した内容になっている。
登場人物
- 私：高校2年生の女子。プログラミングと数学が好き。
- デルタ：高校1年生の男子。プログラミング初心者。
ある日の放課後、私が高校の図書館の自習室に入ると、デルタがノートパソコンを広げたまま、手を止めて画面を見ているのが目に入った。
「なにか困りごと？」
「先輩、ちょうどいいところに来ましたね。ちょっとTypeScriptのコードを書いていたらエラーが発生していて困ってたんです」
私はデルタのノートパソコンの画面を見た。
「型のエラーが出てるね」
デルタに指示を出し、コードを修正するとエラーは消えた。
「デルタってコンパイルエラーとか、型のことわかってる？」
「わかってますよ。文字列だったら stringとか、数だったら number とか、変数につけるヒントみたいなイメージですよね」
「他には？」私は否定せずに聞く。
「後は……真偽値のbooleanとか」
デルタは宙を見つめながらTypeScriptの型を思い出そうとしていた。
「まあ、具体例は他にも色々あるよ。string, number, boolean はプリミティブ型だけど、それ以外にも配列やオブジェクトもあるよね。ほかにはanyやneverとか」
「……そういえば！ TypeScriptの型について、一つどうしても納得できないものがあって...…」
デルタはパソコンのエディタを開き、次のコードを書いた。
const s: "foo" = "foo";
「TypeScriptって、こういう書き方ができますよね？ これって不思議じゃないですか。型を書くところに具体的な値が書けてしまうように見えるのが、納得できないんです」
「たしかに少し分かりづらいね。確認だけど、次の定数にはどんな値を代入することができる？」
const x : number = ???
「1とか、2とか」
「そうだね。3でもいいし、4でもいい。100でもいいし、-1000でもいい」
「数ならなんでもいいってことですね。最小値と最大値はありますけど」
「その通り。では次は?」
const isOk: boolean = ???
「trueかfalseですね」
「その通り。それ以外の値は入らない。型というのは、その値がある集合の要素であるということを保証するものなんだ」
「集合って、数学の集合ですか？」
「そう。数学の集合風に表記するとこのように書ける」
私はノートを取り出し、次のように書いた。
boolean = { true, false }
「２つしかないので、外延的に書くことができるね。numberの場合はそうはいかないので、内包的に書こう。厳密な範囲までは覚えていないから、こんな感じでどうだろうか」
number = { n | 最小値から最大値までの浮動小数点で表せる数 }
「先ほどデルタは型のことをヒントのようなイメージといったけど、集合のイメージのほうが正しい」
「なるほど。型が集合だとは考えたことがなかったです」
「では、リテラル型に話を戻そう。このリテラル型を集合論の記法で書けるだろうか」
type T = "foo"
私はデルタの前にノートとペンを差し出す。デルタはペンを手に取り、少しだけ考えてから手を動かした。
{ "foo" }
「こうでしょうか」
「その通り。このリテラル型は foo という文字列のみを許容する型だ。したがってただ一つの要素 "foo" を持つ集合とみなすことができるんだ」
「あ、そういうことなんですね。型のところに値が来るのが納得できなかったんですけど、そういう書き方なだけで集合なんですね」
「リテラル型が集合だということがわかれば、Union型も理解しやすいだろう」
「Union型ってなんでしたっけ」
「Union型は集合の言葉でいうと、和集合のことだ」
「和集合って…」デルタはノートにペンを走らせ、和集合のベン図を書いた。「……このことですよね」
「そうだ。和集合が2つ以上の集合を合成してできた型であるように、Union型は2つ以上の型を合成してできた型だ。| で型を並べて書くことで Union型を定義できる。このUnion型がどういう意味か、説明できる？」
type Status = "success" | "loading" | "error"
「"success", "loading", "error" のいずれかってことですよね。あ、なるほどこれはリテラル型という要素が一つしかない集合の和集合を作っているんですね」
こうしてデルタはTypeScriptのリテラル型を理解することができ、その応用としてUnion型の記法についても理解することができた。
そして私はデルタにTypeScriptの型を説明しながら、プログラミングと数学の関係に美しさを感じていた。
（おわり）
見ての通り、数学ガールのパロディだ。数学ガールなら、この後ミルカさんが現れてより数学的な話をしてくれるのだろう。カリー=ハワード同型対応に続けるなど、より高度な内容に踏み込んでくれたら面白くなりそうだ。
AIでコーディングすることが当たり前となった今、TypeScriptの型について理解していなくてもTypeScriptのコードを書く事ができてしまう。しかし型について理解するとプログラミングについての理解がかなり深まるので、TypeScriptを触る人には理解してほしい。
