1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

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

Last updated at Posted at 2019-07-15

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」と表現することになる 2 3

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?