TypeScriptで超絶変態型計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

TypeScriptのジェネリック型定義を使って、コンパイル時にフィボナッチ数を計算してみます。面白いだけで、役には立ちません。$`\newcommand{\mrm}[1]{\mathrm{#1} }`$

内容：

はじめに
フィボナッチ数：数の計算の場合
型の世界の順序・型・関数
型の世界のブーリアンと自然数
ニューメラル・カインド
フィボナッチ数：型の計算の場合
おわりに

はじめに

TypeScriptコンパイラ〈トランスパイラ〉にフィボナッチ数を計算させたいと思います。計算するのは、JavaScriptエンジンではなくて、TypeScriptコンパイラです*1。fib.ts というファイルを tsc fib.ts というコマンドでコンパイルすると、空っぽのJavaScriptファイルが生成されます。計算はコンパイルの過程で行われるので、出力ファイルに意味はないのです。

なんでまた「コンパイラに計算させてみよう」と思ったかと言うと、TypeScriptのジェネリック型の定義に三項式〈if-then-else式〉が使えると知ったからです。例えば、型 X が値 null を許容する場合、型 never にしてしまい、そうでないならそのまま X を返すようなジェネリック型の定義は次のようになります。

type KillNull<X> = null extends X ? never : X;

/* ↓ OK */
let x :KillNull<number> = 1;

/* ↓ NG: Type 'number' is not assignable to type 'never'. */
let y :KillNull<number | null> = 1;

ジェネリック型 KillNull の定義に三項式を使っています。この定義を集合に対する演算と解釈して擬似コードで書くと次のようです。

$`\text{For a set }X\\
\text{KillNull}(X) := \\
\quad \text{if } \{\text{null}\} \subseteq X \text{ then }\emptyset
\text{ else }X\\
\:\\
1 \in \text{KillNull}(\text{number})\\
1 \not\in \text{KillNull}(\text{number} \cup \{\text{null}\})
%`$

TypeScriptでは型の定義に再帰も使えます。if-then-else と再帰が使えるなら何でも計算できます。試しにフィボナッチ数を計算してみよう、というわけです。

型の三項式〈if-then-else式〉を、TypeScriptでは条件付き型〈conditional types〉と呼んでいます。条件付き型に対する（ネタではない）解説は、次の記事が秀逸です。

Conditional Types in TypeScript by Marius Schulz

上記記事でも紹介されていますが、インストールされたTypeScriptパッケージ内の lib/lib.es5.d.ts に、実用的な条件付き型の事例があります。

この記事で使用しているTypeScriptコンパイラのバージョンは Version 4.6.2 です。コンパイラをインストールせずに試すには、TypeScriptプレイグラウンドがとても便利で楽しいです。この記事内のコードをコピペして遊んでみてください。

https://typescriptlang.org/ja/play 別URLにリダイレクトされたときは、リンクをたどってプレイグラウンドに行ってください。

フィボナッチ数：数の計算の場合

まず、通常の数の計算としてフィボナッチ数を扱います。フィボナッチ数列 0, 1, 1, 2, 3, 5, 8, 13, ... を計算する関数 fib をTypeScriptプログラムとして書きます。後で、このプログラムを“型の世界”に持っていくので、次のような制限を付けます。

使う型は、any, number, boolean の三種類だけ。
例外は使わず、エラーのときは error と名付けられた特定の値を返す。
関数の入力値の型チェックは、コンパイラに頼らず、型ガードコード（値の型を判定して分岐するコード）を書く。
TypeScriptが認識できる型ガード機能である正式な型述語〈type predicate〉は使わず、ユーザー〈プログラマ〉だけが分かるナンチャッテ型述語を使う。
if-then-else には三項式 ... ? ... : ... を使う。条件部は ... == true と（不要でも）書くことがある。

上記の項目には、プログラミングの常識からは好ましくないものもありますが、なぜこのような制限を付けるかと言うと、“型の世界”ではコンパイラが手厚いサービスを提供してくれないからです。“型の世界”で次のような機能は期待できません。

自由な“型の型”
例外メカニズム
ジェネリック型への型引数の“型の型”チェック
“型の型”述語
自由な制御構造

それでは、上記の制限・方針に従い、フィボナッチ数列を計算する関数を書いてみましょう。プログラムコードの前半は次のようです。

