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
レギュレーション
- 下記によって「数」を再帰的に定義
- 加法単位元(零元)を定義
- Aが「数」n であるときの、 n + 1 を定義
- 「数」a, b が「同値」である関係 a = b を定義
以上によって定義した「数」と「同値」を、TypeScriptの型で表現します。
定義した型を使って「1 + 2 = 3」1が正しく、「1 + 2 = 2」1と「1 + 2 = 4」1が誤りであることを、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であることが確認できました。
プログラムを動かさなくても、演算の結果が正しいかどうかを型エラーで検知することができました。
赤の波線でエラーがしめされています。
アプローチ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行しか残らないのがきれいです。
アプローチ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と抽象代数学の知識が必要です。
