TypeScriptで型レベル演算

はじめに

こちらは長野高専 Advent Calendar 2021の3日目の記事です。前日は @yabanui さんの｢Fusion360で基板設計～第2回「ライブラリーをつくろう②」～｣でした。僕には回路分野はさっぱりですね…

さて、皆さんTypeScriptは使いますか？今やTypeScriptはJavaScriptの代替言語としてWebフロントエンドだけではなく、広い分野で使われています。
TypeScriptの特徴として型の表現力の高さが挙げられます。動的型付け言語の中でもかなり型がゆるい方であるJavaScriptにどうにかして型を当てるためにTypeScriptには他の言語には無い、ユニークな型がたくさんあります。

結果として、TypeScriptの型はチューリング完全です。¹つまりTypeScriptの型だけでかなり色々な事ができるわけです。

ということで今回はTypeScriptの型で加算減算とそれを用いたRange型の実装をしてみたいと思います。

なお、今回実装したコードはこのGistに上がっていますので、詳しく見たい方は参照してください。

自然数型の定義

加算減算を実装するにもそもそも数を表す型がありません。まずは自然数型を定義してみましょう。自然数の表現はタプルを使い、数の大きさをタプルの長さで表現してみます。

// 自然数型
type Nat = unknown[];

// 以下は全てNatと継承関係にある(T extends Natが成り立つ)
type Zero = [];                 // 長さ0のTuple
type One  = [unknown];          // 長さ1のTuple
type Two  = [unknown, unknown]; // 長さ2のTuple
// ...

これだけではただ長さNのタプルを定義しただけで、それぞれの自然数型に関係性がありません。そこで、与えられた自然数型の次の値を返す型を作ってみます。自然数はペアノの公理によると、

ペアノの公理は以下の様に定義される。

自然数は次の5条件を満たす。

1. 0は自然数である。
2. 任意の自然数 a にはその後者 (successor)、suc(a) が存在する（suc(a) は a + 1 の "意味"）。
3. 0 はいかなる自然数の後者でもない（0 より前の自然数は存在しない）。
4. 異なる自然数は異なる後者を持つ：a ≠ b のとき suc(a) ≠ suc(b) となる。
5. 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。

だそうです。今回はこの2番目の条件

任意の自然数 a にはその後者 (successor)、suc(a) が存在する（suc(a) は a + 1 の "意味"）。

を使います。要は与えられたNat型の長さを+1して返せばよさそうですね。これはTypeScript 4.0で導入されたVariadic Tuple Typesを使えば簡単に実装できます。

type Suc<N extends Nat> = [...N, unknown];

このSuc<N>に[]を渡せば[unknown]が返ってきますし、[unknown]を渡せば[unknown, unknown]が返ってきます。これで｢任意の自然数の一つ後ろの数｣を表現できるようになりました。

加算･減算

加減算はどのように実装すればよさそうでしょうか？自然数をタプルの長さで表現しているので与えられた2つのタプルの長さを合わせれば加算は実装できそうです。実はこれもVariadic Tuple Typesを使えば簡単です。

type Add<N1 extends Nat, N2 extends Nat> = [...N1, ...N2];

減算は少し難しいですが、同じように実装できます。先にコードを示します。

type Sub<N1 extends Nat, N2 extends Nat> = N1 extends [...N2, ...infer Ans] ? Ans : Zero;

N1がN2よりも長い(つまりN1の方が大きい数)とき、N1 extends N2が成り立ちます。ここでinferキーワードを使えばN1がN2よりもどれだけ大きいかを型としてキャプチャできます。[...N2, ...infer Ans]とすることでN2からはみ出たunknownを配列としてキャプチャし、それをSub<N1, N2>の結果として返すことで減算が実装できます。なお、N2の方が大きい場合はN1 extends N2が成り立たないためZeroが返ります。²

リテラル型との相互変換

次にリテラル型との相互変換を実装してみましょう。リテラル型はTypeScript特有の型で、数値や文字列などのリテラルを直接型として使うことができます。

Nat型→リテラル型

ということで先程作ったNat型からリテラル型への変換を実装してみます。Nat型→リテラル型はかなり簡単に実装できます。

type NatToNum<N extends Nat> = N["length"];

