Haskell/Zippers

テセウスとZipper

迷宮

「テセウス、何か手を打たなければならない。」ホメロス…Ancient Geeks株式会社の営業部部長は言った。テセウスはミノタウロスアクションフィギュア™を後ろの棚に入れてうなずいた。「今の子供たちはもはや古代神話に興味を持っていない、彼らはスパイダーマンやスポーンのような現代ヒーローが好きなんだ。」ヒーロー。テセウスは、迷宮からクレタ島に戻った英雄^[1]だったから、どのくらいのものかをよく知っていた。しかし「現代ヒーロー」たちは現実的に現れるようなことはしなかった。何が彼らの勝因だったのか？とにかく、未払い金の問題が解決できなかった場合、株主たちはステュクス河を渡ってきてAncient Geeks株式会社を整理するだろう。

「閃いたぞ！テセウス、良い案がある！君のミノタウロスとの戦いの物語をコンピューターゲームにするんだ！どうだい？」ホメロスは正しかった。何冊かの本、叙事詩の歌(ヒットチャートは総なめ)、必須の映画三部作、そして数え切れないテセウスとミノタウロス™のギミックは出してきた。しかしコンピューターゲームは盲点だった。「完璧だよ。テセウス、すぐにゲームの開発に取りかかるんだ。」

真の英雄、テセウスは会社の命運を賭けた製品の開発言語にHaskellを選択した。もちろん、迷宮のミノタウロスを見つけ出すのがこのゲームの売りの一つになった。彼は熟考した。「二次元の迷宮はいろいろな方向に進むことができる。角度や距離といった詳細も抽象化できないとな。脱出方法を見つけるために、経路がどのように分かれるかを知っておく必要があるな。シンプルさを維持するには、迷宮は木構造をモデルにしよう。これなら、どこまで深く歩いても二股が再び合流することはないからプレイヤーが同じ所をぐるぐる廻ることはない。しかし、迷子になる機会は十分あるとおもう。それにヘビープレイヤーなら、左手の法則で迷路全体を探索することができる。」

data Node a = DeadEnd a
            | Passage a (Node a)
            | Fork    a (Node a) (Node a)

テセウスは迷路のノードにパラメータを運ぶa型を追加して作り上げた。後で、ここにはノードが指定する座標、その周辺の雰囲気、床の上に落ちているアイテムのリスト、迷宮を彷徨うモンスターのような、ゲーム関連の情報を保持することができる。Node aの全てのコンストラクタの最初の引数に格納されている、a型の値を変更したり取得したりする二つのヘルパー関数を仮定しよう。

get :: Node a -> a
put :: a -> Node a -> Node a

テンプレート:Exercises

「むむー、迷宮内のプレイヤーの現在位置はどのように表現しよう？プレイヤーは分岐を左か右のどちらへ進むか選択して深くへ潜っていけるとすると、こんな感じか」

 turnRight :: Node a -> Maybe (Node a)
 turnRight (Fork _ l r) = Just r
 turnRight _            = Nothing

「しかし、現在の迷宮のトップをサブ迷宮で置き換える方法は使えないな。戻れなくなってしまう。」彼は熟考した。「ああ、戻るためにはアリアドネの糸^[2]のトリックが使えるな。プレイヤーの位置を「辿ってきた分岐のリスト」にすれば単純に表現できる。「分岐のリスト」の糸を辿って戻ることもできるし、迷路は常に同じままだ。」

data Branch = KeepStraightOn
            | TurnLeft
            | TurnRight
type Thread = [Branch]

「例えば、[TurnRight,KeepStraightOn]という糸は、プレイヤーがエントランスから右へ分岐して、その後Passageをまっすぐ進んで現在の位置に辿り着いたということを意味する。糸をプレイヤーが伸ばしたり短くしたりすることによって迷路を探索することができる。具体的には、turnRight関数はTurnRightを追加することによって糸を伸ばす。」

turnRight :: Thread -> Thread
turnRight t = t ++ [TurnRight]

「アイテムのようなゲームに関連する追加のデータにアクセスするには、単純に糸から迷路に従えばいい。」

retrieve :: Thread -> Node a -> a
retrieve []                  n             = get n
retrieve (KeepStraightOn:bs) (Passage _ n) = retrieve bs n
retrieve (TurnLeft      :bs) (Fork _ l r)  = retrieve bs l
retrieve (TurnRight     :bs) (Fork _ l r)  = retrieve bs r

