[解決済み] ジッパーコモナド、一般的

質問

任意のコンテナ型が与えられると、（要素に焦点を当てた）ジッパーを形成し、この構造がコモナドであることを知ることができます。このことは、最近 Stack Overflow の別の質問 において、次のような型について素晴らしく詳細に検討されました。

data Bin a = Branch (Bin a) a (Bin a) | Leaf a deriving Functor

を次のファスナーで囲みます。

data Dir = L | R
data Step a = Step a Dir (Bin a)   deriving Functor
data Zip  a = Zip [Step a] (Bin a) deriving Functor
instance Comonad Zip where ...

というのは Zip は Comonad であるが、そのインスタンスの構築は少し毛むくじゃらである。とはいえ Zip から完全に機械的に派生させることができます。 Tree であり、（私は）この方法で派生した型は、自動的に Comonad であり、これらの型とその同型を一般的かつ自動的に構築することができるケースであるべきだと感じています。

ジッパー構築の一般性を達成するための1つの方法は、次のクラスと型ファミリーを使用することです。

data Zipper t a = Zipper { diff :: D t a, here :: a }

deriving instance Diff t => Functor (Zipper t)

class (Functor t, Functor (D t)) => Diff t where
  data D t :: * -> *
  inTo  :: t a -> t (Zipper t a)
  outOf :: Zipper t a -> t a

このクラスはHaskell CafeのスレッドやConal Elliottのブログで(多かれ少なかれ)紹介されているものです。このクラスは様々なコア代数型に対してインスタンス化することができ、ADTの導関数について話すための一般的なフレームワークを提供します。

ですから、最終的に私の質問は、私たちが

instance Diff t => Comonad (Zipper t) where ...

は、上記の特定の Comonad インスタンスを包含するために使用される可能性があります。

instance Diff Bin where
  data D Bin a = DBin { context :: [Step a], descend :: Maybe (Bin a, Bin a) }
  ...

残念ながら、私はそのようなインスタンスを書くことに成功していません。このインスタンスは inTo / outOf のシグネチャで十分ですか？型を制約するために何か他に必要なものはありますか？このインスタンスは可能なのでしょうか？

どのように解決するのですか？

チキチキバンバン」に出てくる子供だましがお菓子やおもちゃで子供を誘い込むように、物理学部の勧誘員はシャボン玉やブーメランでごまかすのが好きですが、ドアが閉まると、「さあ、子供たち、偏微分について学ぶ時間です！」です。私もです。警告しなかったとは言わせないぞ。

