Grass で遊んでたらラムダ計算熱が復活してきたので.
以下は特に断りのない限り call-by-value の型無しラムダ計算です (謎の ML 風文法で書いてあるけど, まあわかると思うので適当に読んで下さい).
Church encoding と Scott encoding
関数 (ラムダ抽象) のみを用いて代数的データを表現 (encode) する方法としてよく知られたものとして,
Church encoding と Scott encoding という 2 つの方法がある.
ここでは例としてペアノ数を表現してみる.
Haskell で書くならこんな感じのやつ.
data Number = Z | S Number
Church encoding
Church encoding ではこれを以下のように表現する.
let Z = fun z s -> z
let S n = fun z s -> s (n z s)
これの利点は, fold あるいは catamorphism と呼ばれる操作を行う関数そのものになっていること.
let zero = Z
let one = S Z
let two = S (S Z)
let _ = zero x f
let _ = one x f
let _ = two x f
Scott encoding
一方, Scott encoding では以下のように表現する.
コンストラクタに引数が無い場合は Church encoding と同じだが, 引数がある場合*1が異なる.
let Z = fun z s -> z
let S n = fun z s -> s n
こちらはパターンマッチが簡単に行える.
let zero = Z
let one = S Z
let two = S (S Z)
let _ = zero foo bar
let _ = one foo bar
let _ = two foo bar
また, fold は次のように書ける.
let fold = fix (fun fold n x f ->
n x (fun n' -> fold n' (f x) f)
)
fix は不動点関数で fix f = f (fix f) となり, 再帰関数を定義するために使うことができる.
let rec f = ... が let f = fix (fun f -> ...) と書けると思えば良い.
let fix f = (fun x -> f (fun y -> x x y)) (fun x -> f (fun y -> x x y))
Scott encoding の方がなにかと扱いやすいことが多いので個人的にはよく使う.
非純粋な場合の問題点
さて, 純粋な計算の場合はこれで十分なのだが, 非純粋で副作用がある場合にはちょっと厄介になる.
副作用がある関数の扱い
例えば何かを出力する関数 print があったとして, Scott encode されたペアノ数が 0 (Z) かどうかによって出力する内容を変える処理を以下のように書いたとする.
let _ = n
(print something)
(fun n' -> print nothing)
当然これでは駄目で, call-by-value の場合は引数を評価してから関数適用するので print something が常に評価され,
something の値が出力されてしまう.
というわけで例えば以下のように書く必要がある.
let _ = n
(fun _ -> print something)
(fun n' _ -> print nothing)
n
では n が変数ではなく, 何かの計算を行った結果の値を使ってパターンマッチをする場合はどうだろうか.
let _ = (f x)
(fun n -> print something)
(fun n' n -> print nothing)
(f x)
これは f x の計算結果そのものを使いたいこともあると仮定して f x を引数として渡しているが, これでは駄目で, f x が (副作用があるかもしれないのに) 2 回評価されてしまう.
そこで次のような関数 match を定義する.
let match n f g = n f g n
これを使えば以下のように書けて便利.
let _ = match (f x)
(fun n -> print something)
(fun n' n -> print nothing)
ペアノ数以外の場合
ペアノ数以外のデータについてはどうなるのかを考えるために,
仮に以下のような 3 つのコンストラクタを持つデータを考える.
let A = fun a b c -> a
let B = fun a b c -> b
let C = fun a b c -> c
これについても同じようにパターンマッチを書くと以下のようになる.
let match3 x f g h = x f g h x
let _ = match3 (f x)
(fun y -> print something)
(fun y -> print nothing)
(fun y -> print everything)
もうお気づきのとおり, この方法で同じようにパターンマッチを書こうと思うと,
match1, match2, match3, ... のようにコンストラクタの数によって別々に関数 match を定義しなくてはならない.
解決法
これを解決するには, 元のデータの encoding を少し変更してやれば良い.
見た目重視
まずはペアノ数の場合は次のようにする.
let Z = fix (fun Z z s -> z Z)
let S = fix (fun S n z s -> s S n)
fix は上で挙げた不動点関数で, データを再帰関数として定義して,
引数として受け取った関数にコンストラクタ自身を必ず渡すようにしている.
これを使ってパターンマッチを書くと,
let _ = (f x)
(fun Z -> print something)
(fun S n' -> print nothing)
となり, ふつうの言語におけるパターンマッチと見た目が近くなる.
また, 上で定義した match のような関数をわざわざ使う必要がなくなる.
個人的には match = id = fun x -> x と定義しておいて,
let _ = match (f x)
(fun Z -> print something)
(fun S n' -> print nothing)
と書くのが何をしているのかわかりやすくて好み.
A, B, C の 3 つのコンストラクタを持つ場合も同じように書ける.
let A = fix (fun A a b c -> a A)
let B = fix (fun B a b c -> b B)
let C = fix (fun C a b c -> c C)
let _ = match (f x)
(fun A -> print something)
(fun B -> print nothing)
(fun C -> print everything)
ここでも match = id で, コンストラクタの数によって別の関数を定義する必要はない.
実用重視
実用重視のものとして, パターンマッチにおける所謂 as パターンを予め組み込んでしまう方法がある.
まずはペアノ数の場合は次のようにする.
let Z = fix (fun X z s -> z X)
let S n = fix (fun X z s -> s X n)
上では引数として受け取った関数にコンストラクタを渡していたが,
今度はデータそのものを渡すようにしている.
これを使ってパターンマッチを書くと,
let _ = match (f x)
(fun n -> print something)
(fun n n' -> print nothing)
ここでも match = id である.
また, 変数 n は f x の値に束縛されるので, これを用いると値を再利用することができる.
A, B, C の場合も同様にして以下のように書ける.
let A = fix (fun X a b c -> a X)
let B = fix (fun X a b c -> b X)
let C = fix (fun X a b c -> c X)
let _ = match (f x)
(fun y -> print something)
(fun y -> print nothing)
(fun y -> print everything)
やはり match = id で, コンストラクタの数によって変える必要はない.
まとめ
- 関数を用いた代数的データの表現方法として主に Church encoding と Scott encoding がある
- Scott encoding を少し変更することで, 副作用がある場合のパターンマッチを綺麗に書くことができる
というのがここ最近の思いつきです.
