ジッパー-タイプから派生

ジッパーは、機能的な純度にもかかわらず、構造を調べて個々の要素を変更できるデータ型表現方法です。 たとえば、要素を使用してリストを先に進むことしかできない場合、ジッパーを使用して特定の要素に「とどまり」、前後に移動して現在の要素を変更できます。
興味深いことに、ある種のジッパーは、その派生物を文字通り取得することで取得できます。

最初に、数学のないリスト用のジッパーを考えてみましょう。
リストを前後に移動する機能が必要です。また、リストを変更するには、現在の値を個別に取得する必要があります。
[0,1,2,3,4,5,6,7,8,9]
|
[0,1,2]3[4,5,6,7,8,9]
これは、ジッパーが現在の要素、後続の値のリスト、および以前の値のリストとして表現できることを示しています。 次に、要素4に移動するには、前の要素のリストに3を追加し、この4を後続の要素のリストから「切り離し」ます。逆も同様です。要素2に移動します。 リストの追加と切り取りは先頭から簡単なので、前の要素のリストを展開する方が便利です(この場合、2はリストの前になります)。 現在のアイテムの交換は簡単です。
[1,2]3[4,5,6,7,8,9]
|->
[1,2,3]4[5,6,7,8,9]
|
[1,2,3]7[5,6,7,8,9]
リストのジッパーを取得するには、最初の要素としてその頭を取り、次の要素として尾を取ります。 さて、ジッパーの適切なリストを取得するには、以前の要素のリスト(もちろん、それを元に戻すことを忘れないでください)を現在の要素と後続の要素のリストに接続する必要があります。

デリバティブを取得するには、まず、その取得に適した形式の型を何らかの形で想像する必要があります。
タイプ0を値のないタイプ、1を値が1つだけのタイプなどとします。
タイプA + Bは、タイプAの値またはタイプBの値のいずれかで表すことができます。 タイプA + Bのすべての可能な値の数は、AおよびBのすべての可能な値の合計になります。Haskellでは、これはタイプEither ab対応します。
タイプA×Bは、両方のタイプの値で同時に表されます。 これはタプルです。

リストは空(単純な値は1に対応)でも、ヘッド(対応するタイプの要素)とテール(リストの残り)を含むこともできます。 上記の表記を使用してこれを記述します。
List A = 1 + A × (List A)
リストのジッパーには、現在の要素、前のリスト、後ろのリストが含まれます。
ZipperList A = A × (List A) × (List A)
リスト型を通常の関数の形に書き直します。そのため、導関数を取るのがより馴染みやすくなります。
f(x) = 1 + x*f(x)
zipper = x*f'(x) -- x -
この場合にのみ、xは数値ではなく[リスト項目]のタイプですが、これはそれ以上の変換には影響しません。
以下は、派生物の機械的なキャプチャであり、学校以来誰もが知っています。
f'(x) = 0 + 1*f(x) + x*f'(x)
f'(x) = f(x) + x*f'(x)
fをgに名前変更
g(x) = f(x) + x*g(x)
右側でg(x)を数回開くと
g(x) = f(x) + x*f(x) + x*x*f(x) + x*x*x*g(x)
次に、f(x)を括弧から外すことができることがわかります
g(x) = f(x) * (1 + x*g(x))
追加の関数h(x)を導入する
h(x) = 1 + x*h(x)
h(x)* f(x)= g(x)
h(x)*f(x) = f(x) + x*f(x)*h(x) = f(x) + x*f(x) + x*x*f(x)*h(x) = g(x)
g(x) = f(x)*h(x)
次にf(x)を見てください;)
f(x) = 1 + x*f(x)
h(x) = 1 + x*h(x)
したがって、最終的にジッパーの形式は
zipper = x*f'(x) = x*f(x)*h(x)
Zipper = A × (List A) × (List A)
つまり まさに私たちが持っていたもの!

確認するには、ツリーのジッパーを見つけて、何が起こるかを考えてみてください。 ツリーは空にすることも、現在の要素と左/右の分岐を持つこともできます。
Tree A = 1 + A × (Tree A) × (Tree A)
f(x) = 1 + x*f(x)^2
f'(x) = 0 + 1*f(x)^2 + x*2*f(x)*f'(x)
f'(x) = f(x)^2 + f'(x)*(2*x*f(x))
-- f' -> g, f(x)^2 -> T, 2*x*f(x) -> S
g(x) = T + S*g(x) = T + S*T + S*S*g(x) = T + S*T + S*S*T + ... = T * (1 + S*g(x))
歴史は繰り返され、表現のみがより複雑になります。 同様に、Tを取り出して、最終的に以下を取得できます。
h(x) = 1 + S*h(x) = List S(x)
g(x) = T(x) * (List S(x))