テンプレート:Exercises

この解決策はテセウスが満足するに至らなかった。「なんてこった、経路を伸ばしたり戻ったりする場合、リストの最後の要素を変更しなければならないじゃないか。リストを逆順に格納することはできるが、今度は迷宮内のプレイヤーの位置にアクセスするために何度も何度も糸を辿らないといけない。どちらのアクションも、糸の長さに比例した時間がかかってしまう。大規模な迷路ならこれはあまりにも長すぎる。他に方法はないのか？」

アリアドネのZipper

テセウスは熟練した戦士だったが、プログラミング技術を修練したわけではなかったので、満足のいく解決策を見つけることはできなかった。強烈ながらも無益な思考の後に、以前愛したアリアドネに電話して助言を求めることにした。結局のところ、糸のアイディアを持っていたのは彼女だったからだ。
テンプレート:Haskell speaker 2
我らが英雄はその声をすぐさま理解した。
「やあ、アリアドネ、テセウスだ。」
気まずい沈黙が会話を停止させた。彼女をナクソス島に捨てたテセウスが何故電話してきたのか理解していない事を思い出した。しかし、ハデスの道を逝くAncent Geeks株式会社、彼に選択の余地はなかった。
「ぁあ…、最愛の人、…元気だったかい？」
アリアドネは冷たい反応を返した。テンプレート:Haskell speaker 2
「えぇっと…、実は…実はな。プログラミングの問題で助けが必要なんだ。新しいコンピューターゲーム『テセウスとミノタウロス™』をプログラミング中なんだ。」
彼女はあざけ笑った。テンプレート:Haskell speaker 2
「アリアドネ、どうか頼む。Ancient Geeks株式会社は破産の危機にひんしている。このゲームが最後の望みなんだ！」
少し待った後、彼女は決定を下した。
テンプレート:Haskell speaker 2
テセウスは青ざめた。しかし他に何が出来るだろうか？状況は十分ひっ迫していたので、彼はアリアドネの取り分を10%で交渉し合意した。

テセウスが、彼が念頭に置いていた迷宮の表現をアリアドネに語ると、彼女はすぐさまアドバイスをくれた。
テンプレート:Haskell speaker 2
「えっ？私の"社会の窓"に何か問題があるのかい？」
テンプレート:Haskell speaker 2
「へえ」
テンプレート:Haskell speaker 2
「高速な更新が必要なことはわかっているけど、どのようにコーディングしたらいいんだい？」
テンプレート:Haskell speaker 2
「けど、問題はどうやって戻ればいいんだい？サブ迷宮はプレイヤーがどう分岐してきたかが全て失われてしまう。」
テンプレート:Haskell speaker 2 アリアドネはテセウスが困惑するのを満喫できましたが、彼が既にアリアドネの糸を使用したことに不満を言う隙を与えず、
テンプレート:Haskell speaker 2

type Zipper a = (Thread a, Node a)

zipperはアリアドネの糸と現在プレイヤーが立っているサブ迷宮の組。メインの糸は赤色でサブ迷宮はそこに接続されており、そのような迷宮全体は組から再構築できる。

テセウスは何も言わなかった。
テンプレート:Haskell speaker 2

data Branch a  = KeepStraightOn a
               | TurnLeft  a (Node a)
               | TurnRight a (Node a)
type Thread a  = [Branch a]

テンプレート:Haskell speaker 2
テセウスが遮った、「待ってくれ、turnRightのような関数をどのように実装したらいいんだ？TurnRightの最初の引数の型aは何にすればいいんだ？あぁ、わかった。失われてしまう分岐はくっつける必要はないが、Forkの追加データも同様に失われてしまう。けど、予備を使って新しい分岐を生成できる。

branchRight (Fork x l r) = TurnRight x l

「何らかの方法で既存の糸を拡張する必要があるな。」
テンプレート:Haskell speaker 2
なるほど、これは伸ばすときと戻るときだけ定数時間になって、以前のバージョンのような長さに比例した時間がかかることはないわけだ。だからturnRightの最終バージョンは…」

turnRight :: Zipper a -> Maybe (Zipper a)
turnRight (t, Fork x l r) = Just (TurnRight x l : t, r)
turnRight _               = Nothing