ここでもう一つ警告があります。 {-# LANGUAGE KitchenSink #-} が必要であり、むしろ

{-# LANGUAGE TypeFamilies, FlexibleContexts, TupleSections, GADTs, DataKinds,
    TypeOperators, FlexibleInstances, RankNTypes, ScopedTypeVariables,
    StandaloneDeriving, UndecidableInstances #-}

を順不同で表示します。

微分可能なファンクタは comonadic zippers を与える

微分可能なファンクターとは何でしょうか？

class (Functor f, Functor (DF f)) => Diff1 f where
  type DF f :: * -> *
  upF      ::  ZF f x  ->  f x
  downF    ::  f x     ->  f (ZF f x)
  aroundF  ::  ZF f x  ->  ZF f (ZF f x)

data ZF f x = (:<-:) {cxF :: DF f x, elF :: x}

これはファンクタであり、そのファンクタは導関数を持っています。この導関数は 要素 . ジッパータイプ ZF f x は、1つの穴のコンテキストと穴の中の要素のペアを表します。

の操作は Diff1 の操作は、ジッパーでできるナビゲーションの種類を記述しています（quot;leftward" と "rightward" の概念はありません、これについては私の ピエロとジョーカー の論文を参照してください)。私たちは、要素をその穴に詰めることによって構造を再構築しながら、quot;upward"へと進むことができます。私たちは、「下へ下へ」と、与えられた構造の中で要素を訪問するあらゆる方法を見つけ、すべての要素をその文脈で飾ります。また、「迂回」することもできます。 既存のジッパーを取り出し、各要素をそのコンテキストで装飾することで、再フォーカスする方法 (および現在のフォーカスを維持する方法) をすべて見つけることができるのです。

では aroundF を思い起こす人もいるかもしれません。

class Functor c => Comonad c where
  extract    :: c x -> x
  duplicate  :: c x -> c (c x)

と、思い起こされるのは当然でしょう 私たちは、ホップアンドスキップで、持っています。

instance Diff1 f => Functor (ZF f) where
  fmap f (df :<-: x) = fmap f df :<-: f x

instance Diff1 f => Comonad (ZF f) where
  extract    = elF
  duplicate  = aroundF

と主張し

extract . duplicate == id
fmap extract . duplicate == id
duplicate . duplicate == fmap duplicate . duplicate

また、以下のようなことも必要です。

fmap extract (downF xs) == xs              -- downF decorates the element in position
fmap upF (downF xs) = fmap (const xs) xs   -- downF gives the correct context

多項式ファンクタは微分可能

定数 ファンクタは微分可能です。

data KF a x = KF a
instance Functor (KF a) where
  fmap f (KF a) = KF a

instance Diff1 (KF a) where
  type DF (KF a) = KF Void
  upF (KF w :<-: _) = absurd w
  downF (KF a) = KF a
  aroundF (KF w :<-: _) = absurd w

要素を置く場所がないので、文脈を形成することができない。行き場がない upF または downF から、我々は簡単に行く方法のすべてのnoneを見つける。 downF .

は アイデンティティ ファンクタは微分可能である。

data IF x = IF x
instance Functor IF where
  fmap f (IF x) = IF (f x)

instance Diff1 IF where
  type DF IF = KF ()
  upF (KF () :<-: x) = IF x
  downF (IF x) = IF (KF () :<-: x)
  aroundF z@(KF () :<-: x) = KF () :<-: z

つまらない文脈で1つの要素がある。 downF がそれを見つけます。 upF はそれをリパックし aroundF はじっとしているしかない。

<強い 和 は微分可能性を保持する。

data (f :+: g) x = LF (f x) | RF (g x)
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap h (LF f) = LF (fmap h f)
  fmap h (RF g) = RF (fmap h g)

instance (Diff1 f, Diff1 g) => Diff1 (f :+: g) where
  type DF (f :+: g) = DF f :+: DF g
  upF (LF f' :<-: x) = LF (upF (f' :<-: x))
  upF (RF g' :<-: x) = RF (upF (g' :<-: x))

その他の部分については、もう少し手がかかります。行くには downF に行くには downF のように、タグ付けされたコンポーネントの中に入り、その結果生じるジッパーを修正して、コンテキストの中にタグを表示します。

  downF (LF f) = LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) (downF f))
  downF (RF g) = RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) (downF g))