const error = "error";

function is_number(x:any) :boolean {
  return (
    typeof x == "number" ?
      true :
      false
  );
}

function succ(x:any/*number*/) :any/*number*/ {
  return (
    is_number(x) == true ?
      x + 1 :
      error
  );
}

function pred(x:any/*number*/) :any/*number*/ {
  return (
    is_number(x) == true ?
      x - 1 :
      error
  );
}

function is_zero(x:any) :boolean {
  return (
    x == 0
  );
}

function is_one(x:any) :boolean {
  return (
    is_zero(pred(x))
  );
}

エラーを表す値 error は計算結果の正常値（型 number の値）と区別できれば何でもいいので、ここでは文字列 "error" にしています。

関数 succ（後者関数）, pred（前者関数）の引数型に any/*number*/ と書いてあるのは次の意味です。

どんな引数でも受け入れるが、関数のなかで number かどうかの型チェックをする。

戻り値型の any/*number*/ は次の意味です。

引数の型チェック（型ガード）を通過した場合は、戻り値の型は number である。

コメントなので、ユーザー〈プログラマ〉の気持ちを表明しているだけで、コンパイラは何もしてくれません。

続きは以下のようです。

function is_nat(x:any) :boolean {
  return (
    is_zero(x) == true ?
      true :
      is_nat(pred(x)) == true ?
        true :
        false
  );
}

function add(x:any/*nat*/, y:any/*nat*/) :any/*nat*/{
  return (
    is_nat(x) == true ?
      is_nat(y) == true ?
        is_zero(x) == true ?
          y :
          succ(add(pred(x), y))
        :
        error
      :
      error
  );
}

function fib(x:any/*nat*/) :any/*nat*/ {
  return (
    is_nat(x) == true ?
      is_zero(x) == true ?
        0 :
        is_one(x) == true ?
          1 :
          add( fib(pred(pred(x))), fib(pred(x)) )
      :
      error
  );
}

is_nat は、自然数〈natunal number〉であるかどうかをチェックするナンチャッテ型述語（自前の型チェック用関数）です。自然数型は、ユーザーの気持ちのなかにあるだけで、コンパイラが認識できる型ではないことに注意してください。

add（足し算）と fib（フィボナッチ数列）は、（気持ちの上では）自然数に対する演算として定義されています。

次のプログラムコードは、fib がフィボナッチ数列を正しく計算することを確認する*2ものです。

const f0 = 0;
const f1 = 1;
const f2 = 1;
const f3 = 2;
const f4 = 3;
const f5 = 5;
const f6 = 8;
const f7 = 13;

console.assert(f0 == fib(0), "fib(0)");
console.assert(f1 == fib(1), "fib(1)");
console.assert(f2 == fib(2), "fib(2)");
console.assert(f3 == fib(3), "fib(3)");
console.assert(f4 == fib(4), "fib(4)");
console.assert(f5 == fib(5), "fib(5)");
console.assert(f6 == fib(6), "fib(6)");
console.assert(f7 == fib(7), "fib(7)");
console.log("Done");

型の世界の順序・型・関数

前節で、フィボナッチ数列を“数値の計算”により求めるプログラムを示しました。つまり、“値の世界”での話でした。これをほとんどそのまま“型の世界”に持っていきます。フィボナッチ数列を“型の計算”で求めます。

実際の“型の計算”コードを示す前に、“型の世界”がどんなものであるかを説明します。型を集合とみなして、集合論の用語で説明するのが分かりやすいのでそうします。

TypeScriptの型 any, number, boolean などは、値の集合と同一視します。そうすると、集合 any の部分集合 $`S \subseteq \text{any}`$ が（任意の）型です。“型の世界” とは、集合 any のベキ集合（すべての部分集合の集合）$`\mrm{Pow}(\text{any})`$ のことです。$`\mrm{Pow}`$ は power set ＝ベキ集合のことです。

勝手に選んだ集合 $`S\in \mrm{Pow}(\text{any})`$ が、TypeScriptの型システムで定義可能だとは限りません。定義不可能な超越的な型〈集合〉もあります。“型の世界”の住人で、タチの良いやつとだけ付き合うことにしましょう。TypeScriptで定義可能な型の集合を $`\mrm{TSType} \subseteq \mrm{Pow}(\text{any})`$ として、$`\mrm{TSType}`$ の範囲内で議論をします。