入り口から右のサブツリーを取る。もちろん、糸は最初は空である。糸は後ろ向きに実行することに注意する、すなわち最上位のセグメントは最も最近のもの。

「これは簡単だった。よし、続けて回廊を真っ直ぐ進むkeepStraightOnに取りかかろう。これは追加のデータを維持するのが必要な分岐の選択よりも簡単だ。」

keepStraightOn :: Zipper a -> Maybe (Zipper a)
keepStraightOn (t, Passage x n) = Just (KeepStraightOn x : t, n)
keepStraightOn _                = Nothing

テンプレート:Exercises

嬉しそうに彼は続け、「しかし興味深いのは戻っていくときだな。やってみよう…」

back :: Zipper a -> Maybe (Zipper a)
back ([]                   , _) = Nothing
back (KeepStraightOn x : t , n) = Just (t, Passage x n)
back (TurnLeft  x r    : t , l) = Just (t, Fork x l r)
back (TurnRight x l    : t , r) = Just (t, Fork x l r)

「もし糸が空なら、まだ迷宮の入り口で戻ることはできない。それ以外の場合は、糸を巻かなければならない。糸につなげたおかげで、実際に来た道からサブ迷宮を再構築することができる。」
アリアドネが言った。テンプレート:Haskell speaker 2

テンプレート:Exercises

わかったぞ！これは一部をアリアドネコンサルティングに売却したとしても、Ancient Geeks株式会社が優先すべき、テセウスが求めていた解決策だった。しかし一つだけ疑問が残った。
「なんでzipperと呼ばれているんだ？」
テンプレート:Haskell speaker 2
「アリアドネの真珠のネックレス、ね…。」彼は軽蔑を向けた。「君の糸に助けられたよ。クレタ島の時のように」
テンプレート:Haskell speaker 2彼女は答えた。
「フン、もう糸は必要ない。」
彼の驚いたことに、彼女は同意して、テンプレート:Haskell speaker 2

指で焦点を掴み、下から持ち上げると枝がぶら下がって指差したノードをトップとする新しい木が形成され、代数的データ型で構成する準備が整う。

「ああ。」彼はアリアドネの糸はもう必要としていないが、アリアドネは必要だという事を伝えようとしている？その言葉はあまりに饒舌だった。
「ありがとう、アリアドネ。元気で」
電話を介していて直接見ることはできなかったが、彼女は作り笑いを隠さなかった。

テンプレート:Exercises

半年が過ぎ、テセウスはショッピングウィンドウの前で立ち止まった。冷たい雨に逆らうため防寒着のフードを被った。点滅する文字が告げていたのは…。

"Spider-Man: lost in the Web"

- 糸の迷宮から君の方法を見つけ出せ -
Ancient Geeks株式会社が送る最高のコンピューターゲーム

彼はアリアドネに電話した日を呪って、会社の一部を彼女に売却した。 WineOS社による不自然な敵対的買収は彼女の仕業だったのだろうか。アリアドネの夫ディオニソス^[3]が率いていたのだろうか？テセウスはガラス窓の下に落ちる雨を見つめた。生産ラインが変更されれば、もう誰もミノタウロス™とテセウスの商品を生産しないだろう。彼はため息をついた。彼の時間、英雄の時間は終わりを告げた。今はスーパーヒーローの時代が来たのだ。

データ型の微分

前のセクションでzipperを提示したが、別のサブツリーに焦点を当てる事ができる指で、ツリーのようなデータ構造Node aを強化する方法がある。特定のデータ構造Node aのzipperを構築子ながら、異なる木構造をつなげて構築することは手で簡単に行うことができる。テンプレート:Exercises

機械的な微分

しかし任意の(適切な正規の)データ型のzipperは機械的に導出することもできる。驚くべき事に、「導出（derive）」は文字通りの意味で、zipperはデータ型の導関数(derivative)によって得ることが出来る。最初の発見はConor McBride^[4]によって述べられた。以降のセクションでは、この本当にすばらしい数学の宝石を解明しよう。

体系的な構成のため、私たちは型の計算が必要になる。型の構造的な計算の基礎は[[../Generic Programming/]]の章で概説されており、この素材に大きく頼っている。

