Comonoid with respect to Day convolution.

Laws

coapply must satisfy the following equations. Here, erase1 and erase2 are defined using extract method inherited from Comonad.

erase1 . coapply = id
erase2 . coapply = id
trans1 coapply . coapply = assoc . trans2 coapply . coapply

Furthermore, duplicateDefault derived from coapply must be equivalent to duplicate inherited from Comonad.

duplicateDefault = dayToCompose . coapply
                 = duplicate

Examples

Env comonad, or (,) e, is an instance of Comonoid.

instance Comonoid ((,) e) where
  coapply :: forall x. (e, x) -> Day ((,) e) ((,) e) x
  -- ~ forall x. (e,x) -> ∃b c. ((e,b), (e,c), b -> c -> x)
  -- ~ forall x. (e,x) -> (e,e, ∃b c.(b, c, b -> c -> x))
  -- ~ forall x. (e,x) -> (e,e,x)
  -- ~ e -> (e,e)
  coapply (e, x) = Day (e, ()) (e, ()) (\_ _ -> x)

Traced comonad, or ((->) m), is another example.

instance Monoid m => Comonoid ((->) m) where
  coapply :: forall x. (m -> x) -> Day ((->) m) ((->) m) x
  -- ~ forall x. (m -> x) -> ∃b c. (m -> b, m -> c, b -> c -> x)
  -- ~ forall x. (m -> x) -> (m -> m -> x)
  -- ~ m -> m -> m
  coapply f = Day id id (\x y -> f (x <> y))

Non-example

Unlike Env or Traced, Store comonad can't be an instance of Comonoid. The law requires any lawful Comonoid f to satisfy the following property.

• For any value of f x, coapply doesn't change the "shape" of it. Precisely, for any value fx :: f x, the following equation is true.

  () <$ coapply fx ≡ Day (() <$ fx) (() <$ fx) (\_ _ -> ())@

Therefore, any lawful Comonoid (Store s) must satisfy the following equation:

coapply (store u s0) ≡ Day (store u s0) (store u s0) (\_ _ -> ())
  where u = const () :: s -> ()

But it's incompatible with another requirement that duplicateDefault must be equivalent to duplicate of the Comonad (Store s) instance.

duplicateDefault (store u s0) = store (const (store u s0)) s0
duplicate        (store u s0) = store (\s1 -> store u s1)  s0

erase1 = elim1 . trans1 (Identity . extract)

erase2 = elim2 . trans2 (Identity . extract)

Every Comonoid is a Comonad.

Every Comonoid is a Comonad.

Day f g can be turned into a composition of f and g.

There are two ways to define a comonad:

I. Provide definitions for extract and extend satisfying these laws:

extend extract      = id
extract . extend f  = f
extend f . extend g = extend (f . extend g)

In this case, you may simply set fmap = liftW.

These laws are directly analogous to the laws for monads and perhaps can be made clearer by viewing them as laws stating that Cokleisli composition must be associative, and has extract for a unit:

f =>= extract   = f
extract =>= f   = f
(f =>= g) =>= h = f =>= (g =>= h)

II. Alternately, you may choose to provide definitions for fmap, extract, and duplicate satisfying these laws:

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

In this case you may not rely on the ability to define fmap in terms of liftW.

You may of course, choose to define both duplicate and extend. In that case you must also satisfy these laws:

extend f  = fmap f . duplicate
duplicate = extend id
fmap f    = extend (f . extract)

These are the default definitions of extend and duplicate and the definition of liftW respectively.