定義可能な型達の集合 $`\mrm{TSType}`$ には順序構造があります。型 $`X`$ が型 $`Y`$ の構造的サブタイプ〈structural subtype〉であることを $`X \preceq Y`$ と書くことにします。構造的サブタイプとは、TypeScriptにおけるサブタイプ／スーパータイプの関係です。

$`X \preceq Y`$ であることと、集合の意味で包含関係があること $`X \subseteq Y`$ が一致するかは怪しい（たぶん一致しない）ですが、関係 $`\preceq`$ が型の集合 $`\mrm{TSType}`$ 上のプレ順序関係〈preordered relation〉になることは仮定していいでしょう。つまり、次は使っていいとします。

$`\text{For }X \in \mrm{TSType},\; X \preceq X`$
$`\text{For }X, Y, Z \in \mrm{TSType},\; X \preceq Y \land Y \preceq Z \implies X \preceq Z`$

$`X \preceq Y \land Y \preceq X`$ から $`X = Y`$ が言えるかどうかも僕は未確認ですが、次のような同値関係 $`\simeq`$ は定義できます。

$`\quad \text{For }X, Y \in \mrm{TSType},\; X \simeq Y :\iff X \preceq Y \land Y \preceq X`$

この同値関係 $`\simeq`$ で商集合を作れば、サブタイプ／スーパータイプの関係 $`\preceq`$ は順序関係だと思ってもかまいません。このあたりはあまり神経質にならないことにします。

集合 $`\mrm{TSType}`$ の部分集合をカインド〈kind〉と呼ぶことにします。カインドは、プログラミング言語TypeScriptで自由に扱える概念ではありませんが、型の計算においては“型の型”の役割を果たします。

この記事では、型と集合を同一視してます*3。しかし、プログラミング言語と集合論では、呼び名や書き方が違います。念の為に確認しておきましょう（下）。

型 X ←→ 集合 $`X`$
型 never ←→ 空集合 $`\emptyset`$
型 null ←→ 単元集合 $`{\bf 1} = \{*\}`$
X extends Y ←→ $`X\preceq Y`$

"extends"〈拡張する〉という言葉の語感から、X をスーパータイプと誤解するかも知れませんが、X extends Y の X はサブタイプです*4。

いくつかの型〈集合〉を受け取って型〈集合〉を返す関数を、ここでは型関数〈type function〉と呼びます。ユニオン型 X | Y を作る縦棒演算子 | や、ペア型 [X, Y] を作る [ , ] などは型関数です。山形括弧に型引数〈型パラメータ〉を入れるジェネリック型はもちろん型関数です。

全域的（すべての型に対して定義される）型関数は、次の形の関数です。

$`\quad F:\mrm{TSType} \to \mrm{TSType}`$

型関数の定義域が特定のカインドに絞られることもあります。

$`\quad F:\mathscr{X} \to \mrm{TSType}\:\text{ where }\mathscr{X}\subseteq\mrm{TSType}`$

型関数の定義域となるカインドは、型のあいだの順序 $`\preceq`$ を使って定義されます（型引数の制約）。$`A`$ は与えられた型〈集合〉として、次の形のカインドです。これは、順序 $`\preceq`$ に関する下方集合〈lower set〉と呼ばれるものです。

$`\quad A\!\downarrow \,:= \{ X \in \mrm{TSType}\mid X \preceq A\}`$　$`A`$ のサブタイプからなるカインド

例えば、「配列型の最初の項目の型」という型関数を定義したいなら、その定義域は「1つ以上の項目を持つ配列の型」すべての集まりであるカインドです。「1つ以上の項目を持つ配列の型」のなかで最も一般的な型は [any, ...Array<any>] と書けるので、そのサブタイプ全体は「1つ以上の項目を持つ配列の型」のカインドになります。

参考までに、実際の「配列型の最初の項目の型」という型関数を書いてみると；全域的型関数として定義して、うまくいかない場合は never を返す方式が楽ちんです（型引数の制約はしてない）。