TypeScriptではT[K]と書くとTのKプロパティを型として取得できます。タプルはArrayを継承しているのでlengthプロパティを持ちます。Arrayの場合lengthプロパティの型はnumberになりますが、タプルの場合はnumberのリテラル型として取得できます。結果的にN["length"]とするだけで簡単にリテラル型へ変換できます。

リテラル型→Nat型

さて次はリテラル型→Nat型ですが、これは少々面倒です。というのも一発でリテラル型をNat型に変換する手段がありません。
ここで再帰の力を借ります。Nat型→リテラル型はすでに実装済みなので、

1. [](0)のNat型を用意
2. Natをリテラル型に変換
3. 与えられたリテラル型と等しいか確認
4. 等しかったらその時のNatが答え
5. 等しくなかったらNatを1増やす
6. 2に戻る

これでリテラル型→Nat型が実装できます。何はともあれコードを見てみましょう。

type _NumToNat<L extends number, TNat extends Nat> = NatToNum<TNat> extends L ? TNat : _NumToNat<L, Suc<TNat>>;
type NumToNat<L extends number> = _NumToNat<L, Zero>;

まず_NumToNat<L, TNat>ですが、これは先程の手順の2〜6を行っています。リテラル型は派生型が無いため、Tがリテラル型の場合、T extends UはTとUが等しい値のときのみ成立します。NatToNum<TNat> extends Lが成立する場合はその時のTNatを返し、等しくない場合はTNatをSuc<N>で1増やして再帰しています。
NumToNat<L>は_NumToNat<L, TNat>にLと初期値のZeroを渡しているだけです。

Rangeを作ってみる

ここまで実装してきた自然数とリテラル型との相互変換を用いて、｢SからLまでのタプル｣を作るRange型を作ってみましょう(つまりPythonのrange関数みたいなのを作ります)。と言ってもRangeはdom.d.tsにすでに存在しているため名前はRange_にします。

type _Range<
  F extends Nat,
  L extends Nat,
  I extends Nat,
  Ans extends unknown[],
> = I extends Sub<L, F> ? Ans : _Range<F, L, Suc<I>, [...Ans, NatToNum<Add<F, I>>]>;
type Range_<F extends number, L extends number> = _Range<NumToNat<F>, NumToNat<L>, Zero, []>;

ちょっと複雑ですが、まずは_Range<F, L, X, Ans>から見ていきましょう。
F、Lはそれぞれ開始値と終了値のNat型です。そしてIは現在どこまでカウントしたかを保持するカウンタです。Ansは最終的な答えのタプルを保持しています。
まずI extends Sub<L, F>ですが、数え上げが終了したかどうかを判定しています。Sub<L, F>で求めたいタプルの長さが求まるのでIがそれに達しているかどうかが個々で判定できます。この条件を満たしている場合はそのときのAnsが答えになっているのでAnsをそのまま返します。

さて条件を満たしていないときの処理ですが、_Range<F, L, I, Ans>にFとLはそのまま、Iは1増やしたものを、Ansは末尾に現在のIとFを足したものを追加して渡しています。

Range_<F, L>は与えられたリテラル型をNat型に変換して、IとAnsには初期値を渡しています。

ちなみにAnsはnumber[]であることが自明なのですが、number[]にすると何故かTypeScriptがエラーを吐きます。どうやらNatToNumの型がnumberであることを推論できていないようですが、詳しいことはよくわかりません。直せる方がいたら編集リクエストをお願いします。

これでRange型が完成しました！あとはここに好きな数値リテラル型を入れてあげれば使えます。

最後に

TypeScriptの型は非常に強力で、型レベルで様々な事ができます。今回は使いませんでしたが、Template Literal Typeを使えば型レベルでSQLやGraphQLのパーサを作ることもできるようです。皆さんもTypeScriptのユニークな型を使って面白い型を作ってみましょう！

なお、TypeScriptの型の力を鍛えたい場合はType Challengeというリポジトリの問題を解いてみることをおすすめします。

明日の記事は @Shibaken_8128 の｢論理式簡略化アルゴリズムを実装｣です。どんな記事なのか楽しみですね！

それでは良いTypeScriptライフを！

1. とはいえTypeScriptの型には再帰上限とインスタンス化の上限があり、再帰上限は50とかなり低く設定されているため、複雑なことをするとすぐに再帰上限に引っかかります。 ↩

2. 本当はZeroよりもneverを返したほうがいいのかもしれませんが、今回はZeroにしています。 ↩