TypeScriptで不動点コンビネータに型をつける

不動点コンビネータ

多くのプログラミング言語では、再帰関数を書くことができます。例えば、 JavaScript では fact 関数の定義の中で、自身の名前である fact を参照できます：

function fact(n) {
    return n === 0 ? 1 : n * fact(n - 1);
}
console.log(fact(5));

一方で、ある種のプログラミング言語（または計算体系）では、関数を定義する際に自身の名前を参照できません。（型無し）ラムダ計算がその代表例です。

しかし、型無しラムダ計算では不動点コンビネータと呼ばれるものを書くことができ、それを使うと再帰関数を書けます。不動点コンビネータの例としては、（名前呼びの体系で使える）Yコンビネータがあります：

Y = λf. (λx. f (x x)) (λx. f (x x))

fact = Y (λf. λn. if n == 0 then 1 else n * f (n - 1))

このYコンビネータは値呼びの体系では使えないので、値呼びの体系では別の形の不動点コンビネータ¹を使います：

Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

fact = Z (λf. λn. if n == 0 then 1 else n * f (n - 1))

このZコンビネータをJavaScriptで書くとすれば、次のようになります：

function fix(f) {
    return (x => f(y => x(x)(y)))(x => f(y => x(x)(y))); // 関数定義の中で fix という名前を使っていない！
}

let fact = fix(f => n => n == 0 ? 1 : n * f(n-1)); // 関数定義の中で fact という名前を使っていない！
console.log(fact(5));

let diverge = fix(f => x => f(x)); // 停止しない関数
diverge();

不動点コンビネータと型

型無しラムダ計算では不動点コンビネータを記述することができましたが、型がつくとそうでもなくなってきます。特に、単純型付きラムダ計算や System F では不動点コンビネータを記述できません。このような体系で再帰関数を書けるようにするには、言語組み込みの不動点コンビネータ、またはそれに相当するもの（let rec など）を用意しなければなりません。

しかし、再帰型があると、上記のZコンビネータに適切な型を与える（つまり、不動点コンビネータを体系内で記述する）ことができます。

特に、 TypeScript には再帰型があるので、さっき定義した fix 関数に型をつけることが可能です。

function fix<S,T>(f: (_:(_:S) => T) => (_:S) => T) {
    type U = (_:U) => (_:S) => T;
    return ((x:U) => f((y:S) => x(x)(y)))((x:U) => f((y: S) => x(x)(y)));
}

let fact = fix<number,number>((f: (_:number) => number) => (n: number) => n === 0 ? 1 : n * f(n-1));
console.log(fact(5));

let diverge = fix<any,never>((f: (_:any) => never) => (x:any) => f(x));
diverge(0);

上の例では、 fix 関数の中で定義している U という型が U = (_: U) => (_: S) => T を満たす再帰型です。定義の中で U 自身を参照しているのがポイントです。（このような型はどの言語でも書けるわけではありません）

なお、 TypeScript では関数の引数の型をある程度省略できるので、次のように書くこともできます：

function fix<S,T>(f: (_:(_:S) => T) => (_:S) => T) {
    type U = (_:U) => (_:S) => T;
    return ((x:U) => f(y => x(x)(y)))(x => f(y => x(x)(y)));
}

let fact = fix<number,number>(f => n => n === 0 ? 1 : n * f(n-1));
console.log(fact(5));

let diverge = fix<any,never>(f => x => f(x));
diverge(0);

ちなみに、再帰型を使わないやり方として、参照（変更可能な変数）を使ったものが「型システム入門」で紹介されています。

まとめ

TypeScript には再帰型があるのでヤバい

参考文献

「型システム入門 プログラミング言語と型の理論」：

• 第5章「型無しラムダ計算」 5.2「ラムダ計算でのプログラミング」
• 第11章「単純な拡張」 11.11「一般的再帰」
• 第13章「参照」 13.5「安全性」演習13.5.8
• 第20章「再帰型」 20.1「例」

1. Wikipediaの不動点コンビネータの記事ではZコンビネータと呼ばれています。 ↩