type FirstItemType<X> =
  // 型 X が、“最初の項目の型が F である一般的配列型”のサブタイプならば
  X extends [infer F, ...Array<any>] ?
    // パターンマッチした最初の項目の型 F を返す
    F :
    // そうでない（パターンマッチが失敗）ならば、never を返す
    never

// ↓ OK
let x :FirstItemType<[string, number, boolean]> = "hello";

// ↓ NG: Type 'number' is not assignable to type 'string'.
let y :FirstItemType<[string, number, boolean]> = 1;

// ↓ NG: Type 'string' is not assignable to type 'never'.
let z :FirstItemType<string> = "hello";

型の世界のブーリアンと自然数

型の世界のブーリアン〈真偽値〉を次のように定義します。

type TRUE = never;
type FALSE = null;

真が空集合〈never〉で偽が単元集合〈null〉なのは逆のような気がしますが、真偽値は区別できる2つの値なら何でもいいのです。今ここは型の世界なので、区別できる2つの型なら何でもいいわけです。

とはいえ、上のように選んだのには理由があって、TRUE = never としておくと、三項式〈if-then-else式〉の条件部 ... == true ? を ... extends TRUE ? と書けるのです。これは便利です。

型の二元集合である {TRUE, FALSE} は、型の世界のブーリアン型なのでブーリアン・カインドです。同様に、型の世界の自然数達からなる自然数カインドを定義しましょう。

型の世界の自然数を Zero = N0, One = N1, Two = N2, ... のように書くことにします。Zero, One, Two などはTypeScriptの型ですが、実際にどのような型にしましょうか？色々な定義があり得るでしょうが、ここでは次のようにします。

type I = 'I';

type Zero =[];
type One = [I];
type Two = [I, I];

I は、'I' という文字（TypeScriptでは長さ1の文字列）からなる単元型〈単元集合〉です。Zero, One, Two もそれぞれ型〈集合〉で次のようです。

Zero は、空配列だけからなる単元型。
One は、型 I のインスタンス値を最初の項目とする長さ1の配列の型。つまり、配列 ['I'] だけからなる単元型。
Two は、型 I のインスタンス値を最初の項目とし、型 I のインスタンス値を次の項目とする長さ2の配列の型。つまり、配列 ['I', 'I'] だけからなる単元型。

それぞれ、型 Zero, One, Two だけを要素として含む単元カインドを ZERO, ONE, TWO とします。

大丈夫でしょうか？自然数、単一の自然数を含む単元型、自然数を表す型、単一の自然数を表す型を含む単元カインドはすべて別物です。表にまとめましょう。

自然数	自然数の単元型	自然数を表す型	自然数を表す型の単元カインド
0	zero = {0}	Zero = {[]}	ZERO = {Zero}
1	one = {1}	One = {['I']}	ONE = {One}
2	two = {2}	Two = {['I', 'I']}	TWO = {Two}

自然数の単元型は“値の世界の型”ですが、自然数を表す型は“型の世界の値”です。どちらも単元集合ですが役割が違います。自然数はよく知られたものですが、“型の世界の自然数”である自然数を表す型 Zero, One, Two などは今決めたものです。それぞれが、どちらの世界に棲んでいて、どんな役割を担っているのか、注意深く区別してください。

自然数を表す型 Zero = N0, One = N1, Two = N2, ... をすべて寄せ集めた集合を NAT とします。NAT は型の集合なのでカインドです。

引数として渡された値がとある型のインスタンス値であるかどうか判断する関数が型述語でした。例えば、is_zero は、引数として渡された値が単元型 zero = {0} のインスタンス値であるかどうか判断する関数、つまり型述語です。

同様に、引数として渡された型がとあるカインドのインスタンス型であるかどうか判断する型関数をカインド述語〈kind predicate〉と呼びましょう。例えば、Is_ZERO は、引数として渡された型が単元カインド ZERO = {Zero} のインスタンス型であるかどうか判断する型関数です。

既に出てきた型述語（戻り値型はブーリアン型）、これから出てくるカインド述語（結果型はブーリアン・カインド）をまとめておきます。

値引数の型述語	型引数のカインド述語
is_zero(x)	Is_ZERO<X>
is_one(x)	Is_ONE<X>
is_nat(x)	Is_NAT<X>