zipperが共通に持っているものと、どのように微分を仄めかしているのかを理解するためにいくつかの例を見ていこう。二分木の型は再帰式の不動点で、

𝑇 𝑟 𝑒 𝑒 2 = 1 + 𝑇 𝑟 𝑒 𝑒 2 \times 𝑇 𝑟 𝑒 𝑒 2

.

木を渡り歩くとき、左または右のサブツリーに入ることを繰り返し選択し、アリアドネの糸には入らなかった方のサブツリーをくっつける。したがって、糸の枝は次の型を持つ。

𝐵 𝑟 𝑎 𝑛 𝑐 ℎ 2 = 𝑇 𝑟 𝑒 𝑒 2 + 𝑇 𝑟 𝑒 𝑒 2 ≅ 2 \times 𝑇 𝑟 𝑒 𝑒 2

.

同様に、三分木

𝑇 𝑟 𝑒 𝑒 3 = 1 + 𝑇 𝑟 𝑒 𝑒 3 \times 𝑇 𝑟 𝑒 𝑒 3 \times 𝑇 𝑟 𝑒 𝑒 3

は次のような型の枝を持つ。

𝐵 𝑟 𝑎 𝑛 𝑐 ℎ 3 = 3 \times 𝑇 𝑟 𝑒 𝑒 3 \times 𝑇 𝑟 𝑒 𝑒 3

なぜなら全ての段階で、3つのサブツリーを選択でき、入らなかった二つのサブツリーを格納しなければならない。これは微分 $\frac{d}{d x} x^{2} = 2 \times x$ や $\frac{d}{d x} x^{3} = 3 \times x^{2}$ とは似ても似つかないと思うだろうか？

謎を解く鍵は、データ構造のワンホールコンテキスト(one-hole context)の概念だ。 $X$ 型をパラメタライズしたデータ構造、 $𝑇 𝑟 𝑒 𝑒 X$ 型のようなものを想像しよう。この $X$ 型の要素を構造から一つ削除して、なんらかの方法でその位置を空とマークした場合、「マークした穴(hole)」とデータ構造を得られる。結果は「ワンホールコンテキスト」と呼ばれ、「穴」に $X$ 型の要素を挿入すると完全に満たされた $𝑇 𝑟 𝑒 𝑒 X$ が戻ってくる。「穴」は、位置の識別、焦点の役割を果たす。図でこれを説明しよう。

もちろん、我々の興味はワンホールコンテキストに与える型、すなわちHaskellでこれをどのように表現するかだ。問題は焦点を効率よくマークするにはどうしたらいいだろうか。しかし我々が見るように、型の構造に関する帰納法によってワンホールコンテキストの表現を見つけだし、効率的なデータ型につながるワンホールコンテキストを自動的に取得したいと思う^[5]。さて、データ構造 $F X$ と関手 $F$ 、そして引数の型 $X$ を与えよう。 $\partial F$ という表記法を選択する理由は既におわかりと思うが、ワンホールコンテキストの加法、乗法、合成の法則は、まさに微分におけるライプニッツ則である。

ワンホールコンテキスト		解説
$(\partial 𝐶 𝑜 𝑛 𝑠 𝑡_{𝐴}) X$	$= 0$	$A = 𝐶 𝑜 𝑛 𝑠 𝑡_{𝐴} X$ の中に $X$ は存在しない。つまりワンホールコンテキストの型は空でなければならない。
$(\partial 𝐼 𝑑) X$	$= 1$	$X = 𝐼 𝑑 X$ の中に $X$ の要素が一つだけ存在する場所がある。 $X$ を一つ削除すると、結果は $X$ を残さない。削除できる場所が一つだけ存在するから、 $𝐼 𝑑 X$ はまさにワンホールコンテキストの一つである。したがって、ワンホールコンテキストの型は単一の要素からなるシングルトン型である。
$\partial (F + G)$	$= \partial F + \partial G$	$F + G$ 型は、型 $F$ か型 $G$ のいずれかであるとすると、ワンホールコンテキストもまた $\partial F$ か $\partial G$ である。
$\partial (F \times G)$	$= F \times \partial G + \partial F \times G$	二つの型の組のワンホールコンテキストは、第一または、第二成分のいずれかが穴である。
$\partial (F \circ G)$	$= (\partial F \circ G) \times \partial G$	連鎖律(Chain rule)：合成の穴は囲んでいる構造に穴を開け、そこに密閉構造を当てはめることによって生じる。

