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

ラムダ計算

ラムダ計算で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」以降)

Boolの代わりにEither () ()を使って，論理演算をポイントフリースタイルで定義

カリーハワード対応
Bool Either () ()
true Left
false Right

この記事では，上記の対応付けを使って，ポイントフリースタイルで論理演算を定義します。

否定 not の定義

a not a
true false
false true


notを定義するには，ArrowChoiceの(|||)を使います。

not :: Either () () -> Either () ()
not = false ||| true

true = Left, false = Rightであることに注意してください。


論理和 or を定義する準備

a b or a b
true true true
true false true
false true true
false false false


orの型は，以下のようになります。

or :: (Either () (), Either () ()) -> Either () ()

この記事では，複数個の引数は，タプルの形で与えます。カリー化はしません。



orを定義するために，補助関数distrを定義しておきます。distrは，orの第1引数を場合分けするために使います。

distr :: (Either a b, c) -> Either (a, c) (b, c)
distr = uncurry (curry Left ||| curry Right)
型の表記を変更する

型を読みやすくするために，型の表記を変更します。


distr :: (Either a b, c) -> Either (a, c) (b, c)

↓

distr :: (a + b) * c -> a * c + b * c
or :: (Either () (), Either () ()) -> Either () ()

↓

or :: )(() + ())( * )(() + ())( -> () + ()


orの型が「()」だらけで，まだ読みにくいので，さらに表記を変更します。

or :: )(() + ())( * )(() + ())( -> () + ()

↓

or :: (T + F) * (T + F) -> T + F
Tはtrueに対応する型です。true = Leftなので，左側がTとなります。


orの定義

distrを使えば，orは以下のように定義できます。*1

or :: (T + F) * (T + F) -> T + F
or = distr >>> ((fst >>> true) ||| snd)


このときのdistrの役割は，こんな感じです。



おまけ：直積と直和の分配法則

distrには逆関数が存在します。

undistr :: a * c + b * c -> (a + b) * c
undistr = ((fst >>> Left) ||| (fst >>> Right)) &&& (snd ||| snd)


distrとundistrによって，直積と直和には分配法則が成り立つことがわかります。

(a + b) * c = a * c + b * c

*1:このorは短絡評価できます

curry,(&&&),(|||)の型が，指数法則と対応している

カリーハワード対応

3つの指数法則

  1. c^{\left(a\times b\right)} = \left(c^b\right)^a
  2. b^a\times c^a = \left(b\times c\right)^a
  3. c^a\times c^b = c^{\left(a+b\right)}

指数法則を数式から型に書き換える

数式 型
a^b b -> a
a+b Either a b
a\times b (a, b)

この表の通りに指数法則を書き換えると，こうなります。

  1. (a, b) -> c = a -> (b -> c)
  2. (a -> b, a -> c) = a -> (b, c)
  3. (a -> c, b -> c) = (Either a b -> c)

これらは，curry,(&&&),(|||)の型とよく似ています。

関数型
curry(a, b) -> c -> (a -> b -> c)
(&&&)(a -> b) -> (a -> c) -> (a -> (b, c))
(|||)(a -> c) -> (b -> c) -> (Either a b -> c)

フィボナッチ数列は相互再帰だという話

プログラム合成・変換

この記事では，Haskellの記法を使います。


自然数は以下のように定義しておきます。

data Nat = Zero | Succ Nat

フィボナッチ数列を計算する関数　典型的な定義

fib Zero            = Zero
fib (Succ Zero)     = Succ Zero
fib (Succ (Succ n)) = fib n  +  fib (Succ n)


2段階目の場合分け部分を関数としてくくり出す

fib (S n'')の引数(S n'')は必ず1以上になるので，1段階目で無駄な場合分けが発生します。



1段階目の場合分けをパスして，2段階目の場合分けにジャンプするために，2段階目の場合分け部分を関数としてくくり出します。

fib Zero = Zero
fib (Succ n) = fibS n

fibS Zero = Succ Z
fibS (Succ n) = fib n + fibS n

2段階目の場合分け部分を，fibSという関数にしました。
fibとfibSは相互再帰関数です。


fibとfibSの関数呼び出し関係を図にすると，こんな感じです。


セプキャン2011 プログラミング言語クラスの感想

セキュリティ&プログラミングキャンプ2011にプログラミング言語クラス参加者として参加しました。


私の応募用紙は以下の記事で公開しています。
セプキャン2011 応募用紙 - Meta reifier


5日間の日程表(pdf)
プログラミングコース時間割
なかなかハードですね。

前半

第3日目の昼までは，プログラミング言語クラス全体で1つの講義を受講します。講義内容は日程表の通りです。
Rubyが目立ちますが，Rubyプログラムのソースコードを読み書きすることは，ほとんどありませんでした。C言語で書かれたRuby処理系のソースコードを読み書きすることが多いです。

後半

第3日目の昼から始まる「個別課題」以降は雰囲気が大きく変わります。

個別課題のタイトル
  1. 文法ハック
  2. 可視化・可聴化
  3. preludeをprecompileしよう
  4. 自作のプログラミング言語を作ろう
  5. 拡張ライブラリ作成による高速化
  6. 面白い拡張ライブラリ
  7. LambdaPi
  8. Rubyに末尾再帰の最適化の実装
  9. プロファイラの機能追加
  10. セキュリティコース CTF(Capture The Flag)への参戦


これら10種類のテーマから第3希望までの希望調査を取り，1つのテーマを遂行します。テーマごとに担当講師がいます。1人の講師が複数のテーマを兼任することもあります。


私は初め，シンプルな項書き換え系の処理系でも作ろうかと考えていましたが，様々な出来事があり，最終的に@kinabaさんのもとでシャミノ計算を発表することになりました。(柔軟な対応をしてくださった@takesakoさん達に感謝します)


シャミノ計算というのは，私がセプキャン以前(2011年6月頃)に考えていた計算モデルです。
ラムダ計算を，項書き換え系として，より形式的に表現することを目指しています。
シャミノ計算 - Meta reifier


個別課題への着手が遅れたことと，シャミノ計算の仕様がまだ曖昧であったことから，処理系を作るには至らず，プレゼン内容を考えて資料を作るだけで時間切れとなってしまいました。

今後

私が興味深いと思った概念を，他人に伝えまくるだけでもそれなりに社会貢献できることを初めて実感できたので，自信を持ってアウトプットしていけそうです。
シャミノ計算以外にもいくつか持ちネタがあるので，「またお前か」と言われるようにアウトプットしていくつもりです。