15

私はコモナドの概念を理解しようとしています。このブログ投稿を読んだ後、コモナドが何をするのか、モナドとどのように関係しているのかをしっかりと理解できたと思います。しかし、私はこの主題を少し掘り下げて、一般的なリスト型 (ご存知のように[a]) の comonad インスタンスがどのように見えるかを考えてみようと思いました。正しい。

したがって、ブログ投稿で使用されたインスタンスを考えると、次のようになります。

class Functor w => Comonad w where
    (=>>)    :: w a -> (w a -> b) -> w b
    coreturn :: w a -> a
    cojoin     :: w a -> w (w a)

のインスタンス宣言は次の[a]ようになると思いました ( の構文[a]はおそらく不可能か間違っていますが、ここでアイデアを得ることができます):

instance Comonad [a] where
    coreturn = head
    cojoin = Data.List.subsequences --this is what I'm confused about
    x =>> f = map f (cojoin x)

ここではsubsequences、リストのすべてを見つけるだけですが、それを使用することは完全に実行可能powersetです。の形式のリストにはいくつかの関数があり、(a -> [a])どれが正しいかはあいまいです。

[a]これは、comonad として適切にインスタンス化できないことを意味するのでしょうか、それとも、cojoin実際に何を行うかを決定するのは単にユーザー次第なのでしょうか?

4

2 に答える 2

21

コメントに記載されているように、何かcoreturnを返さなければならないため、空である可能性があるリストの comonad インスタンスを持つことはできません。

それとは別に、インスタンスはコモンド法も満たさなければなりません。とで表すcoreturnとcojoin、次のようになります。

  1. coreturn . cojoin = id
  2. fmap coreturn . cojoin = id
  3. cojoin . cojoin = fmap cojoin . cojoin

空のリストを許可しない場合でも、これらがインスタンスに当てはまらないことは簡単にわかります。ただし、 が であると仮定するcoreturnとhead、これらの法則を使用して、どうあるべきかについての手がかりを得ることができcojoinます。

(1) から、 によって返されるリストの最初の要素はcojoin元のリストでなければならないことがわかります。(2) から、各内部リストの最初の要素を結合すると、元のリストも生成される必要があることがわかります。tailsこれは*のようなものが必要であることを強く示唆しており、これも (3) を満たすことが確認できます。

*具体的にはtails、末尾に空のリストが含まれていないバージョンの が必要です。

于 2012-09-21T20:21:46.750 に答える
13

他の人が言及したことを明確にするために、空でないリストの次のタイプを検討してください。

data NonEmptyList a = One a | Many a (NonEmptyList a)

map :: (a -> b) -> NonEmptyList a -> NonEmptyList b
map f (One x) = One (f x)
map f (Many x xs) = Many (f x) (map f xs)

(++) :: NonEmptyList a -> NonEmptyList a -> NonEmptyList a
One x     ++ ys = Many x ys
Many x xs ++ ys = Many x (xs ++ ys)

tails :: NonEmptyList a -> NonEmptyList (NonEmptyList a)
tails l@(One _) = One l
tails l@(Many _ xs) = Many l (tails xs)

有効な comonad インスタンスは次のように記述できます。

instance Functor NonEmptyList where
  fmap = map

instance Comonad NonEmptyList where
  coreturn (One x) = x
  coreturn (Many x xs) = x

  cojoin = tails

  -- this should be a default implementation
  x =>> f = fmap f (cojoin x)

hammar によって列挙された法則を証明しましょう。与えられた最初のステップとして、自由にそれぞれを eta 展開します。

法律1。

(coreturn . cojoin) xs = id xs
-- definition of `.`, `cojoin`, and `id`
(coreturn (tails xs) = xs
-- case on xs
  -- assume xs is (One x)
  (coreturn (tails (One x))) = One x
  -- definition of tails
  (coreturn (One (One x))) = One x
  -- definition of coreturn
  One x = One x

  -- assume xs is (Many y ys)
  (coreturn (tails (Many y ys))) = Many y ys
  -- definition of tails
  (coreturn (Many (Many y ys) (tails ys)) = Many y ys
  -- definition of coreturn
  Many y ys = Many y ys

  -- assume xs is _|_
  (coreturn (tails _|_)) = _|_
  -- tails pattern matches on its argument
  (coreturn _|_) = _|_
  -- coreturn pattern matches on its argument
  _|_ = _|_

法律 2。

(fmap coreturn . cojoin) xs = id xs
-- definition of `.`, `cojoin`, `fmap`, and `id`
map coreturn (tails xs) = xs
-- case on xs
  -- assume xs is (One x)
  map coreturn (tails (One x)) = One x
  -- defn of tails
  map coreturn (One (One x)) = One x
  -- defn of map
  One (coreturn (One x)) = One x
  -- defn of coreturn 
  One x = One x

  -- assume xs is (Many y ys)
  map coreturn (tails (Many y ys)) = Many y ys
  -- defn of tails
  map coreturn (Many (Many y ys) (tails ys)) = Many y ys
  -- defn of map
  Many (coreturn (Many y ys)) (map coreturn (tails ys)) = Many y ys
  -- defn of coreturn
  Many y (map coreturn (tail ys)) = Many y ys
  -- eliminate matching portions
  map coreturn (tail ys) = ys
  -- wave hands.
  -- If the list is not self-referential,
  -- then this can be alleviated by an inductive hypothesis.
  -- If not, then you can probably prove it anyways.

  -- assume xs = _|_
  map coreturn (tails _|_) = _|_
  -- tails matches on its argument
  map coreturn _|_ = _|_
  -- map matches on its second argument
  _|_ = _|_

法律3。

(cojoin . cojoin) xs = (fmap cojoin . cojoin) xs
-- defn of `.`, `fmap`, and `cojoin`
tails (tails xs) = map tails (tails xs)
-- case on xs
  -- assume xs = One x
  tails (tails (One x)) = map tails (tails (One x))
  -- defn of tails, both sides
  tails (One (One x)) = map tails (One (One x))
  -- defn of map
  tails (One (One x)) = One (tails (One x))
  -- defn of tails, both sides
  One (One (One x)) = One (One (One x))

  -- assume xs = Many y ys
  (this gets ugly. left as exercise to reader)

  -- assume xs = _|_
  tails (tails _|_) = map tails (tails _|_)
  -- tails matches on its argument
  tails _|_ = map tails _|_
  -- tails matches on its argument, map matches on its second argument
  _|_ = _|_
于 2012-09-21T21:56:21.497 に答える