Hatena::ブログ(Diary)

@syamino はてなダイアリー RSSフィード Twitter

2012/05/24

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

ラムダ計算でEither

Either型の値をパターンマッチする状況を考えます。

「データコンストラクタのパターンマッチ」は,下図のようにしてラムダ計算で表現できます。


f:id:syamino:20120524201205p:image




ラムダ計算でBool

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


f:id:syamino:20120524201854p:image


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




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

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



f:id:syamino:20120525055329p:image



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




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

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

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

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

f:id:syamino:20120524202328p:image



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

f:id:syamino:20120524202329p:image



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



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


f:id:syamino:20120524210246p:image



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


f:id:syamino:20120524210247p:image



ラムダ計算で再帰的なデータ型を表現する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)))

f:id:syamino:20120524232855p:image



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

チャーチエンコーディングによってリストを表現すると,リストの値そのものに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)))

f:id:syamino:20120524225809p:image





Either

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


f:id:syamino:20120524223219p:image




Bool


f:id:syamino:20120524223220p:image





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

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


f:id:syamino:20120524225810p:image


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





参考文献

Bernie’s notes on the Scott encoding

Directly Reflective Meta-Programming (9ページ目の「5.1 The Church Encoding」以降)

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証