行くには aroundF にするためには、タグを除去し、タグのないものをどのように迂回するかを考え、その結果生じるすべてのジッパーでタグを復元します。着目している要素 x は、そのジッパー全体によって置き換えられます。 z .

  aroundF z@(LF f' :<-: (x :: x)) =
    LF (fmap (\ (f' :<-: x) -> LF f' :<-: x) . cxF $ aroundF (f' :<-: x :: ZF f x))
    :<-: z
  aroundF z@(RF g' :<-: (x :: x)) =
    RF (fmap (\ (g' :<-: x) -> RF g' :<-: x) . cxF $ aroundF (g' :<-: x :: ZF g x))
    :<-: z

なお、私は ScopedTypeVariables への再帰的な呼び出しを曖昧にしないために aroundF . 型関数として DF は帰納的でないため f' :: D f x が強制されるには十分ではありません。 f' :<-: x :: Z f x .

製品紹介 は微分可能性を保持する。

data (f :*: g) x = f x :*: g x
instance (Functor f, Functor g) => Functor (f :*: g) where
  fmap h (f :*: g) = fmap h f :*: fmap h g

ペアの要素に焦点を合わせるには、左側に焦点を合わせて右側は放っておくか、その逆をすればいいのです。ライプニッツの有名な積の法則は、単純な空間的直観に対応しているのです!

instance (Diff1 f, Diff1 g) => Diff1 (f :*: g) where
  type DF (f :*: g) = (DF f :*: g) :+: (f :*: DF g)
  upF (LF (f' :*: g) :<-: x) = upF (f' :<-: x) :*: g
  upF (RF (f :*: g') :<-: x) = f :*: upF (g' :<-: x)

今すぐ downF は、ジッパーのコンテキストをタグで修正するだけでなく（どちらに行ったかを示すため）、手つかずの他のコンポーネントでも修正しなければならないことを除けば、sums に対して行った方法と同じように動作します。

  downF (f :*: g)
    =    fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f)
    :*:  fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g)

しかし aroundF は笑いの塊のようなものです。現在どちらを訪れても、二者択一である。

1. 移動する aroundF をその側に移動します。
2. 移動 upF をその側に出して downF を反対側へ。

それぞれのケースで、下部構造のための操作を利用し、そして文脈を修正することが必要です。

  aroundF z@(LF (f' :*: g) :<-: (x :: x)) =
    LF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x)
          (cxF $ aroundF (f' :<-: x :: ZF f x))
        :*: fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x) (downF g))
    :<-: z
    where f = upF (f' :<-: x)
  aroundF z@(RF (f :*: g') :<-: (x :: x)) =
    RF (fmap (\ (f' :<-: x) -> LF (f' :*: g) :<-: x) (downF f) :*:
        fmap (\ (g' :<-: x) -> RF (f :*: g') :<-: x)
          (cxF $ aroundF (g' :<-: x :: ZF g x)))
    :<-: z
    where g = upF (g' :<-: x)

ふっふっふっふっ。多項式はすべて微分可能であり、したがってコモナドを与える。

ふむ。ちょっと抽象的ですね。そこで、私は deriving Show を可能な限り追加し、さらに

deriving instance (Show (DF f x), Show x) => Show (ZF f x)

で、以下のようなインタラクションが可能でした（手作業で整頓しています）。

> downF (IF 1 :*: IF 2)
IF (LF (KF () :*: IF 2) :<-: 1) :*: IF (RF (IF 1 :*: KF ()) :<-: 2)

> fmap aroundF it
IF  (LF (KF () :*: IF (RF (IF 1 :*: KF ()) :<-: 2)) :<-: (LF (KF () :*: IF 2) :<-: 1))
:*:
IF  (RF (IF (LF (KF () :*: IF 2) :<-: 1) :*: KF ()) :<-: (RF (IF 1 :*: KF ()) :<-: 2))

運動 微分可能なファンクタの合成は、微分可能であることを示せ。 鎖の法則 .

スウィート! もう家に帰れるの？もちろんダメですよ。私たちはまだ、どんな 再帰的 構造を区別していません。

二分木から再帰的ファンクタを作る

A Bifunctor は、データ型汎用プログラミングに関する既存の文献（Patrik Jansson と Johan Jeuring による著作、または Jeremy Gibbons による優れた講義ノート参照）が長々と説明しているように、2 種類の部分構造に対応する 2 つのパラメータを持つ型コンストラクタです。私たちは、両方を "map"することができるはずです。

class Bifunctor b where
  bimap :: (x -> x') -> (y -> y') -> b x y -> b x' y'

を使うことができます。 Bifunctor を使うことで，再帰的コンテナのノード構造を与えることができます．各ノードには サブノード と 要素 . これらは単に2種類の部分構造である可能性があります。

data Mu b y = In (b (Mu b y) y)

ほらね。再帰的な結び目は b の最初の引数を結び、パラメータ y をその第二引数に残す。したがって、一度だけ、すべての

instance Bifunctor b => Functor (Mu b) where
  fmap f (In b) = In (bimap (fmap f) f b)

これを使うには、キットの Bifunctor インスタンスが必要です。

ビファンクタ・キット

定数 は二分法である。

newtype K a x y = K a

instance Bifunctor (K a) where
  bimap f g (K a) = K a

識別子が短いので、私がこの部分を最初に書いたことがわかりますが、コードが長くなるので、それは良いことです。

変数 は2分法である。

どちらかのパラメータに対応する二分木が必要なので、それを区別するためのデータ型を作り、適当なGADTを定義しました。

data Var = X | Y

data V :: Var -> * -> * -> * where
  XX :: x -> V X x y
  YY :: y -> V Y x y

これは V X x y のコピーです。 x と V Y x y のコピーです。 y . したがって

instance Bifunctor (V v) where
  bimap f g (XX x) = XX (f x)
  bimap f g (YY y) = YY (g y)

合計 と 製品 は二分木である。

data (:++:) f g x y = L (f x y) | R (g x y) deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :++: c) where
  bimap f g (L b) = L (bimap f g b)
  bimap f g (R b) = R (bimap f g b)

data (:**:) f g x y = f x y :**: g x y deriving Show

instance (Bifunctor b, Bifunctor c) => Bifunctor (b :**: c) where
  bimap f g (b :**: c) = bimap f g b :**: bimap f g c

ここまでは定型的なものですが、次のような定義ができるようになりました。

List = Mu (K () :++: (V Y :**: V X))

Bin = Mu (V Y :**: (K () :++: (V X :**: V X)))

もし、これらの型を実際のデータに使い、Georges Seuratのpointillisteの伝統の中で盲目にならないようにしたいのであれば <項目 パターン同義語 .

しかし、ジッパーはどうでしょう？どのようにそれを示そうか。 Mu b が微分可能であることをどうやって示そうか。私たちは、次のことを示す必要があります。 b が微分可能なのは で微分可能である。 変数で微分可能です。Clang! 偏微分について学ぶときが来たのです。

二分木の偏微分

2つの変数があるので、あるときはまとめて、あるときは個別に話すことができるようにする必要があります。私たちは単項式を必要とします。

data Vary :: Var -> * where
  VX :: Vary X
  VY :: Vary Y

さて、二分率が各変数で偏導関数を持つとはどういうことか、それに対応するジッパーの概念を述べます。

class (Bifunctor b, Bifunctor (D b X), Bifunctor (D b Y)) => Diff2 b where
  type D b (v :: Var) :: * -> * -> *
  up      :: Vary v -> Z b v x y -> b x y
  down    :: b x y -> b (Z b X x y) (Z b Y x y)
  around  :: Vary v -> Z b v x y -> Z b v (Z b X x y) (Z b Y x y)

data Z b v x y = (:<-) {cxZ :: D b v x y, elZ :: V v x y}

これは D の操作では、どの変数をターゲットにするかを知る必要があります。対応するジッパー Z b v はどの変数 v がフォーカスされていなければなりません。コンテキストでデコレートする場合、このように x -要素に X -コンテクストと y -要素を持つ Y -コンテキストに置き換えます。しかし、それ以外は同じ話です。

まず、2分木が微分可能であることを示し、次に Diff2 b を確立することができます。 Diff1 (Mu b) .

バイファンクターキットを微分する

この部分は、役に立つというよりも、むしろ厄介なことだと思います。ご遠慮なく読み飛ばしてください。

定数は前と同じです。

instance Diff2 (K a) where
  type D (K a) v = K Void
  up _ (K q :<- _) = absurd q
  down (K a) = K a
  around _ (K q :<- _) = absurd q

この際、型レベルのクロネッカーデルタの理論を展開するのは命が惜しいので、変数だけ別扱いしました。

instance Diff2 (V X) where
  type D (V X) X = K ()
  type D (V X) Y = K Void
  up VX (K () :<- XX x)  = XX x
  up VY (K q :<- _)      = absurd q
  down (XX x) = XX (K () :<- XX x)
  around VX z@(K () :<- XX x)  = K () :<- XX z
  around VY (K q :<- _)        = absurd q

instance Diff2 (V Y) where
  type D (V Y) X = K Void
  type D (V Y) Y = K ()
  up VX (K q :<- _)      = absurd q
  up VY (K () :<- YY y)  = YY y
  down (YY y) = YY (K () :<- YY y)
  around VX (K q :<- _)        = absurd q
  around VY z@(K () :<- YY y)  = K () :<- YY z

構造的なケースでは、変数を一律に扱えるようにするヘルパーを導入するのが便利だと思いました。

vV :: Vary v -> Z b v x y -> V v (Z b X x y) (Z b Y x y)
vV VX z = XX z
vV VY z = YY z

のために必要な retagging" を容易にするためのガジェットを構築しました。 down と around . (もちろん、作業しながら必要なガジェットを確認しました）。

zimap :: (Bifunctor c) => (forall v. Vary v -> D b v x y -> D b' v x y) ->
         c (Z b X x y) (Z b Y x y) -> c (Z b' X x y) (Z b' Y x y)
zimap f = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)

dzimap :: (Bifunctor (D c X), Bifunctor (D c Y)) =>
         (forall v. Vary v -> D b v x y -> D b' v x y) ->
         Vary v -> Z c v (Z b X x y) (Z b Y x y) -> D c v (Z b' X x y) (Z b' Y x y)
dzimap f VX (d :<- _) = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)
  d
dzimap f VY (d :<- _) = bimap
  (\ (d :<- XX x) -> f VX d :<- XX x)
  (\ (d :<- YY y) -> f VY d :<- YY y)
  d

これで準備は整ったので、あとは細部を詰めていくだけです。合計は簡単です。

instance (Diff2 b, Diff2 c) => Diff2 (b :++: c) where
  type D (b :++: c) v = D b v :++: D c v
  up v (L b' :<- vv) = L (up v (b' :<- vv))
  down (L b) = L (zimap (const L) (down b))
  down (R c) = R (zimap (const R) (down c))
  around v z@(L b' :<- vv :: Z (b :++: c) v x y)
    = L (dzimap (const L) v ba) :<- vV v z
    where ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R c' :<- vv :: Z (b :++: c) v x y)
    = R (dzimap (const R) v ca) :<- vV v z
    where ca = around v (c' :<- vv :: Z c v x y)

製品は大変な作業です。だから私はエンジニアではなく数学者なのです。

instance (Diff2 b, Diff2 c) => Diff2 (b :**: c) where
  type D (b :**: c) v = (D b v :**: c) :++: (b :**: D c v)
  up v (L (b' :**: c) :<- vv) = up v (b' :<- vv) :**: c
  up v (R (b :**: c') :<- vv) = b :**: up v (c' :<- vv)
  down (b :**: c) =
    zimap (const (L . (:**: c))) (down b) :**: zimap (const (R . (b :**:))) (down c)
  around v z@(L (b' :**: c) :<- vv :: Z (b :**: c) v x y)
    = L (dzimap (const (L . (:**: c))) v ba :**:
        zimap (const (R . (b :**:))) (down c))
      :<- vV v z where
      b = up v (b' :<- vv :: Z b v x y)
      ba = around v (b' :<- vv :: Z b v x y)
  around v z@(R (b :**: c') :<- vv :: Z (b :**: c) v x y)
    = R (zimap (const (L . (:**: c))) (down b):**:
        dzimap (const (R . (b :**:))) v ca)
      :<- vV v z where
      c = up v (c' :<- vv :: Z c v x y)
      ca = around v (c' :<- vv :: Z c v x y)

概念的には以前と同じですが、より官僚的です。私は、これらをタイプホール以前の技術を使って、次のように作りました。 undefined をスタブとして使用し、タイプチェッカーから有用なヒントを得たい場所 (いつでも) には意図的なタイプエラーを導入しました。あなたも Haskell でさえ、ビデオゲームのような型チェックを体験することができます。

再帰的コンテナのためのサブノードジッパー

の偏導関数は b に関して X は、ノードの一歩内側にあるサブノードを見つける方法を教えてくれるので、従来のジッパーの概念を得ることができます。

data MuZpr b y = MuZpr
  {  aboveMu  :: [D b X (Mu b y) y]
  ,  hereMu   :: Mu b y
  }

を繰り返し差し込むことで、ルートまでズームアップすることができます。 X の位置に繰り返し差し込むことで、ルートまでズームアップすることができます。

muUp :: Diff2 b => MuZpr b y -> Mu b y
muUp (MuZpr {aboveMu = [], hereMu = t}) = t
muUp (MuZpr {aboveMu = (dX : dXs), hereMu = t}) =
  muUp (MuZpr {aboveMu = dXs, hereMu = In (up VX (dX :<- XX t))})

しかし、私たちは 要素 -zippersが必要です。

二分木のfixpointsのための要素ジッパー

各要素はどこかノードの中にあります。そのノードは X -の誘導体の下にあります。しかし、そのノードの中の要素の位置は、そのノードにある Y -の誘導体である。私たちは

data MuCx b y = MuCx
  {  aboveY  :: [D b X (Mu b y) y]
  ,  belowY  :: D b Y (Mu b y) y
  }

instance Diff2 b => Functor (MuCx b) where
  fmap f (MuCx { aboveY = dXs, belowY = dY }) = MuCx
    {  aboveY  = map (bimap (fmap f) f) dXs
    ,  belowY  = bimap (fmap f) f dY
    }

大胆にも、私は主張する

instance Diff2 b => Diff1 (Mu b) where
  type DF (Mu b) = MuCx b

が、操作を開発する前に、いくつかの断片が必要です。

ファンクタージッパーとバイファンクタージッパーの間で、次のようにデータを交換することができますね。

zAboveY :: ZF (Mu b) y -> [D b X (Mu b y) y]  -- the stack of `X`-derivatives above me
zAboveY (d :<-: y) = aboveY d

zZipY :: ZF (Mu b) y -> Z b Y (Mu b y) y      -- the `Y`-zipper where I am
zZipY (d :<-: y) = belowY d :<- YY y

これで定義させるのは十分です。

  upF z  = muUp (MuZpr {aboveMu = zAboveY z, hereMu = In (up VY (zZipY z))})

つまり、まず要素のあるノードを組み立て直し、エレメントジッパーをサブノードジッパーにし、上記のようにずっとズームアウトすることで上に行くのです。

次に、次のように

  downF  = yOnDown []

というヘルパー関数を定義し、空のスタックから順に下っていきます。 down を繰り返すヘルパー関数を定義します。

yOnDown :: Diff2 b => [D b X (Mu b y) y] -> Mu b y -> Mu b (ZF (Mu b) y)
yOnDown dXs (In b) = In (contextualize dXs (down b))

今すぐ down b は私たちをノードの内部に取り込むだけです。私たちが必要とするジッパーは、ノードのコンテキストも運ばなければなりません。それが contextualise を行います。

contextualize :: (Bifunctor c, Diff2 b) =>
  [D b X (Mu b y) y] ->
  c (Z b X (Mu b y) y) (Z b Y (Mu b y) y) ->
  c (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)
contextualize dXs = bimap
  (\ (dX :<- XX t) -> yOnDown (dX : dXs) t)
  (\ (dY :<- YY y) -> MuCx {aboveY = dXs, belowY = dY} :<-: y)

すべての Y -の位置で、エレメントジッパーを与えなければなりませんので、コンテキスト全体を知っておくとよいでしょう。 dXs と同様に、ルートに戻って dY で、その要素がそのノードにどのように配置されるかを記述しています。それぞれの X -の位置に応じて、探索するサブツリーがさらに存在するので、スタックを大きくしていきます。

あとはフォーカスを移動させるだけです。このまま動かないかもしれませんし、今いるところから下がるかもしれませんし、上がるかもしれませんし、上がってから他の道を通るかもしれません。さあ、どうぞ。

  aroundF z@(MuCx {aboveY = dXs, belowY = dY} :<-: _) = MuCx
    {  aboveY = yOnUp dXs (In (up VY (zZipY z)))
    ,  belowY = contextualize dXs (cxZ $ around VY (zZipY z))
    }  :<-: z

これまでと同様に、既存の要素はそのジッパー全体で置き換えられます。の場合は belowY の部分については、既存のノードの中で他にどこに行けるかを探します。 Y -の位置か、あるいはさらに X -サブノードを探索する必要があります。 contextualise を追加しました。については aboveY の部分については、私たちはこの部分を X -の部分から派生したもので、訪問していたノードを再び組み立てた後、スタックを遡っていく必要があります。

yOnUp :: Diff2 b => [D b X (Mu b y) y] -> Mu b y ->
         [D b X (Mu b (ZF (Mu b) y)) (ZF (Mu b) y)]
yOnUp [] t = []
yOnUp (dX : dXs) (t :: Mu b y)
  =  contextualize dXs (cxZ $ around VX (dX :<- XX t))
  :  yOnUp dXs (In (up VX (dX :<- XX t)))

各ステップで、どこか別の場所を向くか、その場所が around である別の場所に行くか、あるいは上り続けるかです。

で終わりです。法則の正式な証明はしていませんが、構造をクロールする際に、オペレーションが注意深くコンテキストを正しく維持しているように見えますね。

私たちは何を学んだのでしょうか？

微分可能性は、thing-in-its-contextの概念を誘発し、以下のようなコモナド構造を誘発する。 extract がものを与え duplicate は文脈を探索し、文脈を形成する他のものを探します。ノードに対して適切な差分構造があれば、木全体に対して差分構造を開発することができます。

それと、型構成子の個々のアリティを別々に扱うのは、あからさまに恐ろしいことです。より良い方法は、インデックス付きセット間のファンクターで作業することです。

f :: (i -> *) -> (o -> *)

ここで o を格納する異なる種類の構造 i というように、さまざまな種類の要素があります。これらは 閉じた であり、ヤコビアン構成

J f :: (i -> *) -> ((o, i) -> *)

ここで、結果の各 (o, i) -の構造は偏導関数であり、どのようにすれば i -に穴を開ける方法を教えてくれます。 o -構造体の中にある穴です。しかし、それは依存する型付けを楽しむもので、別の機会にしましょう。