Zipper = A × (Tree A) × (Tree A) × [A × (Tree A) + A × (Tree A)]
これが何を意味するのか、まだ理解されていない。
最初のAは、明らかに現在のノードの値です。 次の2つ(ツリーA)-このノードに関連する左右のサブツリー。 それらを知っていれば、ツリーを右または左に移動できます。
右側に移動すると、右側のサブツリーからサブツリーの現在の値を取得し、左側のサブツリーを失わないように、リストに書き込みます。 しかし、これに加えて、選択したパス(右または左)をリストで示す必要もあるため、同一のタプルの合計があります。 左の項の値がある場合は、左に進み、右にある場合は右に進みます。 したがって、移動に関するすべての情報が利用可能です。
どのようにして復旧するのですか? 1つ上に進むには、そのノードの要素と、不足しているサブツリー(既にあるもの-現在の位置は上のノードの既知のサブツリー)を知る必要があります。 多くのステップがありますので、リスト全体を保持する必要があります。
Leftの値がリストの先頭(5×rtree)にある場合、値が5のノードから左にステップすることで現在のノードに到達しました。そのノードの右サブツリーにはrtreeがあります。 そして、Right(7×ltree)がリストにある場合、左のrtreeサブツリーを持つノードから右にステップしました。

おそらくコードは理解しやすいでしょう、私はそれを「そのまま」持ってきます、あなたはインタープリターでそれをチェックすることができます。
data Tree a = Empty | Node a ( Tree a ) ( Tree a ) deriving ( Read , Show )

data TreeZipper a = TreeZipper a ( Tree a ) ( Tree a ) [ Either ( a , Tree a ) ( a , Tree a ) ] deriving ( Read , Show )

zipperFromTree Empty = error "Zipper can't point empty trees"
zipperFromTree ( Node val left right ) = TreeZipper val left right []

zipperToTree ( TreeZipper val left right [] ) = Node val left right
zipperToTree zipper = zipperToTree $ moveBack zipper

moveRight ( TreeZipper _ _ Empty _ ) = error "No way!"
moveRight ( TreeZipper val left ( Node nval nleft nright ) trace ) =
TreeZipper nval nleft nright ( ( Right ( val , left ) ) : trace )

moveLeft ( TreeZipper _ Empty _ _ ) = error "No way!"
moveLeft ( TreeZipper val ( Node nval nleft nright ) right trace ) =
TreeZipper nval nleft nright ( ( Left ( val , right ) ) : trace )

moveBack ( TreeZipper val left right [] ) = error "No way!"
moveBack ( TreeZipper val left right ( ( Right ( rval , rleft ) ) : trace ) ) =
TreeZipper rval rleft ( Node val left right ) trace
moveBack ( TreeZipper val left right ( ( Left ( lval , lright ) ) : trace ) ) =
TreeZipper lval ( Node val left right ) lright trace

getNodeValue ( TreeZipper val _ _ _ ) = val
setNodeValue ( TreeZipper _ left right trace ) = TreeZipper val left right trace

-- , , , 10
ghci > zipperFromTree tree
TreeZipper 1 ( Node 2 Empty Empty ) ( Node 3 ( Node 4 Empty Empty ) Empty ) []
ghci > moveRight it
TreeZipper 3 ( Node 4 Empty Empty ) Empty [ Right ( 1 , Node 2 Empty Empty ) ]
ghci > moveLeft it
TreeZipper 4 Empty Empty [ Left ( 3 , Empty ) , Right ( 1 , Node 2 Empty Empty ) ]
ghci > setNodeValue 10 it
TreeZipper 10 Empty Empty [ Left ( 3 , Empty ) , Right ( 1 , Node 2 Empty Empty ) ]
ghci > zipperToTree it
Node 1 ( Node 2 Empty Empty ) ( Node 3 ( Node 10 Empty Empty ) Empty )


通常型の派生型に基づくのは、そのタイプの1ホールコンテキストです

Source: https://habr.com/ru/post/J59552/


All Articles