ラムダ計算で代数的データ型を表現する方法

ラムダ計算でEither

Either型の値をパターンマッチする状況を考えます。
「データコンストラクタのパターンマッチ」は，下図のようにしてラムダ計算で表現できます。

ラムダ計算でBool

今度は，Bool型の値をパターンマッチする状況を考えます。

TrueやFalseには引数が無いので，(3)や(4)はλで囲みません。

パターンマッチ = 「データコンストラクタを他の関数に置き換えること」

パターンマッチによって，Leftがlに置き換わります。以下同様です。

「データコンストラクタを置き換える」という概念について，もう少し詳しく考えていきます。

データコンストラクタの置き換え方は2種類ある

リストのような再帰的なデータ型では，データコンストラクタの置き換え方が2種類あります。

data List a = Cons a (List a) | Nil

(1) 全てのデータコンストラクタを置換する

(2) 最初のデータコンストラクタを置換する

それぞれの置き換え方をラムダ計算で表現すると，以下のようになります。

(1) 全てのデータコンストラクタを置換する

(2) 最初のデータコンストラクタを置換する

ラムダ計算で再帰的なデータ型を表現する2種類の方法には，それぞれ名前がついています。
「(1) 全てのデータコンストラクタを置換する」はチャーチエンコーディング(Church encoding)と呼ばれます。
「(2) 最初のデータコンストラクタを置換する」はスコットエンコーディング(Scott encoding)と呼ばれます。

チャーチエンコーディングで表現されたリスト

[]      = λc n. n
[1]     = λc n. c 1 n
[1,2]   = λc n. c 1 (c 2 n)
[1,2,3] = λc n. c 1 (c 2 (c 3 n))

スコットエンコーディングで表現されたリスト

[]      = λc n. n
[1]     = λc n. c 1 (λc n. n)
[1,2]   = λc n. c 1 (λc n. c 2 (λc n. n))
[1,2,3] = λc n. c 1 (λc n. c 2 (λc n. c 3 (λc n. n)))

チャーチエンコーディングの特徴

チャーチエンコーディングによってリストを表現すると，リストの値そのものにfoldrの機能が内蔵されます。

チャーチエンコーディングでのfoldrの定義

foldr n c l = l c n

上記のfoldrの定義には不動点コンビネータなどが使われていません。型付け可能です。

スコットエンコーディングの特徴

スコットエンコーディングによってリストを表現すると，リストの値そのものにパターンマッチの機能が内蔵されます。

スコットエンコーディングでのtailの定義

tail l = l (λx xs. xs) Nil

ラムダ計算で自然数

自然数も代数的データ型で定義できます。

data Nat = Succ Nat | Zero

チャーチエンコーディングで表現された自然数(チャーチ数)

0 = λs z. z
1 = λs z. s (s z)
2 = λs z. s (s (s z))
3 = λs z. s (s (s (s z)))

スコットエンコーディングで表現された自然数

0 = λs z. z
1 = λs z. s (λs z. z)
2 = λs z. s (λs z. s (λs z. z))
3 = λs z. s (λs z. s (λs z. s (λs z. z)))

Either

Either型は再帰的な構造を持たないので，チャーチエンコーディングでもスコットエンコーディングでもデータコンストラクタの定義は同じになります。

Bool

チャーチエンコーディングの型

チャーチエンコーディングによって代数的データ型をラムダ計算で表現すると，以下のような型が現れます。

チャーチエンコーディングで現れた型は，型コンストラクタやデータコンストラクタの"名前"の情報を持っていません。これらの型が持っている情報は，データ型の構造的な特徴のみです。

参考文献

Bernie's notes on the Scott encoding
Directly Reflective Meta-Programming (9ページ目の「5.1 The Church Encoding」以降)