編集しかし任意の(適切な正規の)データ型のzipperは機械的に導出することもできる。驚くべき事に、「導出(derive)」は文字通りの意味で、zipperはデータ型の導関数(derivative)によって得ることが出来る。McBride[8]によって述べられた。以降のセクションでは、この本当にすばらしい数学の宝石を解明しよう。体系的な構成のため、私たちは型の計算が必要になる。Programmingの章で概説されており、この素材に大きく頼っている。zipperが共通に持っているものと、どのように微分を仄めかしているのかを理解するためにいくつかの例を見ていこう。{Tree2}}}.木を渡り歩くとき、左または右のサブツリーに入ることを繰り返し選択し、アリアドネの糸には入らなかった方のサブツリーをくっつける。したがって、糸の枝は次の型を持つ。{Tree3}}}は次のような型の枝を持つ。{Tree3}}}なぜなら全ての段階で、3つのサブツリーを選択でき、入らなかった二つのサブツリーを格納しなければならない。context)の概念だ。{Tree}}\,X}型のようなものを想像しよう。X}型の要素を構造から一つ削除して、なんらかの方法でその位置を空とマークした場合、「マークした穴(hole)」とデータ構造を得られる。{Tree}}\,X}が戻ってくる。「穴」は、位置の識別、焦点の役割を果たす。図でこれを説明しよう。X}型の値を削除するとその位置に穴を残す。X}を差し込むより抽象的な説明。我々の興味はワンホールコンテキストに与える型、すなわちHaskellでこれをどのように表現するかだ。問題は焦点を効率よくマークするにはどうしたらいいだろうか。我々が見るように、型の構造に関する帰納法によってワンホールコンテキストの表現を見つけだし、効率的なデータ型につながるワンホールコンテキストを自動的に取得したいと思う[9]。F}という表記法を選択する理由は既におわかりと思うが、ワンホールコンテキストの加法、乗法、合成の法則は、まさに微分におけるライプニッツ則である。ワンホールコンテキストの型は空でなければならない。X}の要素が一つだけ存在する場所がある。{Id}}\,X}はまさにワンホールコンテキストの一つである。したがって、ワンホールコンテキストの型は単一の要素からなるシングルトン型である。G}二つの型の組のワンホールコンテキストは、第一または、第二成分のいずれかが穴である。rule):合成の穴は囲んでいる構造に穴を開け、そこに密閉構造を当てはめることによって生じる。}という構文は異なる関手を表している。一つの引数を持つ型関数の種(kind)である。_{X}}という表記法もある。添え字は微分したい変数を表している。_{X}(F\,X)}である。例を挙げると以下のようになる。}はポイントフリースタイルである。演習いくつかの規則をポイントワイズスタイルに書き換えよ。乗法則の左辺は次のようになる。X}を微分し、結果と公式が一致すること確かめよ。X}の値を後ろに差し込むことが出来ない場合は役に立たない。5つの規則に対応するplug関数を書け。2変数の場合の連鎖律を定式化し、それがワンホールコンテキストをもたらすことを証明せよ。F\,X\,Y}として見れば出来るだろう。ポイントフリースタイルでの双関手の偏微分のために便利な記法が必要になるかもしれない。X.\,F\,X}のzipperを構築することができる。functor)である。Zipperは特定のサブツリーに焦点を移す。F}型のサブ構造である。前章のように、焦点を向けたい場所のサブツリーと糸、これはサブツリーが格納されているコンテキストだが、この二つによって表現することが出来る。F)}と一緒に回収される。このコンテキストの穴は選択したサブツリーから削除しながら帰ってくる。{Context}}_{F}}具体的な計算過程がどのようになるかを説明するために、体系的に迷宮データ型のzipperを構築しよう。a)この再帰型は次のような不動点である。{NodeF}}_{A}\,X}この関手は次のようなものだ。三分木のzipperを微分の観点でやり直せ。g(x)のような式を完全に解くことが可能だ。x^2は2x^2を与えて解くと、4つのタプルの2ホールコンテキストである。導関数は次のようなものである。コンテキスト編集しかし一般的には、zipperとワンホールコンテキストは異なるもので表される。zipperは勝手なサブツリーの焦点である一方、ワンホールコンテキストは型構築子の引数にだけ焦点を当てることができる。次のデータ型を例に取ろう。a)ここで不動点は次の通りである。{Tree}}\,A}のワンホールコンテキストの穴はLeafだけに焦点を当てるだろう。A}型の要素が存在しているからだ。A}で飾られているので、zipperであることが判明する。{Tree}}\,A}のzipperは再び同じ型になることが判明した。Y=1}で再び置き換えて得ることが出来ることを証明せよ。状況の中で現れた計算からの規則でどうしてこのようなことが起こるのか、という問いでこのセクションを閉じよう。現在のところ、この答えを知るものはいない。少なくとも、”一度限り”という意味での線形には離散的な概念が存在する。X}を差し込む関数の主な特徴は、要素が一度限りしか使われないという事実、すなわち線形ということだ。我々は次のような型を持つ差し込み写像として考えることが出来る。function)を表している。F\,X}に線形近似されていると考えることが出来る。テセウスがミノタウロスを倒した後に無事迷宮から脱出するために、恋仲だったアリアドネは糸玉を渡して、戻るときはこの糸を辿るよう助言した。Huetによる造語zipperの概念は、それらに関連づけられている余分なデータが存在しない場合でも、サブツリー全体を置き換えることができる事に注意しよう。我々の迷宮の場合これは無関係だが、データ型の微分のセクションでこの話題を取り上げる。最上位ノードから2番目のノードや他のノードも、殆どは同様にトップから離れた分の定数時間で行える。ノードのデータを変更するのではなく、最上位ノード以下のノードが影響を受けてデータ構造全体を変更する場合でも、一定の償却定数時間で達成することができることに注意。二進表現の数をインクリメントするとしよう。111..11から1000..00を得るためには全ての数字に触れなければならいということだが、にもかかわらずインクリメント関数は一定の償却時間で実行される。バッカスとも呼ばれるブドウ酒と酩酊の神。テセウスがナクソス島にアリアドネを捨て去った後、彼女はディオニソスに見初められて妻となった。この現象は一般的なトライ木ですでに現れる。14:05言語このページに他の言語版はありません。4.0のもとで利用可能です。利用規約デスクトップ。