もちろん、穴を埋める関数plugの型は $(\partial F X) \times X \to F X$ を持つ。

これまでのところ、 $\partial$ という構文は異なる関手を表している。すなわち、一つの引数を持つ型関数の種(kind)である。しかし、計算のためにもう少し適した $\partial_{X}$ という表記法もある。添え字は微分したい変数を表している。一般には

(\partial F) X = \partial_{X} (F X)

である。例を挙げると以下のようになる。

\partial (𝐼 𝑑 \times 𝐼 𝑑) X = \partial_{X} (X \times X) = 1 \times X + X \times 1 ≅ 2 \times X

もちろん、 $\partial_{X}$ は単にポイントワイズで、 $\partial$ はポイントフリースタイルである。

テンプレート:Exercises

微分を介したZipper

上記の規則で再帰的データ型 $μ F : = μ X . F X$ のzipperを構築することができる。ここで $F$ は多項式関手(polynomial functor)である。Zipperは特定のサブツリーに焦点を移す。すなわち、大きな木構造の内側は同じ種類の $μ F$ 型のサブ構造である。前章のように、焦点を向けたい場所のサブツリーと糸、これはサブツリーが格納されているコンテキストだが、この二つによって表現することが出来る。

{𝑍 𝑖 𝑝 𝑝 𝑒 𝑟}_{F} = μ F \times {𝐶 𝑜 𝑛 𝑡 𝑒 𝑥 𝑡}_{F}

今、コンテキストは $F μ F$ の中から選択した特定のサブツリー $μ F$ の各手順である。したがって、選ばなかったサブツリーはワンホールコンテキスト $\partial F (μ F)$ と一緒に回収される。このコンテキストの穴は選択したサブツリーから削除しながら帰ってくる。置くことも一緒で、

{𝐶 𝑜 𝑛 𝑡 𝑒 𝑥 𝑡}_{F} = 𝐿 𝑖 𝑠 𝑡 (\partial F (μ F))

を得る。または同じ事だが

{𝐶 𝑜 𝑛 𝑡 𝑒 𝑥 𝑡}_{F} = 1 + \partial F (μ F) \times {𝐶 𝑜 𝑛 𝑡 𝑒 𝑥 𝑡}_{F}

具体的な計算過程がどのようになるかを説明するために、体系的に迷宮データ型のzipperを構築しよう。

data Node a = DeadEnd a
            | Passage a (Node a)
            | Fork a (Node a) (Node a)

この再帰型は次のような不動点である。

𝑁 𝑜 𝑑 𝑒 A = μ X . {𝑁 𝑜 𝑑 𝑒 𝐹}_{A} X

この関手は次のようなものだ。

{𝑁 𝑜 𝑑 𝑒 𝐹}_{A} X = A + A \times X + A \times X \times X

言い換えると、

𝑁 𝑜 𝑑 𝑒 A ≅ {𝑁 𝑜 𝑑 𝑒 𝐹}_{A} (𝑁 𝑜 𝑑 𝑒 A) ≅ A + A \times 𝑁 𝑜 𝑑 𝑒 A + A \times 𝑁 𝑜 𝑑 𝑒 A \times 𝑁 𝑜 𝑑 𝑒 A

.

微分で読むと、

\partial_{X} ({𝑁 𝑜 𝑑 𝑒 𝐹}_{A} X) ≅ A + 2 \times A \times X

そして次を得る。

\partial {𝑁 𝑜 𝑑 𝑒 𝐹}_{A} (𝑁 𝑜 𝑑 𝑒 A) ≅ A + 2 \times A \times 𝑁 𝑜 𝑑 𝑒 A

.

したがって、コンテキストで読むと、前章のものと比べてみると、

data Branch a  = KeepStraightOn a
               | TurnLeft  a (Node a)
               | TurnRight a (Node a)
type Thread a  = [Branch a]

期待通り両者が全く同じものであることがわかるだろう！

テンプレート:Exercises

引数の関数に関する微分

ワンホールコンテキストの型を見つけるときの一つはd f(x)/d xを行うことである。それは、d f(x)/d g(x)のような式を完全に解くことが可能だ。例えば、d x^4 / d x^2は2x^2を与えて解くと、4つのタプルの2ホールコンテキストである。導関数は次のようなものである。

