Edited at

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; // エラー出ない

上記のプログラムではTwoFourといった型にThree型の値を代入しています。一見間違っているようですが、当然すべてnumber型に含まれているためコンパイル時の型エラーは特になにも出ない、いたって正しいプログラムです。それが普通です。

「1 + 2 が3なのかどうか」といった演算の結果を確かめるのは型定義ではなくテストコードの役割だと思います。

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

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


環境


レギュレーション


  • 下記によって「数」を再帰的に定義


    • 加法単位元(零元)を定義

    • 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であることが確認できました。

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

TypeScript playground でエラーを見る

image.png

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


アプローチ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>を定義しようとしたところ、エラーが出てうまくいきませんでした。...TTarray型である時にしか使えないようですが、ConditionalTypeの中でTarrayであることを示す方法がわかりませんでした。

// 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と抽象代数学の知識が必要です。


参考





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