型レベルFizzBuzz（及び、type familyにおけるガードの書き方）
型レベルFizzBuzzどっかで見た気がするが、今書けるかというと絶対無理
— xenophobia (@xenophobia__) 2014, 5月 2
↑みたいなこと呟いたら「そんな難しいか？」という意見が見受けられ、言われてみれば確かにそんな言うほど難しくないのでは、と思い書いてみました。最近Haskell書いていない気がするし。*1
なんですが、そもそも"型レベルFizzBuzz"って何でしょうか。初めに想像したのは
(N1, N2, ...は型レベル自然数として)
*Main> :t Proxy :: Proxy (XFizzBuzz N1)
Proxy :: Proxy (XFizzBuzz N1) :: Proxy ('Number ('S Zero))
*Main> :t Proxy :: Proxy (XFizzBuzz N3)
Proxy :: Proxy (XFizzBuzz N3) :: Proxy 'Fizz
*Main> :t Proxy :: Proxy (XFizzBuzz N5)
Proxy :: Proxy (XFizzBuzz N5) :: Proxy 'Buzz
*Main> :t Proxy :: Proxy (XFizzBuzz N15)
Proxy :: Proxy (XFizzBuzz N15) :: Proxy 'FizzBuzz
*Main> :t Proxy :: Proxy (XFizzBuzz N20)
Proxy :: Proxy (XFizzBuzz N20) :: Proxy 'Buzz
のような挙動をする何かなので、そういうものを作ってみました。
type familyで型から型への関数を書けばいいので、めっちゃ愚直にまずこんなコードを書きました。
FizzBuzzの列が基本的には15周期の列なので*2、15以上の数が来たら再帰、というコードです。いくらなんでもな気がしますが一応
*Main> main "1" "2" "Fizz" "4" "Buzz" "Fizz" "7" "8" "Fizz" "Buzz" "11" "Fizz" "13" "14" "FizzBuzz" "16" "17" "Fizz" "19" "Buzz"
という感じでちゃんと動いてくれます。もちろんREPLで次のような挙動を確認することもできます。
*Main> :t Proxy :: Proxy (XFizzBuzz N1)
Proxy :: Proxy (XFizzBuzz N1) :: Proxy FB ('Number ('S Zero))
*Main> :t Proxy :: Proxy (XFizzBuzz N3)
Proxy :: Proxy (XFizzBuzz N3) :: Proxy FB 'Fizz
*Main> :t Proxy :: Proxy (XFizzBuzz N5)
Proxy :: Proxy (XFizzBuzz N5) :: Proxy FB 'Buzz
*Main> :t Proxy :: Proxy (XFizzBuzz N15)
Proxy :: Proxy (XFizzBuzz N15) :: Proxy FB 'FizzBuzz
*Main> :t Proxy :: Proxy (XFizzBuzz N20)
Proxy :: Proxy (XFizzBuzz N20) :: Proxy FB 'Buzz
で、とりあえず一応できたんですが、やっぱり普通に3で割れたらhogehoge、5で割れたらhugahuga的なコードを書きたい欲が出てきます。
なんで最初からそうしなかったかというと、type familyの場合分けで「nを3で割った余りが0なら……」というガードを書く方法がわかりませんでした。
先駆者を調べると次のような記事がありました。
つまり
type family F x :: *
type family F x = F' x (x :>>= N0)
type family F' x (guard :: Bool) :: *
type instance F' x True = ...
type instance F' x False = ...
のように書けばガードっぽいことができるということです。
最終的に次のようなコードができました。いいんじゃないでしょうか。
githubリポジトリです。: xenophobia/TypeLevelFizzBuzz · GitHub
以下蛇足。
書いていて初めてProxyの意義を理解しました。カインドが*でない型は対応する値が存在しないので、代わりに引数にProxy (n :: Nat)型みたいな値を渡せばいける、ということなんですね。
あと、これは最初のバージョン書いていたときに気づいたんですが、DataKindsで型に昇格させた値のデータコンストラクタってシングルクォートを"付けなきゃいけなかった"記憶がある*3んですが、いつの間に不要になったんですかね？
OchaCamlに触ってみた。
PPL2014（ http://www.fos.kuis.kyoto-u.ac.jp/ppl2014/ ）に参加して来ました。
去年に引続きの参加（但し去年は発表なしで見に行っただけ）だったのですが、去年も今年も（主にお茶女勢による）限定継続の発表を聞いては「限定継続ってなんだっけ」と思ってはググったり、教えてもらったりしていましたので、いい加減ちょっとは学んでおこうと思い、OchaCamlを入れて遊んでみました。
公式ページ通りにインストールしてみます(OSはUbuntu)。tarを落として
cd ~/Project/OchaCaml tar xpfvz cl75unix.tar.gz tar xpfvz OchaCaml.tar.gz patch -p0 < OchaCaml/OchaCaml.diff cd cl75/src make configure
と、ここでエラー。
gcc: エラー: 認識できないコマンドラインオプション ‘-no-cpp-precomp’ です
これは公式に対応が載ってた。makefileのOPTSから消せばそれでいいらしい。
試してみたらconfigure完了。
make configure make world
でビルドも成功。インタプリタを起動させてみる。
~/Project/OchaCaml/OchaCaml/ochacaml
またエラー。「(Home)/cl75/src/camlrun がないです」とのこと。よく見ると公式ページに"Adjust the third line of OchaCaml/ochacaml to your environment. "とある。のでochacamlの3行目をcamlrunの場所に書きかえる。
~/Project/OchaCaml/OchaCaml/ochacaml > Caml Light version 0.75 + shift/reset #
できた。
とりあえず行編集能力がないことを確認したので、
PATH=$PATH:~/Project/OchaCaml/OchaCaml alias ochacaml='ledit ochacaml'
と.bashrcに追加して環境の準備を終えた。
さて、何はともあれshift/resetですね。まずは型を見ましょう。
# shift;;
- : (('a -> 'b) / 'c -> 'c / 'd) / 'b -> 'a / 'd = <fun>
# reset;;
- : (unit / 'a -> 'a / 'b) -> 'b = <fun>
闇っぽいですね。S/A->T/BというのはS->T型なのだけれど、実行（評価？）するとanswer typeをAからBに変更する型、らしいです。answer type？
よくわかんないので論文*1を見てみると、answer typeとは直感的にはresetが返す型のことを言うらしいです。なんだかわかったようなわからないような……
つまり、resetは「unit -> 'a型で、かつanswer typeを'aから'bに変える関数を受け取って'bを返す」関数ということになります。
一方のshiftは、
- ('a -> 'b) -> 'c型で、かつanswer typeを'cから'dに変える関数を受け取って
- 'a型を返し、
- shift関数自身はその実行によってanswer typeを'bから'dに変える。
ということになるのでしょうか。
このへんでわけわからん感じになったので、shift/reset プログラミング入門を読みつつまずは挙動から理解していくことにしました。
shift/resetは
reset (fun () -> C[shift (fun k -> M)])
が(Cは継続*2)
- kにfun x -> C[x]を束縛
- Mを評価
という風に評価されるとのこと。
つまり
評価文脈として E := ... | reset (fun () -> E) | ... みたいになってるっぽい？
— xenophobia (@xenophobia__) 2014, 3月 9
継続を追加するってのはつまり、reset (λ_ . E[shift(fun k -> M)]) → M[k := λx.E[x]]（xはfresh） みたいなreduction relationとさっきの評価文脈を加えること、という理解でいいのかな？
— xenophobia (@xenophobia__) 2014, 3月 9
ということとして理解してよさそう。
なんとなく動作はわかったんで遊びます。
# reset (fun () -> 3 + shift (fun k -> 4 + k 3) * 5);; - : int = 22 # reset (fun () -> shift (fun k -> k) * 2) 123;; - : int = 246
楽しいですね。計算を保留してresetのとこまで一気に戻れるというのはなかなか豪快です。使い道はまだ見えてきませんが。
ちまい例ではまだよくわからんのでもっと複雑な計算をshiftでぶった切ってみましょう。複雑な計算といえば再帰ですね。shift/resetプログラミング入門2.7章を参考に、フィボナッチ関数を再帰の末端に辿りつく度止めるような関数を書いてみます。
let rec path_str_rev = function | -> raise (Invalid_argument "empty path") | x:: -> string_of_int x | x::xs -> path_str_rev xs ^ " -> " ^ string_of_int x;; type 'a result = Cont of (int list * (unit / 'a -> 'a result / 'a)) | Ans of int;; let rec fib_path path n = if n<2 then (shift (fun k -> Cont(path, k));1) else fib_path (n-1 :: path) (n-1) + fib_path (n-2 :: path) (n-2);; let fib_path_start n = reset (fun () -> Ans (fib_path [n] n));; let rec loop = function | Ans n -> print_endline ("Answer = " ^ string_of_int n) | Cont (path, k) -> begin print_endline (path_str_rev path); loop (k ()) end;; let _ = loop (fib_path_start 5);;
実行すると
# load "TestCode/test.ml";; path_str_rev : int list -> string =Type result defined. fib_path : int list => int => int = fib_path_start : int -> 'a result = loop : 'a result => unit = 5 -> 3 -> 1 5 -> 3 -> 2 -> 0 5 -> 3 -> 2 -> 1 5 -> 4 -> 2 -> 0 5 -> 4 -> 2 -> 1 5 -> 4 -> 3 -> 1 5 -> 4 -> 3 -> 2 -> 0 5 -> 4 -> 3 -> 2 -> 1 Answer = 8 - : unit = ()
となります。
なんとなく、どういう型合わせが必要かは掴みかけてきましたが、answer typeの概念がちゃんとわかっている自信はないので、もっとよく調べないとですね。
型に関しては追い追い調べるとして、ひとまず今回はここまで。
Egisonプログラミング実例研究： pattern functionとmatcherの活用例
これは Egison Advent Calendar 2013 ２日目の記事です。
「パターンマッチ指向プログラミング」を謳うEgisonでプログラミングすることにおいては当然「パターンをどのように記述するか」ということが最重要課題になってきます。
関数型プログラミングにおいて、大きな関数はより小さな単位の関数の組合せで表わされるように、Egisonではパターンをより柔軟に記述するためにパターンを再利用可能な形でモジュール化(modularization)する pattern-function や、同じデータ型に対する「パターンマッチングによる分解の仕方」を記述する matcher の仕組みが備わっています。これらは全て、「パターンマッチにより値を分解してデータを得る」という操作を、既存のどんな言語より柔軟に行う為のEgison独自の機能です。
ここではこれらのシンタクスや意味論を述べたりすることは目的としません。後に述べるようにpattern-functionは難しいものではありませんし、matcherについては公式か、手前味噌ですが私が書いた Egisonのmatcherの定義（基本編） - claustrophobia を参照してくれればわかると思います。そうではなく、この記事はpatternのモジュール化機能やmatcherによって、パターンマッチングの記述力が如何に豊かなものとなるかを実例を通して見ていくことを目標にしています。
・型無しλ計算（+整数リテラル、オペレータ）のevalの実装
型無しλ計算のeval、すなわち簡約を実装するときには、λ項をパターンマッチングによって分解していくことになります。つまり対象のλ項を分解し、β基を見付けたらβ簡約すればいいわけです。
（λ項 t := x(変数) | λx.t（λ抽象*1）| t1 t2（適用））
(λx. (λy. x y)) (λz. z z)
↓ β簡約（xに(λz. z z)を代入）
(λy. (λz. z z) y)
ここでは純粋なλ計算をちょっと複雑にして、型無しλ項に整数・整数の加算・整数の乗算をプリミティヴとして加えた体系を考えてみます。まずはλ項を表すalgebraic data matcher: termを定義します。
(define $operator (algebraic-data-matcher {<plus> <mult>}))
(define $term
(algebraic-data-matcher
{<var string>
<int integer>
<op operator term term>
<lam string term>
<app term term>}))
整数とその演算を加えたので、evalに際しては先に見たβ簡約の他に、"1+1"のような式を見つけたら"2"に簡約するという操作も考えることになります。
演算子のmatcherも作ったので、この「演算」は次のように「演算子を渡して「整数をその演算子で計算する関数」を返す関数」を書いて実装することにします。
(define $op-reduce
(match-lambda operator
{[<plus> (match-lambda [term term]
{[[<int $i1> <int $i2>] <Int (+ i1 i2)>]})]
[<mult> (match-lambda [term term]
{[[<int $i1> <int $i2>] <Int (* i1 i2)>]})]}))
代入は次のように定義されます。"^,x"というパターンはEgison独自*2のもので、NOTパターン"^(pattern)"は「(pattern)にマッチしない」、Valueパターン",(expr)"は「(expr)を評価した値にマッチ」を意味します。つまり"^,x"で「変数xの値にマッチしない値にマッチ」となり、λ抽象によるshadowingをうまく表現しています。
ただし、この代入関数で自由変数を含む項を代入しようとすると変数の捕獲が起きる可能性があります。が、ここでは閉じた項に関する代入しか起こらないと仮定します。実際、これから書く例では問題なく動作します。
(define $subst
(lambda [$x $t]
(letrec {[$go
(match-lambda term
{[<var ,x> t]
[<op $ope $t1 $t2> <Op ope (go t1) (go t2)>]
[<lam (& $y ^,x) $t1> <Lam y (go t1)>]
[<app $t1 $t2> <App (go t1) (go t2)>]
[$t t]})]} go)))
Egisonで１ステップのevalを実装してみます。まず「値呼び戦略(call-by-value)」すなわち次の規則に従って（1ステップの）簡約が進むevalを考えます。
Case 1. e1 + e2：e1もe2も値であるなら足した結果の整数を返す。そうでなければe1(or e2)の簡約を1ステップ進める。
Case 2. e1 * e2 ： Case 1と同様
Case 3. e1 e2(関数適用)：e1=λx.eでe2も値ならβ簡約。そうでなければe1(or e2)の簡約を1ステップ進める。
この場合分けをパターンマッチで書けばいいだけです
・pattern functionによる「よく使うパターン」のモジュール化
ここで問題になってくるのが「e1 + e2でe1もe2も値だったとき」のような状況の判定です。このケースに限らず、値にマッチするパターンを簡潔に書きたいところです。
Egisonでは、こうした再利用性のあるパターンをpattern functionによってモジュール化できます。
(define $value
(pattern-function [$p] (& (| <var _> <int _> <lam _ _>) p)))
このvalueは1引数のpattern functionであり、(value p)は「値pにマッチする」という意味のパターンです。これを利用すれば、先の「e1 + e2でe1もe2も値だったとき」と「e1 + e2でe1が値、e2が値でない」は次のように書きわけられます。
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbv-naive t)>]
これなら、ガードを使ってパターンに補助的な述語を付けるより直接的にパターンに「値にマッチする」情報を書けて直感的です。*3
値呼び戦略の１ステップ簡約は次のようになります。マッチ先における分岐が一切ないように定義することができていますね。
(define $beta-reduce-cbv-naive
(match-lambda term
{[<app <lam $x $t> (value $v)> ((subst x v) t)]
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbv-naive t)>]
[<op $ope $t1 $t2> <Op ope (beta-reduce-cbv-naive t1) t2>]
[<app (value $v) $t> <App v (beta-reduce-cbv-naive t)>]
[<app $t1 $t2> <App (beta-reduce-cbv-naive t1) t2>]
[$v v]}))
これでevalの完成です。折角なので関数fで項tをnステップ簡約する関数"n-step"を
(define $n-step
(lambda [$f $t $n]
(if (lte? n 0)
t
(n-step f (f t) (- n 1)))))
と定義して次のexpl
(define $identity <Lam "me" <Var "me">>)
(define $onetwo <Op <Plus> <Int 1> <Int 2>>)
(define $expl <App identity onetwo>)
を簡約してみると
> (n-step beta-reduce-cbv-naive expl 1)
<App <Lam me <Var me>> <Int 3>>
> (n-step beta-reduce-cbv-naive expl 2)
<Int 3>
ちゃんと動いていますね。
・matcherによる評価文脈の分離
私たちはここで、別の評価戦略を考えることもできます。
名前呼び戦略(call-by-name)はいわゆる遅延評価の一つで、次のような規則に従って簡約が進みます。
Case 1. e1 + e2：e1もe2も値であるなら足した結果の整数を返す。そうでなければe1(or e2)の簡約を1ステップ進める。
Case 2. e1 * e2 ： Case 1と同様
Case 3. e1 e2(関数適用)：e1=λx.eならβ簡約。そうでなければe1の簡約を1ステップ進める。
つまり、関数適用の際に引数を評価しないということです。これも先の値呼びと同じく次のように書くことができます。
(define $beta-reduce-cbn-naive
(match-lambda term
{[<app <lam $x $t1> $t2> ((subst x t2) t1)]
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbn-naive t)>]
[<op $ope $t1 $t2> <Op ope (beta-reduce-cbn-naive t1) t2>]
[<app $t1 $t2> <App (beta-reduce-cbn-naive t1) t2>]
[$v v]}))
> (n-step beta-reduce-cbn-naive expl 1)
<Op <Plus> <Int 1> <Int 2>>
> (n-step beta-reduce-cbn-naive expl 2)
<Int 3>
さてこれらのコードを見ると、ほとんど同じ書き方で書いているような気がします。そこで、評価戦略の違いをうまく吸収した統一的なbeta-reduce関数を書けないかと考えてみます。つまり、評価文脈を何らかの形で与えてやって、それによってcall-by-valueのevalにもcall-by-nameのevalにもできるような関数です。
簡約というのは一般に、次のように「簡約できる場所 E」*4にある「簡約できる項 t」を評価するということです。
・([(λx.x + 1) 3]) + 5 → ([3 + 1]) + 5 → [4 + 5] → 9
・([(λx.x x) (λy.y)]) (λz.z) → ([(λy.y) (λy.y)]) (λz.z) → [(λy.y) (λz.z)] → (λz.z)
よって、次のような抽象化を考えられます。λ項をパターンマッチにより「簡約できる場所 E」「簡約できる項 t」に分解するようなmatcherを引数に取り、
(define $beta-reduce
(lambda [$strategy]
(match-lambda strategy
{[<context $e <app <lam $x $t1> $t2>> (e ((subst x t2) t1))]
[<context $e <op $ope (value $v1) (value $v2)>> (e ((op-reduce ope) v1 v2))]
[$v v]})))
のような関数を書けば２つの評価戦略を統一できます。（ここでeは項tを受け取って「簡約できる場所」に再び埋めこむ関数）
このmatcherはちゃんと定義でき、例えばcall-by-valueなら次のようになります。
(define $call-by-value
(matcher
{[<context $ $> [something term]
{[<App $t1 $t2> (match [t1 t2] [term term]
{[[(value _) (value _)] {[(lambda [$t] t) <App t1 t2>]}]
[[(value _) _]
(match t2 call-by-value
{[<context $e $t> {[(lambda [$nt] <App t1 (e nt)>) t]}]
[_ {}]})]
[[_ _]
(match t1 call-by-value
{[<context $e $t> {[(lambda [$nt] <App (e nt) t2>) t]}]
[_ {}]})]})]
[<Op $ope $t1 $t2> (match [t1 t2] [term term]
{[[(value _) (value _)] {[(lambda [$t] t) <Op ope t1 t2>]}]
[[(value _) _]
(match t2 call-by-value
{[<context $e $t> {[(lambda [$nt] <Ope ope t1 (e nt)>) t]}]
[_ {}]})]
[[_ _]
(match t1 call-by-value
{[<context $e $t> {[(lambda [$nt] <Ope ope (e nt) t2>) t]}]
[_ {}]})]})]
[_ {}]}]
[$ term {[$t {t}]}]}))
ちょっと複雑ですが、結局再帰的にcall-by-valueにマッチさせてその結果をもとに組み立てる、ということを繰り返しています。call-by-nameも同様に書けます。
こんな風に私たちは同じデータ表現に対して２つ以上のmatcherを定義することで、パターンマッチの仕方を柔軟に切り換えることができます。このように「データの取り出し方は違うが、取り出したデータの組み立て・変換は共通」のようなアルゴリズムがあったとき、matcherはそこから「データの取り出し方」を分離する役目を担うことができます。
・recursive pattern functionの威力
さて、今まで私たちはevalで評価する項は閉じた項であると仮定してきました。つまり、evalで評価する項が自由変数を持っていてはいけません。
では、「自由変数を持った項」はどのように判定すればよいでしょうか？よくある方法が、「自由変数の集合」を求めてみてそれが空であることを判定する方法です。
しかしEgisonでは「閉じた項にマッチするパターン」をpattern functionによって書くことができます。
(define $closed-term
(pattern-function [$p]
(& (freevar-check ^_) p)))
(define $freevar-check
(pattern-function [$bound-vars]
(| <var bound-vars>
<int _>
<op _ (freevar-check bound-vars) (freevar-check bound-vars)>
<lam $x (freevar-check (| bound-vars ,x))>
<app (freevar-check bound-vars) (freevar-check bound-vars)>)))
(closed-term p)が「閉じた項pにマッチする」パターンを表し、(freevar-check p)は「自由変数がpにマッチする項にマッチする」パターンを表します。"^_"はワイルドカードの否定で何に対してもマッチが失敗するので、つまり(closed-term p)とは「自由変数が何にもマッチしない（＝自由変数などない）項pにマッチ」という意味になります。
> (match identity term {[(closed-term $t) t] [_ <ThereAreFreeVars>]})
<Lam me <Var me>>
> (match <App identity <Var "u">> term {[(closed-term $t) t] [_ <ThereAreFreeVars>]})
<ThereAreFreeVars>
ここで注目すべきは、pattern function freevar-checkは再帰関数であるということです。つまりpattern functionは再帰的定義を許します。これは、pattern functionが無限のパターン表現を表すことができるということを意味します。再帰的なpattern functionを使うことでより柔軟なパターンの記述力を得ることができます。
・部品となるpattern functionの組み立て
関数型プログラミングにおいては、部品となる関数を組み立てることでより大きく複雑な関数を定義します。パターンマッチ指向型言語であるEgisonでは、patternを組合せてより複雑なパターンを記述することが可能です。
λ項は帰納的に定義されています。つまり、λ抽象は「λx.(λ項)」という形をしていますし、適用は「(λ項) (λ項)」という形をしています。つまり、λ項は演算型の項・λ抽象・適用をノードとして変数・整数を葉とする木に見立てることができます。そこで、λ項の子ノードにマッチするようなpattern-function "children"を定義できます。
(define $children
(pattern-function [$t]
(| <lam _ t>
<op _ t _> <op _ _ t>
<app t _> <app _ t>)))
さらに、このchildrenを用い、λ項のsubtree全てにマッチするようなpattern function "subtree"を定義できます。
(define $subtree
(pattern-function [$t]
(| t (children (subtree t)))))
さらにさらに、このsubtreeと、先に出てきたfreevar-checkを組合せることで、λ項に表れる全てのμ基: 「λx.M x(ただしMの中に自由なxは出てこない)」にマッチするpattern function "myu-redex"を作れます。
(define $myu-redex
(pattern-function [$x $t]
(subtree <lam x <app (& t (freevar-check ^x)) <var x>>>)))
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(children $t) t])
{<Lam x <App <Lam me <Var me>> <Var x>>> <Int 0>}
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(subtree $t) t])
{<App <Lam x <App <Lam me <Var me>> <Var x>>> <Int 0>> <Lam x <App <Lam me <Var me>> <Var x>>> <Int 0> <App <Lam me <Var me>> <Var x>> <Lam me <Var me>> <Var x> <Var me>}
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(myu-redex $x $t) [x t]])
{[x <Lam me <Var me>>]}
このようにして、どう書いていいかわからない複雑なパターンも、小さい部品のパターンの組み合わせで作り出すことができるようになるのです。
・まとめ
今回主題にするつもりだったのはpattern functionで、matcherについては正直な話「やりたいだけ」でした。というより、以前からこういう形でのevalの定義、つまり評価文脈と簡約基を使ったβ簡約の定義*5を直接コードに落とせないかと思っていて、実際に実現できたので書いてみたというわけです。
しかし、上にも書きましたがmatcherを自分で書くとコードが煩雑になりやすいです。なので、今回Egisonのもう一つの革新的な機能であるpattern functionに焦点を当ててみました。既に見たとおりこちらはかなり簡潔に書けます。というより普通に関数を定義するのと同じ感じです。これは逆に、関数で値を操作するのと同じぐらい柔軟にパターンを操作できるということでもあります。
ちょっとでも面白い・便利そうだと感じたなら、是非、パターンが柔軟に扱える世界でのプログラミングを試してみてください。すると、実は今まで「データを取り出し」「データの性質によって処理を変える」というただそれだけのことに、極めて冗長で退屈な方法を取らされていたことに気付くと思います。
Egisonのmatcherの定義（基本編）
第1回 Egison Dev Meeting(http://egison.pira.jp/workshops/1-dev.html)に行ってきました。
Egison自体まだまだ色々と発展途上の言語なので、「この仕様はどうなのか」「ここはこの書き方でいいのか」「これからの展望は」などEgisonの今後に関する多くの意見があり、有意義なDev Meetingでした。
ただ、これは以前行われたEgisonのワークショップなんかでも思ったことですが、新しい概念を導入するときのコード例が複雑すぎる気がしました。そこで、その中でも特に重要かつ面白い"matcher"の定義方法についてチュートリアル的なものを書いてみます。この記事はその基本編で、matcherという概念自体の説明及び定義文のシンタックスに関する説明に重きを置いています。あとでもっとmatcherのすごさが伝わる応用編を書く予定です。予定です。
（注意：この記事はEgisonのよさを伝える記事というよりは、Egisonを実際に書く為の基本的ノウハウを共有するための記事であり、そのため極めて簡易的な機能の実装を目指しています。なので「それって別にパターンマッチングでやる必要なくね？」と思ったとしても気にせず読んでいただけたらと思います。）
（注意２：Egisonは現在進行形で開発されている言語なので、Syntaxやその他細かい仕様がいつまでもこの記事のままとは限りません。事実、この記事を書いている間にalgebraic-data-matcher構文のSyntaxが変わりました。*1）
なお、多少厳密さに欠けるところもあるため、詳細が知りたい人は公式マニュアル：How to Define Matchers（http://egison.pira.jp/manual3/how-to-define-matchers.html）を参照してください。
定義方法の前にそもそもmatcherとは、それ自体既存のパターンマッチングには登場しない概念なので、これについて整理します。
既存のパターンマッチは
match expr
pattern_1 -> expr_1
pattern_2 -> expr_2
...
pattern_n -> expr_n
のような構文によって、「exprを評価した値がpattern_iにマッチしたならば、そのマッチングによって得られた変数束縛によって拡張された環境のもとでexpr_iを評価する」というものでした。
これに対しEgisonの（matchによる）パターンマッチは
match expr matcher
pattern_1 -> expr_1
pattern_2 -> expr_2
...
pattern_n -> expr_n
のような構文を持ち、「exprを評価した値をmatcherとして見たとき、pattern_iにマッチしたならば、そのマッチングの結果の１つによって得られた変数束縛によって拡張された環境のもとでexpr_iを評価する」という意味を持ちます。
つまり、例えば既存のパターンマッチで「<cons 0 tail>」と書かれたパターンは、「先頭の要素が0のリストで、Tailを変数tailに束縛」のような意味でしかありえませんが、Egisonではmatcherの違いにより「先頭の要素が0のリストで、Tailを変数tailに束縛」「要素のうちの一つが0の多重集合で、0を取った残りの要素を変数tailに束縛」「要素のうちの一つが0の集合で、元の集合＝set∪{0}となるようなsetを変数tailに束縛」のように、「<cons ....>」が様々な意味を持ち得ます。さらには「0」でさえ、単なる「整数値0」という意味だけでなく、「3で割ったら0になる値」のようなマッチングも可能です。*2
つまるところmatcherとは、既存の言語では「値を評価してデータの構造レベルで比べる」というたった１つの方法しかなかった「パターンマッチングの方法」を独自に定義するものです。様々なmatcherを定義して使うことで、柔軟な方法によるパターンマッチングを実現することができます。
さて本題です。Egisonのパターンマッチの柔軟さを示す例として、まず紹介されるのがmultisetというmatcherで、これはコレクションを多重集合と見て（つまりリストと違い順序を無視して）パターンマッチすることができるというものです。matcherの使い方・定義方法の説明には今までこのmultisetが使われてきました。しかし、使用方法はともかく、multisetの定義はとっかかりとしては大きすぎ、実際ここですこし引いてしまうようなところがあります。
そこで、もっと小さく、しかし既存のパターンマッチングでは実現できなかった例として同じ型のペア（対）に対するmatcherを定義することを考えてみます。
別に特別高機能な言語でなくとも、ペアに相当するデータ構造を定義するのは容易です。OCamlやHaskellでは普通に2-タプルを使えばいいですし、例えばHaskellだったら
data Pair a = Pair a a
のようにデータ型としても定義できるわけです。OCamlならバリアントを使えばいいですね。
しかし、そのパターンマッチの仕方としては、Pairを順序対として見るような方法しかありません。つまり、Pair x 4のようなパターンでPair 3 4という値をマッチさせると、{x=3}という束縛が手に入ります。
しかし、ペアの値を考えるにあたって順序が重要でない、あるいは意図的に無視したい場合があります。そこでこれから、Egisonで順序対・非順序対のmatcher、つまり、
> (test (match <Pair 4 3> (unordered-pair integer) {[<pair $x ,4> <Just x>] [_ <Nothing>]}))
<Just 3>
> (test (match <Pair 4 3> (ordered-pair integer) {[<pair $x ,4> <Just x>] [_ <Nothing>]}))
<Nothing>
となる*3ようなmatcher ordered-pairとunordered-pairを定義してみましょう。
順序対のmatcherは簡単です。matcher式を使うまでもありません。
先に述べたように、順序対としてのマッチは既存の言語にもある「データ構造に基づくパターンマッチ」です。このようなmatcherを実現するために、これを簡単に定義する構文糖algebraic-data-matcherがあります。
(define $ordered-pair
(lambda [$a]
(algebraic-data-matcher
{<pair a a>})))
(algebraic-data-matcher {...})で...に指定したコンストラクタ・パターンに対応するmatcherが定義できます。つまりordered-pair integerを指定した<Pair 2 5>のパターンマッチの結果は
- _ → {[]}
- $x → {[x = <Pair 2 5>]}
- <Pair $x $y> → {[x = 2, y = 5]}
のようになります。
本題の非順序対のmatcherです。定義は以下のようになります。
((1)...(10)は単なる参照)
(define $unordered-pair
(lambda [$a]
(matcher(1)
{[,$val(2) [](3)
{[$tgt(4) (match [val tgt] [(ordered-pair a) (ordered-pair a)]
{[(| [<pair $a $b> <pair ,a ,b>]
[<pair $a $b> <pair ,b ,a>]) {[]}(5)]
[_ {}(6)]})]}]
[<pair $ $> [a a](7)
{[<Pair $x $y>(8) {[x y] [y x]}(9)]}]
[$ [something](10)
{[$tgt {tgt}]}]})))
一気に複雑になりましたね。各部分の意味を読解します。
- (matcher {[case 1] [case 2] ... [case n]})
matcher式は「（パターン・再帰的に呼ぶmatcher・マッチング処理）をひとまとめにした節」のコレクションをとり、これ（コレクションの一要素）をプリミティブパターン節(primitive pattern clause)と呼びます。ここでは「,$val」「<pair $ $>」「$」の3つのケースに対するマッチング処理が記述されています。 - ,$val
パターンマッチ・ケースの第1要素にはプリミティブパターンパターン(primitive pattern pattern)と呼ばれる、パターンにマッチさせるパターンが記述されます。「このパターンはどの規則によってパターンマッチさせるべきか」という分岐処理はまさに「パターンに対するパターンマッチ」で記述されるべきだからです。現時点ではパターンに対するパターンはごく基本的なものに限られており、「,$val」はその一つのバリューパターンパターン(value pattern pattern)と呼ばれるものです。これは「,(コンマ)＋値」の形式のパターンすなわちバリューパターン(value pattern)にマッチするものです。つまりこのケースには、値「<Pair 3 4>」をパターン「,<Pair 4 3>」にマッチさせるときの処理が記述されています。 - []
Egisonだけでなく従来のパターンマッチにおいても、あるパターンへのマッチング処理が再帰的に他のパターンマッチを呼ぶことは普通にあることで、例えば「Pair 3 4」の「Pair x y」へのパターンマッチングは厳密には「Pair 3 4がPair x 4にマッチ」→「3がxにマッチ＆4が4にマッチ」→「{x=3}、4が4にマッチ」→「{x=3}」と進んでいくわけです。ここでは変数へのマッチングを呼んでいることになります。
さて、Egisonでmatcherを定義する際にはこのマッチングに使用するmatcherを明示しなくてはなりません。ここではバリューパターンへのマッチングであり、他のマッチングを呼ぶことはないので（上でいう「4が4にマッチ」に対応）空のタプルを書きます。 - $tgt
マッチング処理をするには、とりあえず普通の（プリミティヴな）方法で値を束縛・分解しなければなりませんが、それをするための「最も原始的なパターン」がプリミティブデータパターン(primitive data pattern)です。マッチング処理はプリミティブデータパターンによる原始的なパターンマッチングのマッチ節: [<primitive data pattern> (マッチング結果)]のコレクションによって書かれ、これらのマッチ節をプリミティブデータ節(primitive data clause)と言います。ここには1つのマッチ節しかなく、単なる変数束縛(primitive data variable: $+識別子)を使って、データ自体を変数に束縛しています。 - {[]}
Egisonでは、マッチング結果として複数の値を許します。よってマッチング結果はコレクションを返す仕様になっています。マッチング結果は、再帰的に呼ぶmatcherが[matcher_1 matcher_2 ... matcher_n]ならば[(matcher_1にマッチさせる式) (matcher_2にマッチさせる式)... (matcher_nにマッチさせる式)]となります。ここでは再帰的にマッチさせるmatcherはありませんので、マッチングが成功した場合は[]を1つ返すことでマッチングの成功を表現することになります。ここでやっているのは、「,$valにマッチしたバリューパターンの表す値が<Pair a b>か<Pair b a>で、マッチさせる値（$tgtに束縛されている）が<Pair a b>であればマッチング成功、そうでなければ失敗」という処理を、先程定義したordered-pairによるマッチングを使って書いています。 - {}
パターンマッチの失敗は、空のコレクション{}を返すことで表現します。「パターンマッチに失敗した＝マッチングの結果が0個」ということです。 - <pair $ $> [a a]
このケースは、<pair $x _>のようなパターンに対する処理が記述されています。<pair ...>はプリミティブインダクティブパターン(primitive inductive pattern)、$はプリミティブパターン変数(primitive pattern variable)と呼ばれます。
$は再帰的なパターンマッチングを行う場所を示すもので、3.では１つもなかった「再帰的なマッチングに用いるmatcher」がここでは指定されています。pairの要素に対応するmatcherはラムダでaに束縛しているため、ここでは２つともaを指定しておけばいいというわけです。 - <Pair $x $y>
4.ではマッチさせる値を変数に束縛するだけでしたが、今回は値を分解しています。ここで用いている<Pair ...>はプリミティブインダクティブデータ(primitive inductive data)というプリミティブデータパターンで、コンストラクタの先頭は値と同じ大文字になります。 - {[x y] [y x]}
このケースでは、前とは違いマッチング結果を返すケースです。マッチング結果を返すと、指定したmatcherによるパターンマッチングが結果のすべてについて行われます。
ここでは非順序対のmatcherを書きたいので、値「<Pair x y>」に対するパターン「<pair pattern_1 pattern_2>」をマッチングする際、「xにpattern_1がマッチ＆yにpattern_2がマッチ」と「yにpattern_1がマッチ＆xにpattern_2がマッチ」が行われて欲しいので、[x y]と[y x]の２つを指定します。 - $ [something]
最後のケースは上のどれにもあてはまらないパターン、すなわち変数パターン$xであり、このときは単純にxにマッチングさせる値を束縛すればいいことになります。
さて、実はここまで変数に値をマッチングさせる方法を一切紹介していません。最初のケースは束縛の必要がなく、次のケースも再帰的に呼ぶmatcherに後の処理を任せてしまっています。変数に値を束縛するにはどうすればいいのでしょうか？
ここで登場するのが唯一の組み込みmatcherであるsomethingです。somethingは変数パターンしか取れないmatcherで、変数パターンに対するマッチは必ず成功し、その変数に値を束縛します。ライブラリcollection.egiなどを見てもらえばわかりますが、この書き方はmatcherの最後によく来るので、イディオムとして覚えておくのもよいでしょう。
以上がunordered-pairの定義の読み方で、matcher定義の基本的な部分です。
まとめると、matcherを定義するには「マッチさせるパターンをプリミティブパターンパターンによるパターンマッチングによって分類」し、「マッチする値をプリミティブデータパターンによるパターンマッチングによって分類」し、それら分岐の先で「マッチング結果を返す」式を書けばいいことになります。こう言ってしまえば単純なのですが、やはりSyntaxが込みいっていることもあって初見はとまどってしまいますね。
しかし、上の定義を追えたのならば、もう後はわからないことは紹介していないプリミティブ{パターン or データ}パターンぐらいなもんでしょうから、上で紹介した公式マニュアル片手にライブラリのmatcherのコードも読めると思います。
次に読むとしたら先に挙げた多重集合か、剰余環Z/nZの上の等号を使ってマッチできるmod nなんかが面白いと思います。mod nを使うと「3で割ったあまりが2な数にマッチ」とか面白いことができます。
本記事はEgisonの本格的な紹介記事ではないので紹介しませんでしたが、先に述べたようにEgisonでは複数のマッチング結果を返せるので、従来のパターンマッチではありえなかった（というより、従来のパターンマッチではマッチング結果が一個しかないから意味がなかった）「複数のマッチング結果すべてを取り出して処理を行う」match-all 構文があります。これと組みあわせることでEgisonのパターンマッチはその真価を発揮することとなります。
Egisonはパターンマッチ指向言語ですので、matcherを独自に定義できるようになれば一気にできることの幅が広がります。是非独自matcherで色々遊んでみましょう。