u=x^2と置くと、

d x^4 / d x^2 = d u^2 /d u = 2u = 2 x^2

Zipper vs コンテキスト

しかし一般的には、zipperとワンホールコンテキストは異なるもので表される。zipperは勝手なサブツリーの焦点である一方、ワンホールコンテキストは型構築子の引数にだけ焦点を当てることができる。次のデータ型を例に取ろう。

 data Tree a = Leaf a | Bin (Tree a) (Tree a)

ここで不動点は次の通りである。

𝑇 𝑟 𝑒 𝑒 A = μ X . A + X \times X

.

zipperはサブツリーのトップであるBinやLeafに焦点を当てることが出来るが、 $𝑇 𝑟 𝑒 𝑒 A$ のワンホールコンテキストの穴はLeafだけに焦点を当てるだろう。なぜなら、これは $A$ 型の要素が存在しているからだ。 $𝑁 𝑜 𝑑 𝑒 A$ の導関数はサブツリーの全てのトップが常に $A$ で飾られているので、zipperであることが判明する。

テンプレート:Exercises

帰結

離散的な状況の中で現れた計算からの規則でどうしてこのようなことが起こるのか、という問いでこのセクションを閉じよう。現在のところ、この答えを知るものはいない。しかし少なくとも、”一度限り”という意味での線形には離散的な概念が存在する。ワンホールコンテキストの穴に $X$ を差し込む関数の主な特徴は、要素が一度限りしか使われないという事実、すなわち線形ということだ。我々は次のような型を持つ差し込み写像として考えることが出来る。

\partial_{X} F X \to (X ⊸ F X)

ここで、 $A ⊸ B$ は、その引数を無視したり複製したりしない線形論理としての線形関数(liner function)を表している。ある意味では、ワンホールコンテキストは関数空間 $X ⊸ F X$ を表現したもので、これは $X \to F X$ に線形近似されていると考えることが出来る。

脚注

↑ Ian Stewart. The true story of how Theseus found his way out of the labyrinth. Scientific American, February 1991, page 137.
↑ テセウスがミノタウロスを倒した後に無事迷宮から脱出するために、恋仲だったアリアドネは糸玉を渡して、戻るときはこの糸を辿るよう助言した。
↑ バッカスとも呼ばれるブドウ酒と酩酊の神。テセウスがナクソス島にアリアドネを捨て去った後、彼女はディオニソスに見初められて妻となった。
↑ Conor Mc Bride. The Derivative of a Regular Type is its Type of One-Hole Contexts. Available online. PDF
↑ この現象は一般的なトライ木ですでに現れる。

参考文献

Zipper on the haskell.org wiki
Generic Zipper and its applications
Zipper-based file server/OS
Scrap Your Zippers: A Generic Zipper for Heterogeneous Types

テンプレート:Haskell navigation テンプレート:Auto category

[1] Ian Stewart. The true story of how Theseus found his way out of the labyrinth. Scientific American, February 1991, page 137.

[2] テセウスがミノタウロスを倒した後に無事迷宮から脱出するために、恋仲だったアリアドネは糸玉を渡して、戻るときはこの糸を辿るよう助言した。

[3] バッカスとも呼ばれるブドウ酒と酩酊の神。テセウスがナクソス島にアリアドネを捨て去った後、彼女はディオニソスに見初められて妻となった。

[4] Conor Mc Bride. The Derivative of a Regular Type is its Type of One-Hole Contexts. Available online. PDF

[5] この現象は一般的なトライ木ですでに現れる。

[1]

[2]

[3]

[4]

[5]

Haskell/Zippers

目次

テセウスとZipper

迷宮

アリアドネのZipper

データ型の微分

機械的な微分

微分を介したZipper

引数の関数に関する微分

Zipper vs コンテキスト

帰結

脚注

参考文献

ナビゲーションメニュー

Haskell/Zippers

テセウスとZipper

迷宮

アリアドネのZipper

データ型の微分

機械的な微分

微分を介したZipper

引数の関数に関する微分

Zipper vs コンテキスト

帰結

脚注

参考文献

ナビゲーション メニュー

検索

ナビゲーションメニュー