TypeScriptから構造体を奪って、関数だけでまた構造体を得るまでの道のり (チャーチ・エンコーディング)

これは定理証明支援系 Advent Calendar 2023の参加記事です。

https://adventar.org/calendars/9022

なお、この記事はさほど定理証明は直接的には関係ありませんが、「周辺の分野」ということで寄稿させていただきました。

概要

この記事はラムダ計算などで登場する概念を、もっと身近な言語で説明してみよう、という試みのうちのひとつです。最初はチャーチ・エンコーディングの "気持ち" の部分をとりあえず理解するための記事を作ってみました。

(この他にもシリーズを展開していきたいなと思っています)

対象読者

• 関数だけでどこまでできるか、関数の限界を知りたい人
• ラムダ計算・TaPLをこれから勉強したい人
• チャーチ数・チャーチエンコーディングを勉強したものの、その "気持ち" を知りたい・納得したい人
• 白紙からチャーチ数・チャーチブール等の定義を構成できるようになりたい人
• チャーチ数 (チャーチ・エンコーディング) のちょっと変わった入門をしたい人
• 関数型のちょっと変わった入門をしたい人
• 再帰型と帰納型と違いが知りたい人
• 推奨: JavaScript/TypeScript、さらにRust(もしくはHaskellやOCamlなど)が多少わかるとよみやすいです
• 発展: ラムダ計算に触れたことがある方は、「ラムダ計算では」の折りたたみを見ながら読み進めてみてください

TypeScriptの部分言語を考える

この記事では、最終的にTypeScriptの一部の機能のみを使ったサブ言語みたいなものをベースにします。

簡単のため、この記事ではプラクティス的に readonly をつけるべき場所でもつけていません。

また、JavaScript/TypeScriptに関して、関数のみを許可した部分的な言語を考えてみてください。

ただし、以下も禁止されています。

• 循環参照(値):
  • const a = {}; a.foo = a; のようにして作られた a
  • function f(x) { return x } のようにして作られた f
• 循環参照(型): type Foo = { foo: Foo } | null のような型

また、途中までは、説明のために文字列リテラル型や一部のリテラル型を使います。また、説明のために、特別な注釈がある場合は許可されます。

構造体(判別共用体,タグ付きユニオン)

構造体というのは、次のような、オブジェクト型のユニオン型であって、 D という名前の識別用のフィールドを持つ型としておきましょう。

Dはdiscriminantを略して

構造体、というよりここでは判別共用体(discriminated union)をベースとしていきます。判別共用体は判別子(discriminant)を共通で持って判別できる型になります。

例えば、

type Person = { name: string; age: number; };
type Pet = { age: number; weight: number; };
type Member = Person | Pet;

TypeScript Playground

という型定義を考えて、 Member型の値がPersonかPetかを判別するために、 'name' in member とすることもできます。

そのような内部的な特徴に依存することなく、共通で識別用のフィールドを持つスタイルを（少なくともJavaScript/TypeScriptにおいてはこの定義で）判別共用体と呼びます。

type Person = { discriminant: 'person'; name: string; age: number; };
type Pet = { discriminant: 'pet'; age: number; weight: number; };
type Member = Person | Pet;

TypeScript Playground

TypeScriptのみで考えても判別共用体をあえて用いるメリットは大きく、私は基本的にこのスタイルを採用するようにルールとして持ちます。

また、C言語やRustでメモリレベルの構造体の設計をしなければならない場合は、違う構造で同じメモリを判別子によって別の目的で使い分けることで大きな意味があります。
(余裕があれば後でこちらに関した説明を追記します)

例えば、これさえあれば boolean だって表現できてしまいます。

type Bool = {
  D: 'true';
} | {
  D: 'false';
};

TypeScript Playground

すると true は { D: 'true' } として表現できます。演算子 && は次のようにかけます。

const bool_and = (b1: Bool, b2: Bool): Bool => {
  switch (b1.D) {
    case 'true': {
      switch (b2.D) {
        case 'true': return { D: 'true' };
        case 'false': return { D: 'false' };
      }
    }
    case 'false': {
      return { D: 'false' };
    }
  }
};

