40

私は で遊んでいますがCofree、まったく理解できません。

たとえばCofree [] Num、ghci で遊びたいのですが、興味深い例がまったく得られません。

たとえば、Cofree 型を作成すると、次のようになります。

let a = 1 :< [2, 3]

私は期待extract a == 1しますが、代わりに次のエラーが発生します。

No instance for (Num (Cofree [] a0)) arising from a use of ‘it’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

そして次のタイプ：

extract a :: (Num a, Num (Cofree [] a)) => a

Cofree をファンクターと一緒に使用する方法について、些細なことでも簡単な例をいくつか入手できますか[]?MaybeEither

  • extract
  • extend
  • unwrap
  • duplicate?

クロス投稿: https://www.reddit.com/r/haskell/comments/4wlw70/what_are_some_motivating_examples_for_cofree/

編集: David Young のコメントに導かれて、ここに私の最初の試みが間違っていた場所を示すいくつかのより良い例がありますが、Cofree の直感を導くことができるいくつかの例が大好きです:

> let a = 1 :< []
> extract a
    1
> let b = 1 :< [(2 :< []), (3 :< [])]
> extract b
    1
> unwrap b
    [2 :< [],3 :< []]
> map extract $ unwrap b
    [2,3]
4

1 に答える 1

61

Cofreeデータ型の定義を要約してみましょう。

data Cofree f a = a :< f (Cofree f a)

少なくとも、例の問題を診断するにはこれで十分です。あなたが書いたとき

1 :< [2, 3]

あなたは小さな間違いを犯しました。ここで、f = []とaは数値です1 :: a。それに応じて必要です

[2, 3] :: [Cofree [] a]

それゆえ

2 :: Cofree [] a

のインスタンスでもある場合、これは問題ありません。したがって、定義は満たされる可能性が低い制約を取得し、実際、値を使用すると、制約を満たす試みは失敗します。Cofree [] aNum

で再試行してください

1 :< [2 :< [], 3 :< []]

運が良くなるはずです。

では、何があるか見てみましょう。シンプルに保つことから始めます。なにCofree f ()？特に、とはCofree [] ()何ですか？後者は の固定点に同形です[]: 各ノードがサブツリーのリストであるツリー構造で、「ラベルのないバラの木」としても知られています。例えば、

() :< [  () :< [  () :< []
               ,  () :< []
               ]
      ,  () :< []
      ]

同様に、Cofree Maybe ()は多かれ少なかれ の固定点Maybe: 自然数のコピーですMaybe。サブツリーを差し込む位置がゼロまたは 1 つになるためです。

zero :: Cofree Maybe ()
zero = () :< Nothing
succ :: Cofree Maybe () -> Cofree Maybe ()
succ n = () :< Just n

重要な自明なケースはCofree (Const y) ()で、これは のコピーですy。Const yファンクターはサブツリーの位置を与えません。

pack :: y -> Cofree (Const y) ()
pack y = () :< Const y

次に、もう一方のパラメーターに取り掛かりましょう。各ノードに付けるラベルの種類がわかります。パラメータの名前をより暗示的に変更する

data Cofree nodeOf label = label :< nodeOf (Cofree nodeOf label)

(Const y)例にラベルを付けると、ペアが得られます

pair :: x -> y -> Cofree (Const y) x
pair x y = x :< Const y

数値のノードにラベルを付けると、空でないリストが得られます

one :: x -> Cofree Maybe x
one = x :< Nothing
cons :: x -> Cofree Maybe x -> Cofree Maybe x
cons x xs = x :< Just xs

リストの場合は、ラベルの付いたバラの木を取得します。

0 :< [  1 :< [  3 :< []
             ,  4 :< []
             ]
     ,  2 :< []
     ]

これらの構造は、たとえ子がなくても、少なくとも最上位ノードがあり、そのノードには常にラベルがあるため、常に「空ではありません」。このextract操作により、最上位ノードのラベルが得られます。

extract :: Cofree f a -> a
extract (a :< _) = a

つまり、トップ ラベルのコンテキストextractを破棄します。

これで、duplicate操作によってすべてのラベルが独自のコンテキストで装飾されます。

duplicate :: Cofree f a -> Cofree f (Cofree f a)
duplicate a :< fca = (a :< fca) :< fmap duplicate fca  -- f's fmap

ツリー全体にアクセスすることでFunctorインスタンスを取得できますCofree f

