既にいろんな人がいろんなやり方でやっていると思うけど、自分もTypeScriptの型の世界で自然数を表現するというのをやってみた。

なんでそんなことを？と言うと、ただ「型で遊ぶ」という以上の意味はないです。

思ったよりかなり簡単に書けて、今のTSの表現力に驚いた。（TS4.1以上）

Gist版

// 配列の先頭以外を抜き取る型
type Tail<T extends any[]> = T extends [any, ...infer U] ? U : []

type Zero = []
type Succ = 'Succ'
type Next<T extends Nat> = [...T, Succ] // どっちかというとNextでやってることがSuccなんだけど,,,簡単のため妥協

// 自然数 Nat
type Nat = Zero | Succ[]

// Nat の値を人間が読めるように変換する型
type NatResolver<T extends Nat> = T['length']

// Nat を数値から生成
type NatGenerator<N extends number, Acc extends Nat = Zero> = Acc['length'] extends N
  ? Acc
  : NatGenerator<N, [Succ, ...Acc]>

// 加算
type Add<T extends Nat, U extends Nat> = [...T, ...U]

// 減算(マイナスになる場合はゼロ)
type Subtract<T extends Nat, U extends Nat> = U extends Zero ? T : Subtract<Tail<T>, Tail<U>>

// 乗算
type Multiply<T extends Nat, U extends Nat, Acc extends Nat = Zero> = U extends Zero
  ? Zero
  : U extends [Succ]
  ? Add<Acc, T>
  : Multiply<T, Tail<U>, Add<Acc, T>>

// 除算(切り捨て)
type Divide<T extends Nat, U extends Nat, Acc extends Nat = Zero> = U extends Zero
  ? never
  : T extends [Succ] | Zero
  ? Acc
  : Divide<Subtract<T, U>, U, Next<Acc>>

// 使用例
type One = Next<Zero>
type Two = Add<One, One>
type Three = Add<Two, One>
type Four = Multiply<Two, Two>
type Five = Add<Two, Three>
type Six = Multiply<Two, Three>
type Ten = NatGenerator<10>
type OneHundred = Multiply<Ten, Ten>

type n1 = NatResolver<One> // 1
type n2 = NatResolver<Two> // 2
type n3 = NatResolver<Three> // 3
type n4 = NatResolver<Four> // 4
type n5 = NatResolver<Five> // 5
type n6 = NatResolver<Six> // 6
type n10 = NatResolver<Ten> // 10
type n100 = NatResolver<OneHundred> // 100

type n24 = NatResolver<Multiply<Six, Four>> // 24
type n20 = NatResolver<Subtract<Multiply<Six, Four>, Four>> // 20

type n0_1 = NatResolver<Multiply<Zero, Six>> // 0
type n0_2 = NatResolver<Subtract<Two, Six>> // 0

type div_1 = NatResolver<Divide<Ten, Two>> // 5
type div_2 = NatResolver<Divide<Multiply<Six, Four>, Four>> // 6

ポイントとしては

• Tupleの長さで実際の数値を表現しているところ
• Variadic Tuple Types
• Tail
• ['length']
• Recursive Conditional Types

あたり。

Variadic Tuple Types はTuple型に ...T を使えるヤツ。これはめちゃめちゃ最高で、これのおかげで配列同士の結合とかがめっちゃ簡単に書ける。最高。（大事なことなので2回言った）

あと、Tuple型の ['length'] はただの number ではなく numeric literal type として実際の長さを返してくれるというところ。初めてこれを知ったときは長さを__型__として実際に取れるのか～👀と驚いた。

その辺のことはTuple型のドキュメントに書いてある: A tuple type is another sort of Array type that knows exactly how many elements it contains

まあなんというか、とにかく Tuple のおかげでいろいろ表現できる。

Tail は、今回は登場してない Head とあわせて型パズルではわりと頻出のテクニック。だと思う。いろいろ使える。

Head と Tail はなんというか、 OCaml とかでリストのパターンマッチするときに head と rest に分けるアレをTSの型でやるみたいなイメージ。

ちなみに Head の定義の仕方はいろいろあるけど、最もシンプルに書くとこんな感じ。

// 配列の先頭の要素を取り出す型
type Head<T extends any[]> = T[0]

あとは、Recursive Conditional Types。これはベースケース（再帰しないケース）に最終的には必ず到達するようにしておけば、 Conditional Types を再帰的に書けるというやつ。

再帰的な Conditional Types を再帰関数を書くメンタルモデルそのままで定義できる。やりたいことそのままを直感的に書けるので難しいハックとか知らなくてもよくなった。ウレシイ。

制限

ちなみに、recursion depth limits の制限があるので無限に大きい数を扱えるわけではなく、あまりに大きい数は制限に引っかかってエラーになる。まあ、あくまでただの型遊びなので、、、そこまで実用性を求めるものではアリマセン。

OCamlのばあい(オマケ)

ちなみに、Nat の部分はあんまり納得いってなくて、OCamlなら再帰ヴァリアント型を使ってこんな風に書きたいところ。

type nat = Zero | Succ of nat

TSではここまで完結に書けなくてちょっと妥協した。