haskell - バイナリツリージッパーを Comonad のインスタンスにする方法は?

Question

バイナリツリージッパーを comonad のインスタンスにしたいのですが、duplicate適切に実装する方法がわかりません。

これが私の試みです：

{-# LANGUAGE DeriveFunctor #-}
import Data.Function
import Control.Arrow
import Control.Comonad

data BinTree a
    = Leaf a
    | Branch a (BinTree a) (BinTree a)
      deriving (Functor, Show, Eq)

data Dir = L | R
    deriving (Show, Eq)

-- an incomplete binary tree, aka data context
data Partial a = Missing Dir (BinTree a) a
    deriving (Show, Eq, Functor)

-- BTZ for BinTree Zipper
newtype BTZ a = BTZ { getBTZ :: ([Partial a], BinTree a) }
    deriving (Show, Eq)

instance Functor BTZ where
    fmap f (BTZ (cs,t)) = BTZ (map (fmap f) cs, fmap f t)

-- | replace every node label with the zipper focusing on that node
dup :: BinTree a -> BinTree (BTZ a)
dup (Leaf v) = Leaf (BTZ ([], Leaf v))
dup t@(Branch v tl tr) = Branch (BTZ ([],t)) tlZ trZ
    where
        tlZ = fmap (BTZ . first (++ [Missing L tr v]) . getBTZ) (dup tl)
        trZ = fmap (BTZ . first (++ [Missing R tl v]) . getBTZ) (dup tr)

-- | extract root label
rootVal :: BinTree a -> a
rootVal (Leaf v) = v
rootVal (Branch v _ _) = v

-- | move zipper focus around
goUp, goLeft, goRight :: BTZ a -> BTZ a

goUp (BTZ ([], _)) = error "already at root"
goUp (BTZ (Missing wt t2 v:xs, t1)) = case wt of
    L -> BTZ (xs, Branch v t1 t2)
    R -> BTZ (xs, Branch v t2 t1)

goLeft z = let (cs,t) = getBTZ z in
    case t of
      Leaf _ -> error "already at leaf"
      Branch v t1 t2 -> BTZ (Missing L t2 v:cs, t1)

goRight z = let (cs,t) = getBTZ z in
    case t of
      Leaf _ -> error "already at leaf"
      Branch v t1 t2 -> BTZ (Missing R t1 v:cs, t2)

instance Comonad BTZ where
    extract (BTZ (_,t)) =
        case t of
          Leaf v -> v
          Branch v _ _ -> v

    duplicate z@(BTZ (cs, bt)) = case bt of
        Leaf _ -> BTZ (csZ, Leaf z) -- extract . duplicate = id
        Branch v tl tr ->
            -- for each subtree, use "dup" to build zippers,
            -- and attach the current focusing root(bt) and rest of the data context to it
            let tlZ = fmap (BTZ . first (++Missing L tr v :cs) . getBTZ) (dup tl)
                trZ = fmap (BTZ . first (++Missing R tl v :cs) . getBTZ) (dup tr)
             in BTZ (csZ, Branch z tlZ trZ)
        where
            -- go up and duplicate, we'll have a "BTZ (BTZ a)"
            -- from which we can grab "[Partial (BTZ a)]" out
            -- TODO: not sure if it works
            upZippers = take (length cs-1) . tail $ iterate goUp z
            csZ = fmap (head . fst . getBTZ . duplicate) upZippers

main :: IO ()
main = do
   let tr :: BTZ Int
       tr = rootVal $ dup (Branch 1 (Leaf 2) (Branch 3 (Leaf 4) (Leaf 5)))
       equalOnTr :: Eq a => (BTZ Int -> a) -> (BTZ Int -> a) -> Bool
       equalOnTr = (==) `on` ($ tr)
   print $ (extract . duplicate)      `equalOnTr` id
   print $ (fmap extract . duplicate) `equalOnTr` id
   print $ (duplicate . duplicate)    `equalOnTr` (fmap duplicate . duplicate)

いくつかの説明：

BinTree aはバイナリツリーデータ型で、各ツリーノードにはラベルが含まれます。
Partial a左または右の部分木を持つ二分木です。私のコードのスタックはPartial a 、データコンテキストの役割を果たします。
BTZBinTreeのインスタンスを作成したいジッパーを表しComonad、データコンテキストとフォーカスサブツリーで構成されます。

のインスタンスにするためにComonad、私の計画はとを実装extractしduplicate、いくつかのランダムなバイナリツリーを取得して、コモナドプロパティが保持されるかどうかを検証することです。

これextractは簡単で、フォーカスサブツリーを取り出すだけです。

関数dupは、各ノードラベルをそのノードに焦点を当てたツリージッパーに置き換える補助関数として機能します。

の場合duplicate z、ノードラベルはzそれ自体である必要がありextract . duplicate == idます。非リーフノードのdup場合、親がいないかのようにサブツリーを処理し、現在のフォーカスzと残りのデータコンテキストが後でこれらのジッパーに追加されます。

これまでのところ、最初の 2 つの comonad プロパティ (extract . duplicate = idおよびfmap extract . duplicate) は満たされていますが、データコンテキストをどうするかはわかりません。私が現在していることは、ジッパーを取り、z上げ続けることです. 途中で、各データコンテキストスタックのトップを取得して新しいデータコンテキストスタックを構築します。これは正しいように聞こえますが、正しい型 ([Partial (BTZ a)]です。しかし、私のアプローチでは第 3 法則を満たすことはできません。

上記のバイナリツリージッパーのデータ型定義を考えると、それを Comonad のインスタンスにすることは可能ですか? 答えが「はい」の場合、私のアプローチに何か問題がありますか?

score 38 · Accepted Answer

微分計算では、ライプニッツの表記法はニュートンの表記法よりも混乱が少ないです。物事の文脈は微分によって与えられるので、文脈化されているものに注意を払わなければなりません。ここでは、サブツリーと要素という 2 つの「サブ構造」の概念が働いています。それらはそれぞれ、「コンテキスト」と「ジッパー」の異なる (ただし関連する) 概念を持っています。ジッパーは、物とそのコンテキストのペアです。

あなたのタイプは、サブツリーBTZのジッパーの概念として提示されます。ただし、ジッパーの共通構造は、要素のジッパーで機能します。つまり、「ここに要素を与える」ことを意味します。「各要素をそのコンテキストで装飾する」ことを意味します。したがって、要素コンテキストが必要です。紛らわしいことに、これらのバイナリツリーでは、要素ジッパーとサブツリージッパーは同型ですが、それは非常に特殊な理由によるものです (つまり、それらが cofree 共通モナドを形成するため)。extractduplicate

一般に、要素ジッパーとサブツリージッパーは異なります (たとえば、リストの場合)。リストの要素ジッパー共通モナドを構築することから始めれば、ツリーに戻ったときに迷子になる可能性が低くなります。他の人やあなた自身のために、もう少し全体像を埋めてみてください.

サブリストコンテキスト

のサブリスト-contexts は[a]によって与えられ[a]、サブリストからリスト全体への途中で通過する要素のリストです。[3,4]inのサブリストコンテキスト[1,2,3,4]はです[2,1]。再帰的データのサブノードコンテキストは常に、ノードからルートへのパス上にあるものを表すリストです。各ステップのタイプは、再帰変数に関するデータの 1 つのノードの式の偏微分によって与えられます。だからここに

[a] = t where             -- t is the recursive variable standing for [a]
  t = 1 + a*t             -- lists of a are either [] or an (a : t) pair
∂/∂t (1 + a*t) = a        -- that's one step on a path from node to root
sublist contexts are [a]  -- a list of such steps

したがって、サブリストジッパーはペアです

data LinLZ a = LinLZ
  {  subListCtxt  :: [a]
  ,  subList      :: [a]
  }

サブリストをそのコンテキストにプラグインし、パスを逆に戻す関数を書くことができます

plugLinLZ :: LinLZ a -> [a]
plugLinLZ (LinLZ { subListCtxt = [],      subList = ys})  = ys
plugLinLZ (LinLZ { subListCtxt = x : xs,  subList = ys})
  = plugLinLZ (LinLZ { subListCtxt = xs,  subList = x : ys})

しかしLinLZ、Comonad（たとえば）から

LinLZ { subListCtxt = [], subList = [] }

要素( from )extractはできません。サブリストのみです。aLinLZ a

リスト要素のコンテキスト

リスト要素コンテキストはリストのペアです: フォーカスされた要素の前の要素とその後の要素です。再帰構造内の要素コンテキストは常にペアです。最初に、要素が格納されているサブノードのサブノードコンテキストを指定し、次にそのノード内の要素のコンテキストを指定します。要素を表す変数に関してノードの式を微分することにより、ノード内の要素コンテキストを取得します。

[a] = t where             -- t is the recursive variable standing for [a]
  t = 1 + a*t             -- lists of a are either [] or an (a : t) pair
∂/∂a (1 + a*t) = t = [a]  -- the context for the head element is the tail list

したがって、要素コンテキストはペアで与えられます

type DL a =
  (  [a]     -- the sublist context for the node where the element is
  ,  [a]     -- the tail of the node where the element is
  )

要素ジッパーは、そのようなコンテキストと要素「穴の中」をペアにすることによって与えられます。

data ZL a = ZL
  {  this :: a
  ,  between :: DL a
  }  deriving (Show, Eq, Functor)

このようなジッパーをリストに戻す (要素から「外に出る」) には、最初に要素が置かれているサブリストを再構成し、サブリストジッパーを指定してから、サブリストをそのサブリストコンテキストにプラグインします。

outZL :: ZL a -> [a]
outZL (ZL { this = x, between = (zs, xs) })
  = plugLinLZ (LinLZ { subListCtxt = zs, subList = x : xs })

各要素をコンテキストに入れる

リストがあれば、各要素をそのコンテキストとペアにすることができます。要素の 1 つに「入る」方法のリストを取得します。私たちはこのように始まり、

into :: [a] -> [ZL a]
into xs = moreInto (LinLZ { subListCtxt = [], subList = xs })

しかし、実際の作業は、リストインコンテキストで機能するヘルパー関数によって行われます。

moreInto :: LinLZ a -> [ZL a]
moreInto (LinLZ { subListCtxt = _,   subList = [] })      = []
moreInto (LinLZ { subListCtxt = zs,  subList = x : xs })
  =  ZL { this = x, between = (zs, xs) } 
  :  moreInto (LinLZ { subListCtxt = x : zs,  subList = xs })

出力が電流の形状を反映していることに注意してくださいsubList。また、ファスナーxの所にファスナーが付いていthis = xます。また、装飾用の生成ジッパーには正しいコンテキストxsがsubList = xsあり、過去に移動したことを記録していxます。テスト、

into [1,2,3,4] =
  [  ZL {this = 1, between = ([],[2,3,4])}
  ,  ZL {this = 2, between = ([1],[3,4])}
  ,  ZL {this = 3, between = ([2,1],[4])}
  ,  ZL {this = 4, between = ([3,2,1],[])}
  ]

リスト要素ジッパーの共通構造

要素から出る方法、または利用可能な要素の 1 つに入る方法を見てきました。共通構造は、現在の場所にとどまるか、他の要素の 1 つに移動するかのいずれかで、要素間を移動する方法を教えてくれます。

instance Comonad ZL where

はextract、訪問している要素を示します。

  extract = this

ジッパーの場合、現在の要素を現在のジッパー全体duplicateに置き換えます(その)...xzlthis = x

  duplicate zl@(ZL { this = x, between = (zs, ys) }) = ZL
    {  this = zl

...そして、各要素に再び焦点を当てる方法を示しながら、コンテキストを順を追って説明します。私たちの存在moreIntoは私たちを内側に動かしますが、私たちも動かなければなりませんoutward...

    ,  between =
         (  outward (LinLZ { subListCtxt = zs, subList = x : ys })
         ,  moreInto (LinLZ { subListCtxt = x : zs, subList = ys })
         )
    }

...これには、次のように、コンテキストに沿って戻り、要素をサブリストに移動することが含まれます

    where
      outward (LinLZ { subListCtxt = [], subList = _ }) = []
      outward (LinLZ { subListCtxt = z : zs, subList = ys })
        =  ZL { this = z, between = (zs, ys) }
        :  outward (LinLZ { subListCtxt = zs, subList = z : ys })

だから私たちは得る

duplicate ZL {this = 2, between = ([1],[3,4])}
  = ZL
  {  this = ZL {this = 2, between = ([1],[3,4])}
  ,  between =
     (  [  ZL {this = 1, between = ([],[2,3,4])}  ]
     ,  [  ZL {this = 3, between = ([2,1],[4])}
        ,  ZL {this = 4, between = ([3,2,1],[])}
        ]
     )
  }

wherethisは "staying at 2" で、between"moving to 1" と "moving to 3or moving to 4" です。

したがって、共通構造は、リスト内にあるさまざまな要素間を移動する方法を示しています。サブリスト構造は、要素が存在するノードを見つける上で重要な役割を果たしますが、ジッパー構造duplicated は要素ジッパーです。

では、木はどうですか？

余談: ラベルの付いたツリーは既にコモナドです

あなたのタイプのバイナリツリーをリファクタリングして、いくつかの構造を引き出します。文字通り、葉やフォークにラベルを付ける要素を共通因数として引き出してみましょう。TFこのリーフまたはフォークサブツリー構造を説明するファンクター ( ) も分離してみましょう。

data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
data BT a = a :& TF (BT a) deriving (Show, Eq, Functor)

つまり、すべてのツリーノードには、リーフであれフォークであれ、ラベルがあります。

すべてのノードがラベルと部分構造の塊を持つ構造を持っているところはどこでも、コモナドがあります: cofree comonadです。もう少しリファクタリングして、抽象化してみましょうTF...

data CoFree f a = a :& f (CoFree f a) deriving (Functor)

...つまり、以前のf場所に将軍がいTFます。特定の木を復元できます。

data TF t = Leaf | Fork (t, t) deriving (Show, Eq, Functor)
type BT = CoFree TF
deriving instance Show a => Show (BT a)
deriving instance Eq a => Eq (BT a)

そして今、一度、cofree comonad 構造を与えることができます。すべてのサブツリーにはルート要素があるため、すべての要素をルートを持つツリーで装飾できます。

instance Functor f => Comonad (CoFree f) where
  extract   (a :& _)     = a                         -- extract root element
  duplicate t@(a :& ft)  = t :& fmap duplicate ft    -- replace root element by whole tree

例を挙げましょう

aTree =
  0 :& Fork
  (  1 :& Fork
     (  2 :& Leaf
     ,  3 :& Leaf
     )
  ,  4 :& Leaf
  )

duplicate aTree =
  (0 :& Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf)) :& Fork
  (  (1 :& Fork (2 :& Leaf,3 :& Leaf)) :& Fork
     (  (2 :& Leaf) :& Leaf
     ,  (3 :& Leaf) :& Leaf
     )
  ,  (4 :& Leaf) :& Leaf
  )

見る？各要素はそのサブツリーとペアになっています!

すべてのノードが要素を持っているわけではないため、リストは cofree comonad を生成しません。具体的に[]は、要素を持っていません。cofree comonad では、常にあなたがいる要素があり、ツリー構造のさらに下を見ることはできますが、それ以上上を見ることはできません。

エレメントジッパーコモナドでは、常に自分のいる場所にエレメントがあり、上下の両方を見ることができます。

二分木のサブツリーと要素のコンテキスト

代数的に

d/dt (TF t) = d/dt (1 + t*t) = 0 + (1*t + t*1)

定義できるように

type DTF t = Either ((), t) (t, ())

「サブ構造のブロブ」内のサブツリーが左側または右側にあると言っています。「プラグイン」が機能することを確認できます。

plugF :: t -> DTF t -> TF t
plugF  t  (Left   ((), r))  = Fork (t, r)
plugF  t  (Right  (l, ()))  = Fork (l, t)

インスタンス化tしてノードラベルとペアにすると、サブツリーコンテキストの 1 つのステップが得られます

type BTStep a = (a, DTF (BT a))

Partialこれは質問のに同形です。

plugBTinBT :: BT a -> BTStep a -> BT a
plugBTinBT t (a, d) = a :& plugF t d

したがって、別の内部のサブツリーコンテキストはで与えられます。BT a[BTStep a]

しかし、要素コンテキストはどうでしょうか? さて、すべての要素は何らかのサブツリーにラベルを付けるので、そのサブツリーのコンテキストと、要素によってラベル付けされたツリーの残りの部分の両方を記録する必要があります。

data DBT a = DBT
  {  below  :: TF (BT a)    -- the rest of the element's node
  ,  above  :: [BTStep a]   -- the subtree context of the element's node
  }  deriving (Show, Eq)

面倒なことに、自分のFunctorインスタンスをロールバックする必要があります。

instance Functor DBT where
  fmap f (DBT { above = a, below = b }) = DBT
    {  below = fmap (fmap f) b
    ,  above = fmap (f *** (either
         (Left   . (id *** fmap f))
         (Right  . (fmap f *** id)))) a  
    }

これで、要素ジッパーとは何かを言うことができます。

data BTZ a = BTZ
  {  here  :: a
  ,  ctxt  :: DBT a
  }  deriving (Show, Eq, Functor)

「何が新しいの？」と思っているなら、あなたは正しいです。aboveとで与えられるサブツリーとともに、サブツリーコンテキストがhereありbelowます。それは、ノードにラベルを付ける要素だけが要素だからです。ノードを要素とそのコンテキストに分割することは、ノードをラベルとサブ構造のブロブに分割することと同じです。つまり、cofree コモナドでこの一致が得られますが、一般的にはそうではありません。

しかし、この偶然はただの気晴らしです！リストで見たように、element-zippers を共通にするために、element-zippers を subnode-zippers と同じにする必要はありません。

上記のリストと同じパターンに従って、すべての要素をそのコンテキストで装飾できます。この作業は、現在アクセスしているサブツリーコンテキストを蓄積するヘルパー関数によって行われます。

down :: BT a -> BT (BTZ a)
down t = downIn t []

downIn :: BT a -> [BTStep a] -> BT (BTZ a)
downIn (a :& ft) ads =
  BTZ { here = a, ctxt = DBT { below = ft, above = ads } }
  :& furtherIn a ft ads

a重点的にジッパーに交換されていることに注意してくださいa。サブツリーは別のヘルパーによって処理されます。

furtherIn :: a -> TF (BT a) -> [BTStep a] -> TF (BT (BTZ a))
furtherIn a Leaf           ads  = Leaf
furtherIn a (Fork (l, r))  ads  = Fork
  (  downIn l ((a, Left   ((), r)) : ads)
  ,  downIn r ((a, Right  (l, ())) : ads)
  )

ツリー構造をfurtherIn保持しますが、サブツリーにアクセスしたときにサブツリーコンテキストを適切に成長させます。

再確認しましょう。

down aTree =
  BTZ {  here  = 0, ctxt = DBT {
         below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf),
         above = []}} :& Fork
  (  BTZ {  here = 1, ctxt = DBT {
            below = Fork (2 :& Leaf,3 :& Leaf),
            above = [(0,Left ((),4 :& Leaf))]}} :& Fork
     (  BTZ {  here = 2, ctxt = DBT {
               below = Leaf,
               above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf
     ,  BTZ {  here = 3, ctxt = DBT {
               below = Leaf,
               above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf
     )
  ,  BTZ {  here = 4, ctxt = DBT {
            below = Leaf,
            above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf)

見る？各要素は、その下のツリーだけでなく、そのコンテキスト全体で装飾されています。

コモナドを形成する二分木ジッパー

要素をコンテキストで装飾できるようになったので、Comonadインスタンスを構築しましょう。従来通り...

instance Comonad BTZ where
  extract = here

...extractは、フォーカスされている要素を示しており、既存の機械を利用してツリーをさらに進めることができますが、外側に移動する方法を探るために新しいキットを作成する必要があります。

  duplicate z@(BTZ { here = a, ctxt = DBT { below = ft, above = ads }}) = BTZ
    {  here = z
    ,  ctxt = DBT
         {  below = furtherIn a ft ads  -- move somewhere below a
         ,  above = go_a (a :& ft) ads  -- go above a
         }
    } where

リストの場合と同様に、外側に移動するには、パスに沿ってルートに戻る必要があります。リストと同様に、パスの各ステップは訪問できる場所です。

    go_a t []          = []
    go_a t (ad : ads)  = go_ad t ad ads : go_a (plugBTinBT t ad) ads
    go_ad t (a, d) ads =
      (  BTZ { here = a, ctxt = DBT { below = plugF t d, above = ads } }  -- visit here
      ,  go_d t a d ads                                                   -- try other subtree
      )

リストとは異なり、探索するパスに沿って代替ブランチがあります。未訪問のサブツリーがパスに格納されている場合は常に、その要素をコンテキストで装飾する必要があります。

    go_d t a (Left ((), r)) ads = Left ((), downIn r ((a, Right (t, ())) : ads))
    go_d t a (Right (l, ())) ads = Right (downIn l ((a, Left ((), t)) : ads), ())

これで、任意の要素位置から別の要素位置に再フォーカスする方法を説明しました。

どれどれ。ここで私たちは訪問していました1：

duplicate (BTZ {here = 1, ctxt = DBT {
                below = Fork (2 :& Leaf,3 :& Leaf),
                above = [(0,Left ((),4 :& Leaf))]}}) =
  BTZ {here = BTZ {here = 1, ctxt = DBT {
                   below = Fork (2 :& Leaf,3 :& Leaf),
                   above = [(0,Left ((),4 :& Leaf))]}}, ctxt = DBT {
       below = Fork (BTZ {here = 2, ctxt = DBT {
                          below = Leaf,
                          above = [(1,Left ((),3 :& Leaf)),(0,Left ((),4 :& Leaf))]}} :& Leaf
                    ,BTZ {here = 3, ctxt = DBT {
                          below = Leaf,
                          above = [(1,Right (2 :& Leaf,())),(0,Left ((),4 :& Leaf))]}} :& Leaf
                   ),
       above = [(BTZ {here = 0, ctxt = DBT {
                      below = Fork (1 :& Fork (2 :& Leaf,3 :& Leaf),4 :& Leaf),
                      above = []}}
                ,Left ((),BTZ {here = 4, ctxt = DBT {
                               below = Leaf,
                               above = [(0,Right (1 :& Fork (2 :& Leaf,3 :& Leaf),()))]}} :& Leaf)
                )
               ]}}

少量のデータサンプルでコモナドの法則をテストする方法として、次のことを確認してみましょう。

fmap (\ z -> extract (duplicate z) == z) (down aTree)
  = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)
fmap (\ z -> fmap extract (duplicate z) == z) (down aTree)
  = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)
fmap (\ z -> fmap duplicate (duplicate z) == duplicate (duplicate z)) (down aTree)
  = True :& Fork (True :& Fork (True :& Leaf,True :& Leaf),True :& Leaf)

haskell - バイナリ ツリー ジッパーを Comonad のインスタンスにする方法は?

1 に答える 1

サブリスト コンテキスト