Haskell/Zippers

テセウスとZipper

迷宮

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

演習
getとputを実装せよ。getの実装の一つは以下のようになる。 get (Passage x _) = x。 具体的な例を得るために、Node (Int,Int)の値を図にして迷路を表示するコードを書け。追加のパラメータ(Int,Int)はノードのデカルト座標系を保持するものとする。

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

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

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

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

演習
プレイヤー位置上の追加データにa -> a型の関数を適用するupdate関数を書け。

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

アリアドネのZipper

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

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

type Zipper a = (Thread a, Node a)

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

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

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

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

branchRight (Fork x l r) = TurnRight x l

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

回廊を真っ直ぐ進む。

演習
turnLeft関数を書け。

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

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)

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

演習
今やzipperの中を移動することができるようになった。プレイヤーの位置の追加データを操作する関数get、put、updateを書け。 zipperはNode aのような具体例に制限されることはないので、全ての木構造のようなデータ型で構成することができる。最初に戻って、以下の二分木のzipperを構築し、糸が取ることの出来る可能な分岐について考えよ。木を探索するときに糸へ何をくっつけるべきだろうか？ data Tree a = Leaf a | Bin (Tree a) (Tree a) 単純なリストも同様にzipperにできる。 data List a = Empty | Cons a (List a) これは何に見えるだろうか？ テセウスの迷宮ゲームを完成させよ。

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

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

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

演習
リストを一つとり、指で真ん中の要素を修正し、リストを下から持ち上げる。結果の木はどのような種類になるだろうか？

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

"Spider-Man: lost in the Web"

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

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

データ型の微分

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

演習
三分木から始めよう。 data Tree a = Leaf a | Node (Tree a) (Tree a) (Tree a) と対応するThread aとZipper aを導出せよ。

機械的な微分

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

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

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

${\mathit {Tree2}}=1+{\mathit {Tree2}}\times {\mathit {Tree2}}$.

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

${\mathit {Branch2}}={\mathit {Tree2}}+{\mathit {Tree2}}\cong 2\times {\mathit {Tree2}}$.

同様に、三分木

${\mathit {Tree3}}=1+{\mathit {Tree3}}\times {\mathit {Tree3}}\times {\mathit {Tree3}}$

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

${\mathit {Branch3}}=3\times {\mathit {Tree3}}\times {\mathit {Tree3}}$

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

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

${\mathit {Tree}}\,X$から$X$型の値を削除するとその位置に穴を残す。

ワンホールコンテキストに$X$を差し込むより抽象的な説明。

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

ワンホールコンテキスト		解説
$(\partial {\mathit {Const_{A}}})\,X$	$=\,0$	$A={\mathit {Const_{A}}}\,X$の中に$X$は存在しない。つまりワンホールコンテキストの型は空でなければならない。
$(\partial {\mathit {Id}})\,X$	$=\,1$	$X={\mathit {Id}}\,X$の中に$X$の要素が一つだけ存在する場所がある。$X$を一つ削除すると、結果は$X$を残さない。削除できる場所が一つだけ存在するから、${\mathit {Id}}\,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 ({\mathit {Id}}\times {\mathit {Id}})\,X=\partial _{X}(X\times X)=1\times X+X\times 1\cong 2\times X$

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

演習
いくつかの規則をポイントワイズスタイルに書き換えよ。例えば、乗法則の左辺は次のようになる。$\partial _{X}(F\,X\times G\,X)=\dots$ ワンホールコンテキストに慣れるために、因数をちょうど$n$回掛けた$X^{n}:=X\times X\times \dots \times X$を微分し、結果と公式が一致すること確かめよ。 もちろん、ワンホールコンテキストは$X$の値を後ろに差し込むことが出来ない場合は役に立たない。5つの規則に対応するplug関数を書け。 2変数の場合の連鎖律を定式化し、それがワンホールコンテキストをもたらすことを証明せよ。これは$(X,Y)$の組における通常の関手を双関手(bifunctor)$F\,X\,Y$として見れば出来るだろう。もちろん、ポイントフリースタイルでの双関手の偏微分のために便利な記法が必要になるかもしれない。

微分を介したZipper

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

${\mathit {Zipper}}_{F}=\mu F\times {\mathit {Context}}_{F}$

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

${\mathit {Context}}_{F}={\mathit {List}}\,(\partial F\,(\mu F))$

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

${\mathit {Context}}_{F}=1+\partial F\,(\mu F)\times {\mathit {Context}}_{F}$

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

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

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

${\mathit {Node}}\,A=\mu X.\,{\mathit {NodeF}}_{A}\,X$

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

${\mathit {NodeF}}_{A}\,X=A+A\times X+A\times X\times X$

言い換えると、

${\mathit {Node}}\,A\cong {\mathit {NodeF}}_{A}\,({\mathit {Node}}\,A)\cong A+A\times {\mathit {Node}}\,A+A\times {\mathit {Node}}\,A\times {\mathit {Node}}\,A$.

微分で読むと、

$\partial _{X}({\mathit {NodeF}}_{A}\,X)\cong A+2\times A\times X$

そして次を得る。

$\partial {\mathit {NodeF}}_{A}\,({\mathit {Node}}\,A)\cong A+2\times A\times {\mathit {Node}}\,A$.

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

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

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

演習
三分木の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 vs コンテキスト

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

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

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

${\mathit {Tree}}\,A=\mu X.\,A+X\times X$.

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

演習
驚いたことに、$\partial _{A}({\mathit {Tree}}\,A)\times A$と${\mathit {Tree}}\,A$のzipperは再び同じ型になることが判明した。計算することは容易いが、なぜこのようになるか理由を与えることができるだろうか？ $\mu F$のzipperは補助変数$Y$導入し、それに関して$\mu X.\,Y\times F\,X$を微分して$Y=1$で再び置き換えて得ることが出来ることを証明せよ。なぜこのようなことができるのだろうか？ zipperとは異なるワンホールコンテキスト$G\,A$型を見つけよ。

帰結

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

$\partial _{X}F\,X\to (X\multimap F\,X)$

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

参考文献

• 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