ラムダ計算での代数的データのエンコード的な話

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 (* = x *)
let _ = one  x f (* = f x *)
let _ = two  x f (* = f (f x) *)

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 (* = foo *)
let _ = one  foo bar (* = bar Z *)
let _ = two  foo bar (* = bar (S Z) *)

また, 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)         (* n = Z の場合 *)
    (fun n' -> print nothing) (* n = S n' の場合 *)

当然これでは駄目で, call-by-value の場合は引数を評価してから関数適用するので print something が常に評価され, something の値が出力されてしまう.

というわけで例えば以下のように書く必要がある.

let _ = n
    (fun _    -> print something) (* n = Z の場合 *)
    (fun n' _ -> print nothing)   (* n = S n' の場合 *)
    n

では n が変数ではなく, 何かの計算を行った結果の値を使ってパターンマッチをする場合はどうだろうか.

let _ = (f x)
    (fun n    -> print something) (* f x = n = Z の場合 *)
    (fun n' n -> print nothing)   (* f x = n = S n' の場合 *)
    (f x)

これもやはり駄目で, f x が (副作用があるかもしれないのに) 2 回評価されてしまう.

そこで次のような関数 match を定義する.

let match n f g = n f g n

これを使えば以下のように書けて便利.

let _ = match (f x)
    (fun n    -> print something) (* f x = n = Z の場合 *)
    (fun n' n -> print nothing)   (* f x = n = S n' の場合 *)

ペアノ数以外の場合

ペアノ数以外のデータについてはどうなるのかを考えるために, 仮に以下のような 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)  (* f x = y = A の場合 *)
    (fun y -> print nothing)    (* f x = y = B の場合 *)
    (fun y -> print everything) (* f x = y = C の場合 *)

もうお気づきのとおり, この方法で同じようにパターンマッチを書こうと思うと, 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) (* f x = Z の場合 *)
    (fun S n' -> print nothing)   (* f x = S n' の場合 *)

となり, ふつうの言語におけるパターンマッチと見た目が近くなる. また, 上で定義した match のような関数をわざわざ使う必要がなくなる. 個人的には match = id = fun x -> x と定義しておいて,

let _ = match (f x)
    (fun Z    -> print something) (* f x = Z の場合 *)
    (fun S n' -> print nothing)   (* f x = S n' の場合 *)

と書くのが何をしているのかわかりやすくて好み.

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)  (* f x = A の場合 *)
    (fun B -> print nothing)    (* f x = B の場合 *)
    (fun C -> print everything) (* f x = C の場合 *)

ここでも 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) (* f x = n = Z の場合 *)
    (fun n n' -> print nothing)   (* f x = n = S n' の場合 *)

ここでも match = id である. また, 変数 nf 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)  (* f x = y = A の場合 *)
    (fun y -> print nothing)    (* f x = y = B の場合 *)
    (fun y -> print everything) (* f x = y = C の場合 *)

やはり match = id で, コンストラクタの数によって変える必要はない.

まとめ

  • 関数を用いた代数的データの表現方法として主に Church encoding と Scott encoding がある
  • Scott encoding を少し変更することで, 副作用がある場合のパターンマッチを綺麗に書くことができる

というのがここ最近の思いつきです.

*1:正確には「今定義しているデータ型の」引数がある場合