Haskell/Zippers
テセウスとZipper

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

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

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

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

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

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

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

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

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

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

テセウスが、彼が念頭に置いていた迷宮の表現をアリアドネに語ると、彼女はすぐさまアドバイスをくれた。 "あなたが必要なのはzipperね。" 「えっ?私の"社会の窓"に何か問題があるのかい?」 "何も。このデータ構造はGérard Huetによって最初に発表されたわ。" 「へえ」 "より正確には、リストや二分木のようなツリー型データ構造に対して、純粋に関数的な方法で焦点を当てたり、データ構造内のサブツリーの一点を指して、定数時間で更新や参照を可能にする方法ね。。私たちの場合では、プレイヤーの位置に焦点を当てましょう。" 「高速な更新が必要なことはわかっているけど、どのようにコーディングしたらいいんだい?」 "せっかちね、コーディングによって問題を解決することはできないわ。あなたの思考だけが問題を解決できるの。 純粋関数型のデータ構造で定数時間で更新できるのは最上位ノードだけね。だから焦点は必ず最上部にする必要があるわ。現在、あなたの迷宮の最上位ノードは常に入り口だけど、あなたが以前思いついたサブ迷宮で置き換えるアイディアはプレイヤーの位置が最上位ノードであることを保証します。" 「けど、問題はどうやって戻ればいいんだい?サブ迷宮はプレイヤーがどう分岐してきたかが全て失われてしまう。」 "えーと、サブ迷宮サブ迷宮を失わないために糸が使えるわ。" アリアドネはテセウスが困惑するのを満喫できましたが、彼が既にアリアドネの糸を使用したことに不満を言う隙を与えず、 "鍵は糸にサブ迷宮をくっつけること、実際にはまったく失われないようにね。この意図は、糸と現在のサブ迷宮をお互いに補完させて迷宮全体とするの。サブ迷宮は'現在'プレイヤーが立っている場所を意味します。zipperは単純に糸と現在のサブ迷宮で構成されています。"
テセウスとZipper

テセウスは何も言わなかった。 "また、現在のサブ迷宮が置かれている糸のコンテキストを表示することができるわ。ところで、Threadはサブ迷宮を格納するためにaという追加パラメータを取る必要があるわね。糸はまだ単純な分岐のリストだけど、分岐は以前とは異なっているわ。"
テセウスとZipper

"もっとも重要なのは、TurnLeftとTurnRightはサブ迷宮をくっつけるということ。プレイヤーが右へ曲がる時、TurnRightと今は辿れない左の分岐を取り付けて糸を拡張し、それが失われないようにしなければ。" テセウスが遮った、「待ってくれ、turnRightのような関数をどのように実装したらいいんだ?TurnRightの最初の引数の型aは何にすればいいんだ?あぁ、わかった。失われてしまう分岐はくっつける必要はないが、Forkの追加データも同様に失われてしまう。けど、予備を使って新しい分岐を生成できる。
テセウスとZipper

「何らかの方法で既存の糸を拡張する必要があるな。」 "確かに。第二のポイントは糸に新しい分岐を追加するときは後ろから入れていくことよ。伸ばすときは新しい分岐をリストの前面に置く。戻るには最初の要素を削除すればいいわね。" なるほど、これは伸ばすときと戻るときだけ定数時間になって、以前のバージョンのような長さに比例した時間がかかることはないわけだ。だからturnRightの最終バージョンは...」
テセウスとZipper

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

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

「もし糸が空なら、まだ迷宮の入り口で戻ることはできない。それ以外の場合は、糸を巻かなければならない。糸につなげたおかげで、実際に来た道からサブ迷宮を再構築することができる。」 アリアドネが言った。"部分テストは、左側のx、l、rのような各束縛変数が右辺に一度だけ現れているか確認するためであることに注意して。だから、zipperを上下に歩くとき、糸と現在のサブ迷宮を再配布するだけでいいわ。"
テセウスとZipper

わかったぞ!これは一部をアリアドネコンサルティングに売却したとしても、Ancient Geeks株式会社が優先すべき、テセウスが求めていた解決策だった。しかし一つだけ疑問が残った。 「なんでzipperと呼ばれているんだ?」 "そうね、'アリアドネの真珠のネックレス'と呼ぶべきでしょうね。でもたいていの場合で、zipperと呼ばれるのは衣服のチャックの開いている部分を糸、閉じている部分をサブ迷宮とするアナロジーね。データ構造内の移動がチャックを上げ下げするのに似ているから。" 「アリアドネの真珠のネックレス、ね...。」彼は軽蔑を向けた。「君の糸に助けられたよ。クレタ島の時のように」 "あのときの糸のアイディアはあなた次第で、"彼女は答えた。 「フン、もう糸は必要ない。」 彼の驚いたことに、彼女は同意して、"そうね、確かにもう糸は必要ないわね。別の視点では文字通り指差した木の焦点を掴んで下から持ち上げることね。焦点が上になって他の全ての枝は垂れ下がる。結果、木に適合する代数的データ型はzipperになる可能性が最も高いわね。"
テセウスとZipper

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

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

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

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

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

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

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

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

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

同様に、三分木
データ型の微分

は次のような型の枝を持つ。
データ型の微分

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

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

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

もちろん、穴を埋める関数plugの型は ( ∂ F X ) × X → F X {\displaystyle (\partial F\,X)\times X\to F\,X} を持つ。
データ型の微分

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

である。例を挙げると以下のようになる。
データ型の微分

もちろん、 ∂ X {\displaystyle \partial _{X}} は単にポイントワイズで、 ∂ {\displaystyle \partial } はポイントフリースタイルである。
データ型の微分

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

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

を得る。または同じ事だが
データ型の微分

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

この再帰型は次のような不動点である。
データ型の微分

この関手は次のようなものだ。
データ型の微分

言い換えると、
データ型の微分

微分で読むと、
データ型の微分

そして次を得る。
データ型の微分

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

期待通り両者が全く同じものであることがわかるだろう!
データ型の微分

ワンホールコンテキストの型を見つけるときの一つは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とワンホールコンテキストは異なるもので表される。zipperは勝手なサブツリーの焦点である一方、ワンホールコンテキストは型構築子の引数にだけ焦点を当てることができる。次のデータ型を例に取ろう。
データ型の微分

ここで不動点は次の通りである。
データ型の微分

zipperはサブツリーのトップであるBinやLeafに焦点を当てることが出来るが、 T r e e A {\displaystyle {\mathit {Tree}}\,A} のワンホールコンテキストの穴はLeafだけに焦点を当てるだろう。なぜなら、これは A {\displaystyle A} 型の要素が存在しているからだ。 N o d e A {\displaystyle {\mathit {Node}}\,A} の導関数はサブツリーの全てのトップが常に A {\displaystyle A} で飾られているので、zipperであることが判明する。
データ型の微分

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

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