fmap :: (a -> b) -> Cofree f a -> Cofree f b
fmap g (a :< fca) = g a :< fmap (fmap g) fca
    --                     ^^^^  ^^^^
    --                 f's fmap  ||||
    --                           (Cofree f)'s fmap, used recursively

それを見るのは難しいことではありません

fmap extract . duplicate = id

duplicateすべてのノードをそのコンテキストで装飾し、装飾を破棄するためfmap extractです。

fmap出力のラベルを計算するには、入力のラベルのみを参照する必要があることに注意してください。コンテキスト内の各入力ラベルに応じて出力ラベルを計算したいとします。たとえば、ラベルのないツリーが与えられた場合、各ノードにそのサブツリー全体のサイズでラベルを付けたい場合があります。Foldableのインスタンスのおかげで、Cofree fノードをカウントできるはずです。

length :: Foldable f => Cofree f a -> Int

つまり、

fmap length . duplicate :: Cofree f a -> Cofree f Int

comonads の重要なアイデアは、「何らかのコンテキストを持つもの」をキャプチャし、コンテキスト依存のマップをどこにでも適用できるようにすることです。

extend :: Comonad c => (c a -> b) -> c a -> c b
extend f = fmap f       -- context-dependent map everywhere
           .            -- after
           duplicate    -- decorating everything with its context

より直接的に定義するextendことで、重複の問題を回避できます (ただし、それは共有にすぎません)。

extend :: (Cofree f a -> b) -> Cofree f a -> Cofree f b
extend g ca@(_ :< fca) = g ca :< fmap (extend g) fca

そして、あなたは取るduplicateことによって戻ることができます

duplicate = extend id -- the output label is the input label in its context

extractさらに、コンテキスト内の各ラベルに対して行うこととして選択した場合は、各ラベルを元の場所に戻すだけです。

extend extract = id

これらの「コンテキスト内のラベルに対する操作」は、「co-Kleisli 矢印」と呼ばれます。

g :: c a -> b

の仕事はextend、co-Kleisli アローを構造全体の関数として解釈することです。extract演算は恒等共クライスリの矢であり、 によって恒等関数として解釈されextendます。もちろんコ・クライスリ構成もある

(=<=) :: Comonad c => (c s -> t) -> (c r -> s) -> (c r -> t)
(g =<= h) = g . extend h

また、コモナドの法則により、=<=が 結合的で吸収されることが保証されextract、co-Kleisli カテゴリが得られます。さらに、

extend (g =<= h)  =  extend g . extend h

これextendは、co-Kleisli 圏から集合関数への (圏論的な意味での)関手です。これらの法則は、ノード形状Cofreeの法則に従うため、チェックするのは難しくありません。Functor

cofree comonad の構造を理解するための 1 つの便利な方法は、一種の「ゲームサーバー」です。構造

a :< fca

ゲームの状態を表します。ゲーム内の移動は、 を取得する場合は「停止」するaか、 のサブツリーを選択して「続行」するかのいずれかで構成されますfca。たとえば、

Cofree ((->) move) prize

このサーバーのクライアントは、停止するか、またはmove: のリストを指定して続行する必要がありますmove。ゲームは次のように行われます。

play :: [move] -> Cofree ((->) move) prize -> prize
play []       (prize :< _) = prize
play (m : ms) (_     :< f) = play ms (f m)

おそらく amoveは aCharであり、 theprizeは文字シーケンスを解析した結果です。

[move]よく見ると、それが のバージョンであることがわかりますFree ((,) move) ()。フリーモナドはクライアント戦略を表します。ファンクター((,) move)は、コマンド「send a move」のみを備えたコマンドインターフェイスになります。functor((->) move)は、対応する構造体である "の送信に応答するmove" です。

一部のファンクタは、コマンド インターフェイスをキャプチャしていると見なすことができます。そのようなファンクタの自由なモナドは、コマンドを作成するプログラムを表します。ファンクターには、コマンドへの応答方法を表す「デュアル」があります。双対の cofree comonad は、コマンドを作成するプログラムを実行できる環境の一般的な概念であり、ラベルは、プログラムが停止して値を返した場合に何をすべきかを示し、下位構造は、次の場合にプログラムの実行を続行する方法を示します。コマンドを発行します。

例えば、

data Comms x = Send Char x | Receive (Char -> x)

文字の送受信が許可されていることを示します。その二重は

data Responder x = Resp {ifSend :: Char -> x, ifReceive :: (Char, x)}

演習として、相互作用を実装できるかどうかを確認します

chatter :: Free Comms x -> Cofree Responder y -> (x, y)
于 2016-08-07T19:41:25.237 に答える