値と型の二階層ならなんとかなっても、値・型・カインドの三階層になると途端にややこしくなります。とはいえ「たったの三階層」、落ち着いて値・型・カインドを区別しましょう。

ニューメラル・カインド

自然数の型 nat に対応するカインド NAT とは別に、ニューメラル・カインド NUMERAL を定義しておきましょう。

型 I はインスタンス値 'I' だけを持つ単元型でした。集合としては I = {'I'} です。項目の型が I である配列の型は Array<I> です。型 Array<I> のすべてのサブタイプからなるカインドが NUMERAL です。次のように書けます。

$`\quad \text{NUMERAL} := \{X \in \mrm{TSType} \mid X \preceq \text{Array}\langle \text{I}\rangle\}`$

NUMERAL は NAT と同じに思えるかも知れませんが、そうではありません。NAT は自然数の集合 nat と同型で、型 Zero, One, Two, ... を含みます。一方、NUMERAL には NAT に含まれない型も入っています。例えば、One | Two は NUMERAL に含まれる型です。One | Two を集合として書き下すと：

   One | Two
 = {['I']} ∪ {['I', 'I']}
 = {['I'], ['I', 'I']}

{['I'], ['I', 'I']} は Array<I> 型のサブタイプになりますが、二元型〈二元集合〉なので、NAT には入ってません（NAT に含まれる型はすべて単元型）。

ニューメラル・カインド NUMERAL が計算に必須なわけではないですが、自然数を表す型達のカインド NAT を含むもっと大きなカインドとして定義してみました*5。

さて、値・型・カインドの三階層、そして値の世界と型の世界を明確にするために、また表にまとめます。

値の世界	型の世界
値	型
型	カインド
型のインスタンス値	カインドのインスタンス型
関数	型関数
引数	型引数
引数の型	型引数のカインド
関数の戻り値	型関数の結果型
型述語	カインド述語

より具体的な対応は次のようです。ただし、型 number とカインド NUMERAL の対応はそれほどハッキリしたものではありません*6。カインド述語や型関数は次の節で定義されるものです。

値の世界	型の世界
ブーリアン型	ブーリアン・カインド
true, false	TRUE, FALSE
値 0	型 Zero
値 1	型 One
単元型	単元カインド
型 zero	カインド ZERO
型 one	カインド ONE
型 nat	カインド NAT
型 number	カインド NUMERAL
型述語 is_zero	カインド述語 Is_ZERO
型述語 is_one	カインド述語 Is_ONE
型述語 is_nat	カインド述語 Is_NAT
型述語 is_number	カインド述語 Is_NUMERAL
エラーを表す値 error	エラーを表す型 ERROR
関数 succ	型関数 Succ
関数 pred	型関数 Pred
関数 add	型関数 Add
関数 fib	型関数 Fib

フィボナッチ数：型の計算の場合

型計算によりフィボナッチ数列を計算するプログラムコードの前半は次のようです。

type ERROR = never;

type Is_NUMERAL<X> = /*BOOLEAN*/
  X extends Array<I> ?
    TRUE :
    FALSE
;

type Succ<X/*NUMERAL*/> = /*NUMERAL*/
  X extends Array<I> ? // Can not use Is_NUMERAL<X>
    [I, ...X] :
    ERROR
;

type Pred<X/*NUMERAL*/> = /*NUMERAL*/
  Is_NUMERAL<X> extends TRUE ?
    X extends [I, ...(infer P)] ?
      P : 
      ERROR
    :
    ERROR
;

type Is_ZERO<X> = /*BOOLEAN*/
  X extends never ?
    FALSE :
    X extends Zero ?
      TRUE :
      FALSE
;

type Is_ONE<X> = /*BOOLEAN*/
  Is_ZERO<Pred<X>> extends TRUE ?
    TRUE :
    FALSE
;

数の計算の場合とほとんど同じです。TypeScriptコンパイラの構文解析の都合から、型関数 Succ 内で Is_NUMERAL<X> と書きたかったけど書けなかったところだけ食い違っています。

残りのプログラムコードは以下です。

type Is_NAT<X> = /*BOOLEAN*/
  Is_ZERO<X> extends TRUE ?
    TRUE :
    Is_NAT<Pred<X>> extends TRUE ?
      TRUE :
      FALSE
;