なお、後の説明で比較してわかりやすいようにswitchをあえて使用しています。
とてもめんどくさく感じるかもしれませんが、これで boolean ( true | false ) はこの構造体の仕組みの上で表現できることがわかりました。

BoolはRustで書くと？

enum Bool {
    True,
    False,
}

fn bool_and(b1: Bool, b2: Bool) -> Bool {
    match (b1, b2) {
        (Bool::True, Bool::True) => Bool::True,
        _ => Bool::False,
    }
}

Rust Playground

その他の構造体

構造体の他の例も以下に乗せていきます。

その他の構造体: 直積型

type Pair<T1, T2> = {
  D: 'intro';
  v1: T1;
  v2: T2;
};

交差型(共通部分) T1 & T2 とは異なるので注意してください。タプル型 [T1, T2] に相当します。

集合論でいえば、 $T_1 \times T_2 = \{ (x, y) ; x \in T_1, y \in T_2\}$ を作る操作に相当します

その他の構造体: 直和型

type Either<Left, Right> = {
  D: 'intro_left';
  left: Left;
} | {
  D: 'intro_right';
  right: Right;
};

Eitherとは英語表現 either A or B (A か B (のどちらか)) からきています。

合併型(ユニオン型, 共用型) T1 | T2 とは異なるので注意してください。タプル型のユニオン [false, T1] | [true, T2] に相当します。

重要なのは、例えば T1 = T2 = number だったとしても、T1のほうのnumber, T2のほうのnumberというのを区別できるというところです。
{ D: 'intro_left', left: 3 }: Either<number, number> と { D: 'intro_right', left: 3 }: Either<number, number> は別物としてみなせるということです。

v: number | string は typeof v === 'number' とすれば厳密に区別できるので、直和型を使うというのはなかなか馴染みがないかもしれないですが、関数型言語ではよく見られます。
また、ややこしいことを書きますが、そもそも判別共用体そのものが (対象の型の数を任意の個数に一般化した) 直和型です。その意味では、この Either 型はとても基礎的な例なのです。

JavaScriptの値はすべて直和型

なんなら、動的型付けの内部実装は typeof v を返すためにランタイムの内部的に判別子を持っているはずで、任意の値 v とは、 typeof v を判別子に持つ直和型（判別共用体）なのです。
(という捉え方もできますよ、という話です)

もっとも、より厳密にはJavaScriptの typeof は [[Call]] (呼び出し用の内部スロット = ランタイム内部用のプロパティみたいなもの) があれば "function" を返す、のように、まったくもって判別共用体のスタイルのセマンティクスではないのですが...

集合論でいえば、 特別な要素 $* \not\in T_1 \cup T_2$ を用いて $\{ (*, x) ; x \in T_1 \} \cup \{ (x, *) ; x \in T_2\}$ を作る操作に相当します。

"気持ち": 構造体を関数だけで表現する

さて、ここで天下り的な、少し突拍子もないことを書きます。初めて読む人は簡単には受け入れがたいかもしれないですが、最も重要な部分です。

上記で見てきたように、また、Rustなどでは実際そうであるように、構造体(判別共用体)をプログラムのすべての値の基礎に置くような試みも可能だと考えられるわけです。

ノート: クラスは？ポインタは？各種リテラル型は？

まず、各種リテラル型に関して（浮動小数点数など）ですが、まずbooleanは表現できるということでした。その他の float64 みたいなものも、究極ビット列、すなわち boolean を並べたものとして表現できてしまいます。(とても効率は悪いですが)

一方で、クラスや、特にポインタ、もしくは参照型などは、関数のように、本質的に言語にあらたな能力を与えてくれると考えることもできます。詳しくは TaPL などを参照していただければと思います。

プログラムのすべての値の基礎として判別共用体を置くことができそうです。次に、これを関数で代用できないか考えます。

さて、判別共用体は(Rustなどをみるとわかるように)それが使われる本質的な基礎の操作は match です。 match は判別子を見て、それに応じてプロパティに分解して、それらを利用した処理を継続できる、というものです。

ノート: たとえばbooleanはifが基礎なのではないか?

