TypeScriptで、プログラムを動かさず型定義だけで足し算の結果を得たい選手権

TypeScriptでは静的型定義を使うことで、変数に予期せぬ値が入ってこない事を保証できます。

ですが、当たり前ですがそれ以上の事はできません。

例えば下記のプログラム

type One    = number;
type Two    = number;
type Three  = number;
type Four   = number;

const three: Three = 3;

const valA: Two   = three; // エラー出ない
const valB: Three = three;
const valC: Four  = three; // エラー出ない

上記のプログラムではTwoやFourといった型にThree型の値を代入しています。一見間違っているようですが、当然すべてnumber型に含まれているためコンパイル時の型エラーは特になにも出ない、いたって正しいプログラムです。それが普通です。
「1 + 2 が3なのかどうか」といった演算の結果を確かめるのは型定義ではなくテストコードの役割だと思います。

ですが、こういった演算の結果を、型定義だけを使って確かめる事はできないかと思いました。そこで「TypeScriptでプログラムを動かさず、型定義だけで足し算の結果を得る」ことはできないか、試してみました。

TypeScriptの静的型付けだけでどこまで「プログラムの正しさ」を表現できるのか、すこし見てみましょう。

環境

TypeScript 3.5.1
- TypeScript playgroundを利用

レギュレーション

下記によって「数」を再帰的に定義
- 加法単位元(零元)を定義
- Aが「数」n であるときの、 n + 1 を定義
「数」a, b が「同値」である関係 a = b を定義

以上によって定義した「数」と「同値」を、TypeScriptの型で表現します。

定義した型を使って「1 + 2 = 3」¹が正しく、「1 + 2 = 2」¹と「1 + 2 = 4」¹が誤りであることを、TypeScriptのプログラムを動かさずに型定義のエラーによって示すことを目指します。

ここで言う型定義のエラーとは、TypeScriptをStrict Modeでコンパイルできないこと(TypeScript playgroundでAlways Strictを有効にし、赤の波線が表示されること)とします。

アプローチ1: 次元数風の定義

0 := ∅ (空集合)
1 := [∅]
2 := [[∅]]
3 := [[[∅]]]

のように、集合の次元数を「数」と定義してみます。

// 零元を空集合
type Zero = null;
// Aが「数」nであるとき、n + 1 は [A]
type Increment<T> = [T];

AとBが「同値」であることの定義は「型Aに型Bが代入できる」とします。

数の定義はこんなかんじになります。

type One    = [null];
type Two    = [[null]];
type Three  = [[[null]]];
type Four   = [[[[null]]]];

下記のように定義しても同様です。

type One    = Increment<Zero>;
type Two    = Increment<One>;
type Three  = Increment<Two>;
type Four   = Increment<Three>;

実際の演算はこんな感じです。

function plusOne<T>(val: T): Increment<T> {
  return [val];
}

const zero: Zero = null;
const one: One = plusOne(zero);
const two: Two = plusOne(one);

const result = plusOne(two);
const valA: Two   = result; // Error
const valB: Three = result;
const valC: Four  = result; // Error

無事に2と4で型定義のエラーが出て、答えが3であることが確認できました。

プログラムを動かさなくても、演算の結果が正しいかどうかを型エラーで検知することができました。

TypeScript playground でエラーを見る

赤の波線でエラーがしめされています。

アプローチ2: 順序数風の定義

0 := ∅ (空集合)
1 := [∅]
2 := [∅, [∅]]
3 := [∅, [∅], [∅, [∅]]]

のように、順序数の定義のような集合を用意し、これを「数」としてみます。

// 零元を空集合
type Zero = never;
// Aが「数」nであるとき、n + 1 は A ∪ [A]
type Increment<T> = T | [T];

この時、AとBが「同値」であることの定義は、(A∪B)⊆(A∩B)とします。

type Equal<T,U> = T | U extends T & U ? any : never;

数の定義はこんな感じ。

type One    = [never];
type Two    = [never] | [[never]];
type Three  = [never] | [[never]] | [[[never]]];
type Four   = [never] | [[never]] | [[[never]]] | [[[[never]]]];

実際の演算は、こんな感じです。

// 1 + 1
type OnePlusOne = Increment<Increment<Zero>>;
// 2 + 1
type Result = Increment<OnePlusOne>;

const valA: Equal<Result, Two> = null;   // 2 + 1 = 2: Error
const valB: Equal<Result, Three> = null; // 2 + 1 = 3
const valC: Equal<Result, Four> = null;  // 2 + 1 = 4: Error

こちらも無事に型エラーを出し、演算結果が3であると得ることができました。

同値の定義がちょっと冗長なものの、ほとんどを型で表現できておりJavaScriptにコンパイルすると最後の3行しか残らないのがきれいです。

TypeScript playgroundでエラーを見る

アプローチ3: 基数風の定義

0 := []
1 := [1]
2 := [1, 2]
3 := [1, 2, 3]

上記のように、「数」を集合の濃度として定義しようとしました。定義としては最も直感的かもしれません。

しかし、Increment<T>を定義しようとしたところ、エラーが出てうまくいきませんでした。...TはTがarray型である時にしか使えないようですが、ConditionalTypeの中でTがarrayであることを示す方法がわかりませんでした。

// A rest element type must be an array type.
type Increment<T extends any[]> = T extends Array<infer U> ? [U, ...T] : never;

結果。
一応エラーは出るのですが「数」の定義がうまくいっていないので、これは納得できません。

type One    = [number];
type Two    = [number, number];
type Three  = [number, number, number];
type Four   = [number, number, number, number];

const three: Three = [1,2,3];

const valA: Two   = three; // Error
const valB: Three = three;
const valC: Four  = three; // Error

まとめ

ここまでやってみたのですが、やはり「数」だけでなく、数と数との「演算」が定義されていないと面白くないですね。もっとTypeScriptと抽象代数学の知識が必要です。

参考

本稿では任意のa, bに対する演算a+bを定義していないため、実際には「1 + 2」を表現することはできず「((0 + 1) + 1) + 1」と表現することになる ↩