type Add<X/*NAT*/, Y/*NAT*/> = /*NAT*/
  Is_NAT<X> extends TRUE ?
    Is_NAT<Y> extends TRUE ?
      Is_ZERO<X> extends TRUE ?
        Y :
        Succ<Add<Pred<X>, Y>>
      :
      ERROR
    :
    ERROR
;

type Fib<X/*NAT*/> =  /*NAT*/
  Is_NAT<X> extends TRUE ?
    Is_ZERO<X> extends TRUE ?
      Zero :
      Is_ONE<X> extends TRUE ?
        One :
        Add< Fib<Pred<Pred<X>>>,  Fib<Pred<X>> >
    :
    ERROR
;

型計算の場合、計算結果を確認するのが難しいです。計算結果の型を調べるコンパイラAPIがあるのかも知れませんが、とりあえず素朴な方法で；当該の型の変数を宣言し、変数に値を代入してみて型が正しいかどうか見当を付けます。以下のコードには代入文があるので、JavaScriptの実行コードが出力されます。

type N0 = Zero;
type N1 = One;
type N2 = Two;
type N3 = Succ<Two>;
type N4 = Succ<N3>;
type N5 = Succ<N4>;
type N6 = Succ<N5>;
type N7 = Succ<N6>;
type N8 = Succ<N7>;
type N13 = Succ<Succ<Succ<Succ<Succ<N8> >>>>;

const i :I = 'I'
const i0 :N0 = [];
const i1 :N1 = [i];
const i2 :N2 = [i, i];
const i3 :N3 = [i, i, i];
const i5 :N5 = [i, i, i, i, i];
const i8 :N8 = [i, i, i, i, i, i, i, i];
const i13 :N13 = [i, i, i, i, i, i, i, i, i, i, i, i, i];

let v0 :Fib<N0> = i0 ;
let v1 :Fib<N1> = i1;
let v2 :Fib<N2> = i1;
let v3 :Fib<N3> = i2;
let v4 :Fib<N4> = i3;
let v5 :Fib<N5> = i5;
let v6 :Fib<N6> = i8;
let v7 :Fib<N7> = i13;

型エラーは出ないので、型の計算結果は合ってそうです。

おわりに

タイトルに「超絶変態」と付けていますが、これは釣りタイトルです。実際に使っている方法は「ごく普通のいたって真っ当な」方法です。内容に正直なタイトルを付けるなら：

TypeScriptでごく普通のいたって真っ当な型計算

最初に出した“数の計算”としてのフィボナッチ数列は、書き方に制限を付けていますが、特に変わったことはしていません。“型の計算”としてのフィボナッチ数列はといえば、“数の計算”バージョンをそのまま型計算に書き換えただけです。

計算の舞台を、値の集合 $`\text{any}`$ から型の集合 $`\mrm{TSType} \subseteq \mrm{Pow}(\text{any})`$ に持ち上げただけで、まったく同じことをしているのです。もしそれが、「超絶変態」的に見えるとすれば、$`\text{any}`$ から $`\mrm{TSType}`$ のような“持ち上げ”があまり馴染みじゃない、という理由でしょう -- この機会に馴染んでみてはいかかでしょうか。

*1:「TypeScriptコンパイラもJavaScriptエンジンの上で走っているではないか」というツッコミは無し。

*2:8つの値を試しているだけなので甘い確認ですが、まーいいとしましょう。

*3:いつでも同一視していいわけではありません。例えば、型を余代数とみなすことがあります。

*4:語感（雰囲気）で判断するのは危険なのでやめましょうね。

*5:Array<I> は自然数の集合 $`{\bf N}`$ と集合としては同型です。そのサブタイプの集合はベキ集合 $`\mrm{Pow}(\text{Array}\langle\text{I}\rangle) \cong \mrm{Pow}({\bf N})`$ の部分集合です。超越的なサブタイプまで含めると、$`\mrm{Pow}(\text{Array}\langle\text{I}\rangle) \cong {\bf R}`$ となります。

*6:numberのインスタンス値をビット列表現して、ビット列で1となるインデックスの集合を、$`\mrm{Pow}(\text{Array}\langle\text{I}\rangle)`$ 内にエンコードすればハッキリした対応を作れます。が、そこまでする意味はないでしょう。