Rustでもifはmatchに書き換えられて、if letなんかもmatchの糖衣構文と考えることができます。

if flag {
  println!("true");
} else {
  println!("false");
}

match flag {
  true => println!("true"),
  false => println!("false"),
}

Rust Playground

さて、上記の考察を元に、更に飛躍させますが、 match とは「すべての判別子のパターンでの処理を、それぞれの判別子に対応するプロパティを引数とする関数」を受け取り、実際の構造体の判別子をもとにいずれかの関数を実行する。

つまり、「構造体」とは「すべての判別子のパターンでの処理を、それぞれの判別子に対応するプロパティを引数とする関数」を受け取り、そのいずれかの関数を引数を与えて実行する「関数」である、と捉える事ができます（！！）

「構造体(判別共用体)」を「関数」だと捉えるということです。

booleanを関数で

上記の考察をもとに、booleanを関数で定義してみましょう。まずJavaScriptで考えてみます。trueのときに実行してほしい関数と、falseのときに実行してほしい関数を受け取って、自分自身の値に応じてどちらかを実行する、ということなので、次のようになります。

const Bool_true = (when_true, when_false) => when_true();
const Bool_false = (when_true, when_false) => when_false();

ラムダ計算では

$$\mathit{true} = \lambda \textcolor{#6789dd}{t}. \lambda \textcolor{#dd6789}{f}. ~ \textcolor{#6789dd}{t} \\ \mathit{false} = \lambda \textcolor{#6789dd}{t}. \lambda \textcolor{#dd6789}{f}. ~ \textcolor{#dd6789}{f}$$

とよく定義されるものです。

対比してみて、対応付けられそうに感じられるかと思います。

これをまずはTypeScriptにしてみます。

type Bool = <T>(when_true: () => T, when_false: () => T) => T;

const Bool_true = <T>(when_true: () => T, when_false: () => T): T => when_true();
const Bool_false = <T>(when_true: () => T, when_false: () => T): T => when_false();

// それぞれがBool型であることを確認
{
  let _: Bool;
  _ = Bool_true;
  _ = Bool_false;
}

例えば、このブール値のフラグを受け取り、そのフラグがtrueのときだけHello!と表示するプログラムは以下のようになります。

const main = (shouldSayHello: Bool) => {
  shouldSayHello(
    // then節
    () => {
      console.log("Hello!");
    },
    // else節
    () => {
    }
  );
};

演算子 && 相当の定義は以下になります。すべて関数だけで定義されたプログラム...美しい。

const bool_and = (b1: Bool, b2: Bool): Bool => b1(
  () => b2(() => Bool_true, () => Bool_false),
  () => Bool_false,
);

TypeScript Playground

改めて、構造体版との比較をしてみましょう。

type Bool_D = {
  D: 'true';
} | {
  D: 'false';
};

type Bool_F = <T>(
  when_true: () => T,
  when_false: () => T,
) => T;

まだピンと来ていないかもしれないですが、残りの例も見ていって感覚を養っていきましょう。

ノート: 通常のチャーチエンコーディングと定義が少し異なることについて

通常の定義方法であれば、

const Bool_true = (when_true, when_false) => when_true;
const Bool_false = (when_true, when_false) => when_false;

のようになるべきかと思いますが、上記の定義はどうしても、「そのパターンで実行する」、という説明にするためには正格評価のJavaScriptとはどうしても相性が悪いため、わかりやすさのために、関数を受け取る、という形で（擬似的に遅延評価を再現して）表現することにしました。

直積型を関数で

ブール型はプロパティがなくて単純でした。次は、プロパティを２つ持つ直積型（ペア、２つ組）を定義してみましょう。

まず、構造体を作るときは { D: 'intro', v1, v2 } と書くように、 v1, v2 が必要になります。その後で、構造体が出来上がります。上記の説明の通り関数を作ると以下のようになります。

const Pair_intro = (v1, v2) => (when_intro) => when_intro(v1, v2);

これは、構造体を作る関数であり、 実際の構造体は (when_intro) => when_intro(v1, v2) の部分です。「その構造の中にある v1 と v2 を使いたい関数」を受け取って、適用してあげる、それが直積型の関数としての捉え方です。

ラムダ計算では

$$\mathit{pair} = \lambda \textcolor{#47cdcd}{a}. \lambda \textcolor{#cd47cd}{b}. \lambda \textcolor{#cc4444}{h}. ~ \textcolor{#cc4444}{h} ~ \textcolor{#47cdcd}{a} ~ \textcolor{#cd47cd}{b}$$

とよく定義されるものです。

直積型もTypeScriptで書いてみましょう。

type Pair<T1, T2> = <T>(
  when_intro: (
    v1: T1,
    v2: T2,
  ) => T,
) => T;

const Pair_intro = <T1, T2>(v1: T1, v2: T2) => <T>(when_intro: (v1: T1, v2: T2) => T): T => when_intro(v1, v2);

// Pair_intro(v1, v2) が Pair<T1, T2> の要素を作ることを確認
namespace _ {
  declare const t1: unique symbol;
  declare const t2: unique symbol;
  type T1 = typeof t1;
  type T2 = typeof t2;
  let _: Pair<T1, T2> = Pair_intro(t1, t2);
  void _;
}

例えば、２つある要素のそれぞれに射影する関数は以下のように定義できます。

const Pair_get1 = <T1, T2>(p: Pair<T1, T2>): T1 => p((v1, v2) => v1);
const Pair_get2 = <T1, T2>(p: Pair<T1, T2>): T2 => p((v1, v2) => v2);

TypeScript Playground

ラムダ計算では

ラムダ計算では get1 (first) と get2 (second) はチャーチブール $\mathit{true}$ と $\mathit{false}$ で代用されるのを見かけるかと思います。

実際、上記の Pair_get1 の定義内の (v1, v2) => v1 の部分は Bool_true の定義に（遅延評価を再現するために関数呼び出しをしている点を除いて）一致していると思います。

しかし、今回はあくまでも構造をベースとしてチャーチエンコーディングするというのが趣旨なので、ここに関してはあくまでも偶然であるとして特に触れずにいきます。

これはそれぞれ、 ([v1, v2]) => v1、 ([v1, v2]) => v2 のようなJSの関数に相当します。

もう一度、直積型に期待する関数としての振る舞いを復習します。直積型とは、「２つの引数を取る関数」を与えたら、その構造体が持っている２つの値を引数にいれて実行してくれる「関数」なのでした。
なので、構造体が持ってる値を取り出すには、この構造体に、「第一引数/第二引数を返す関数」を適用すればよいのです。

一瞬だけ number を使うことを許して、 ([v1, v2]) => v1 + v2 相当をする定義を考えてみましょう。このように2つの値を両方使いたい場合は、「受け取った引数をそのまま足す関数」を渡して上げればよいです。

const Pair_plus = (p: Pair<number, number>): number => p((v1, v2) => v1 + v2);

もちろん、さきほど定義した射影関数を利用しても良いですね。

const Pair_plus_ = (p: Pair<number, number>): number => Pair_get1(p) + Pair_get2(p)

おわりに、今回も二種類の定義を並べてみます。

type Pair_D<T1, T2> = {
  D: 'intro';
  v1: T1;
  v2: T2;
};

type Pair_F<T1, T2> = <T>(
  when_intro: (
    v1: T1,
    v2: T2,
  ) => T,
) => T;

構造体の関数型への翻訳方法が見えてきましたでしょうか...？次の例に行ってみましょう。

直和型を関数で

つづいて直和型 Either を関数型として定義してみます。

type Either<Left, Right> = <T>(
  when_intro_left: (
    left: Left,
  ) => T,
  when_intro_right: (
    right: Right,
  ) => T,
) => T;

const Either_intro_left = <Left, Right>(left: Left) => <T>(when_intro_left: (left: Left) => T, when_intro_right: (right: Right) => T): T => when_intro_left(left);
const Either_intro_right = <Left, Right>(right: Right) => <T>(when_intro_left: (left: Left) => T, when_intro_right: (right: Right) => T): T => when_intro_right(right);

// Either_intro_{left, right}<Left, Right>(v) が Either<Left, Right> の要素を作ることを確認
namespace _ {
  declare const t1: unique symbol;
  declare const t2: unique symbol;
  type T1 = typeof t1;
  type T2 = typeof t2;
  let _: Either<T1, T2>;
  _ = Either_intro_left(t1);
  _ = Either_intro_right(t2);

  // @ts-expect-error -- LeftとしてT2を入れることはできない
  _ = Either_intro_left(t2);
}

TypeScript Playground

たとえば、 string と number を一時的に解禁して、どちらかを受け取り、 string ならそのまま、 number なら toFixed(2) を呼び出して返す関数は次のように定義できます。

// numberかstringを受け取って文字列として返す
const format = (v: Either<number, string>): string => v(
  // number の場合
  (left) => left.toFixed(2),
  // string の場合
  (right) => right,
);

今回も構造体版との比較をします。

type Either_D<Left, Right> = {
  D: 'intro_left';
  left: Left;
} | {
  D: 'intro_right';
  right: Right;
};

type Either_F<Left, Right> = <T>(
  when_intro_left: (
    v: Left,
  ) => T,
  when_intro_right: (
    v: Right,
  ) => T,
) => T;

どうでしょう...？構造体の定義を関数型に機械的に変換できそう...な感覚が掴めてきましたでしょうか。

再帰型: 自然数

さて、ここでいきなりですが、慣れてないと見かけない定義かもしれませんが、自然数 $0, 1, 2, \cdots$ を構造体で表現することも可能です。型自体の自己参照を一時的に解禁します。

type Nat = {
  D: 'zero';
} | {
  D: 'succ';
  n: Nat;
};

循環参照を禁止しているので、この定義に当てはまる値は { D: 'zero' }, { D: 'succ', n: { D: 'zero' } } などがあります。

const Z: Nat = { D: 'zero' };
const S: (_: Nat) => Nat = (n: Nat) => { D: 'succ', n };

という定義を考えて、 $0, 1, 2, \cdots$ を Z, S(Z), S(S(Z)), ... と対応付けていきます。

$100$ だったら S を百回重ねることになります。

再帰的な自然数を関数で (Scott encoding)

さて、さきほど紹介した自然数型を作ってみます。この型は自分自身への参照がある型になります。

type Nat = <T>(
  when_zero: () => T,
  when_succ: (
    np: Nat,
  ) => T,
) => T;

const Nat_zero = <T>(when_zero: () => T, when_succ: (np: Nat) => T): T => when_zero();
const Nat_succ = (np: Nat) => <T>(when_zero: () => T, when_succ: (np: Nat) => T): T => when_succ(np);

// Nat_{zero, succ} が Nat の要素を作ることを確認
namespace _ {
  let _: Nat;
  _ = Nat_zero;
  _ = Nat_succ(Nat_zero);
  _ = Nat_succ(Nat_succ(Nat_zero));
}

TypeScript Playground

なお、自己参照的な構造体は禁止してることに注意してください。 function omega<T>(when_zero: () => T, when_succ: (n: Nat) => T): T { return when_succ(omega); } のような関数を指して Nat の値とは呼ばないということです。

上記のもとで、 Nat は $0, 1, 2, \cdots$ に対応する。 つまり、 Nat_zero, Nat_succ(Nat_zero), Nat_succ(Nat_succ(Nat_zero)) のように Nat_succ を $n$ 回 Nat_zero に適用した値が自然数 $n$ に対応します。

たとえば、ゼロかどうかを判定する関数を考えてみましょう。

const isZero = (n: Nat): Bool => n(
  // 0 のとき
  () => Bool_true,
  // np+1 のとき
  (_np) => Bool_false,
);

これは、先程のBoolを利用すれば、すべて関数でできています。

他にも一個前の自然数を返す前者関数を作ってみましょう。（ただっし $0$ の前者は $0$ を返すとします）

const pred = (n: Nat): Nat => n(
  // 0 のとき
  () => Nat_zero,
  // np+1 のとき
  (np) => np,
);

なお、足し算をする場合には再帰呼び出しが必要になってしまいます。禁止されている再帰呼び出しを使うと、以下のように書くことはできます。

const add = (n: Nat, m: Nat): Nat => n(
  // 0 のとき
  () => m,
  // np+1 のとき (addを再帰的に呼び出している)
  (np) => Nat_succ(add(np, m)),
);

ラムダ計算では

今回のエンコーディングはScott Encodingと呼ばれるものです。通常のチャーチによるエンコーディングとは異なることに注意してください。

$$s_0 = \lambda z. \lambda s. ~ z \\ s_1 = \lambda z. \lambda s. ~ s ~ s_0 \\ s_2 = \lambda z. \lambda s. ~ s ~ s_1 \\ \mathit{succ}_s = \lambda n. \lambda z. \lambda s. ~ s ~ n \\ \mathit{pred}_s = \lambda n. ~ n ~ (\lambda z. \lambda s. ~ z) ~ (\lambda p. ~ p)$$

となります

type Nat_D = {
  D: 'zero';
} | {
  D: 'succ';
  n: Nat_D;
};

type Nat_Scott = <T>(
  when_zero: () => T,
  when_succ: (
    np: Nat_Scott,
  ) => T,
) => T;

再帰型から帰納型へ

さて、また飛躍したことを書きますが、自然数型の捉え方をまた変えてみましょう。一般の自分自身を参照する判別共用体を考えます。(とはいえ一般化すると難しいので、自然数型だけ考えておいても問題ありません)

判別共用体(構造体)とは、関数として見立てると、「それぞれのパターンに応じた関数」を受け取って、そのパラメータを渡して実行してあげるのでした。

自分自身を参照する場合も、再帰型では、これは変わりませんでした。

しかし、ここで自分自身を参照するパターンに入る場合、その構造体に関数的に期待することを、パラメータに渡る「自分の型に属する値」を、最初に渡した「それぞれのパターンに応じた関数」を渡した結果、としてみます。

かなり「何を言っているんだ」、という感じかもしれませんが、要は、「自己参照をする判別共用体」を、 "ループをする" 関数、もしくは "再帰呼び出しをする" 関数と捉えるということです。

とりあえず、さっそく定義してみましょう。変更点は一箇所のみです。

type Nat = <T>(
  when_zero: () => T,
  when_succ: (
-    np: Nat,
+    v_np: T,
  ) => T,
) => T;

上記のように変えて...

帰納的な自然数を関数で (Church encoding)

type Nat = <T>(
  when_zero: () => T,
  when_succ: (
    v_np: T,
  ) => T,
) => T;

const Nat_zero = <T>(when_zero: () => T, when_succ: (v_np: T) => T): T => when_zero();
const Nat_succ = (np: Nat) => <T>(when_zero: () => T, when_succ: (v_np: T) => T): T => when_succ(np(when_zero, when_succ));

TypeScript Playground

さっそく、使い方の例を見ていきます。着目すべきは、Scott Encodingでは再帰呼び出しが必要だった add の定義が、再帰呼び出し無しで実現しているという点にあります。

まずは isZero です。これはあまり変わりませんね。

const isZero = (n: Nat): Bool => n(
  // 0 のとき
  () => Bool_true,
  // np+1 のとき
  (_v_np) => Bool_false,
);

pred はちょっと飛ばして、 add の定義が次のようになります。

const add = (n: Nat, m: Nat): Nat => n(
  // 0 のとき
  () => m,
  // np+1 のとき: v_np = add(np) として
  (v_np) => Nat_succ(v_np),
);

とても簡単になりましたね... n 上で再帰呼び出し(帰納法)をしていると捉えてください。
n === 0 のときは n + m は m ですね。
n === np + 1 のときは n + m は　S(np + m) ですね。

あえて通常の書き方をすれば、以下のようになります。

const add = (n: number, m: number): number => {
  if (n === 0) {
    return m;
  } else {
    const np = n-1;
    const v_np = add(np, m);
    return (v_np)+1;
  }
};

簡易的には、例えば以下のような順序で足し算が求まることになります。

add(n2, n3)
= Nat_succ(add(n1, n3))
= Nat_succ(Nat_succ(add(n0, n3)))
= Nat_succ(Nat_succ(n3))
= Nat_succ(n4)
= n5

他の例でも試していくことでこの定義が掴めてくるかもしれません。

最後に pred です。ちょっとだけ面倒にはなってしまいます。まず、 pred_ という補助関数を定義します。これは直積型 Pair<Bool, Nat> を返しますが、 zero のときだけ第一引数が Bool_false になります。

const pred_ = (n: Nat): Pair<Bool, Nat> => n(
  // 0 のとき
  () => Pair_intro(Bool_false, Nat_zero),
  // np+1 のとき: v_np = pred_(np) として
  (v_np) => Pair_intro(
    Bool_true,
    Pair_get1(v_np)(
      // pred_(np).1 が true のとき
      () => Nat_succ(Pair_get2(v_np)),
      // pred_(np).1 が false のとき
      () => Nat_zero,
    ),
  ),
);
const pred = (n: Nat): Nat => Pair_get2(pred_(n));

どうしても帰納の文脈に載せなければならないので、 pred は初期値付近で複雑になりがちです。ただ、 Pair<Bool, Nat> は Nat | null みたいなもの（もしくは Option<Nat>）と捉えると良いかと思います。
Option も当然、判別共用体として定義できるので、練習として定義してみるのも面白いかもしれません。

もしくは、 Pair_intro(false, 0) は $-1$ の代わりと捉えてもいいかもしれません。

あえて通常のリテラル型で書くならば、以下の定義に相当します。

const pred_ = (n: number): [boolean, number] => {
  if (n === 0) {
    return [false, 0];
  } else {
    const np = n-1;
    const v_np = pred_(np, m);
    return [true, v_np[0] ? (v_np[1])+1 : 0];
  }
};
const pred = (n: number): number => pred_(n)[1];

ラムダ計算では

$$c_0 = \lambda z. \lambda s. ~ z \\ c_1 = \lambda z. \lambda s. ~ s ~ (s ~ z) \\ c_2 = \lambda z. \lambda s. ~ s ~ (s ~ (s ~ z)) \\ \mathit{succ}_c = \lambda n. \lambda z. \lambda s. ~ s ~ (n ~ z ~ s) \\$$

駆け足になりましたが、最後に同様に比較をしてみます。

type Nat_D = {
  D: 'zero';
} | {
  D: 'succ';
  n: Nat_D;
};

type Nat_Church = <T>(
  when_zero: () => T,
  when_succ: (
    np: T,
  ) => T,
) => T;

Nat_Church は自己参照を利用せずに定義できている点に着目してください
(なお、Scott Encodingも自己参照を用いずに近い型定義をすることは可能です)

帰納的なリストを関数で

申し訳ないことにここでは省略しますが、リストも当然表現できます。別記事にするかもです。

まとめ

TypeScriptの関数への限定をして、構造体を関数だとみなして表現する方法、そして帰納的な構造体をも、ループ処理をする関数だとみなして関数で表現できました。

ループ処理をする関数だとみなす表現方法がチャーチエンコーディングに相当します。関数だけでここまでの表現力があるとは本当に面白いことだと思います。

関数がすべての基礎なのではないだろうか...そんなことを思わせる非常に面白いエンコーディングですね。

そしてそれを体現するかのような基礎的な体系がラムダ計算です。ラムダ計算はほんの少しのルール、関数に関する記述能力だけを持ちながら、その計算能力はチューリング完全になります。

今回の記事で関数の表現力が伝わっていたら嬉しく思います。今回始めてラムダ計算という言葉を聞いた方も、ひょっとすれば、ラムダ計算(関数だけの計算体系)がチューリング完全だと思えるきっかけになったりすればいいな...とおもいます。

感想

締め切りギリギリまで書いていたこともあり(というかギリギリまで内容があまり決まっておらず)だいぶ駆け足にはなってしまいましたが、自分も急いで書きながら自分の中の考え方を整理したり、Church Encoding / Scott Encoding に関する知識を整理できてよかったかなと思います。

あまり推敲もできないままで破綻している箇所もあるかもしれないので、継続的に修正していこうと思います。また、なにか問題等を見つけましたら、コメントかTwitter(新X)の方で教えていただければ幸いです。

次回予告

なんかまたラムダ計算×TypeScript(JavaScript)でやりたいです