Coaction.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK show-extensions #-}

{-|
Module      : Control.Comonad.Coaction
Description : comonad coactions
Copyright   : © noiioiu
License     : LGPL-2
Maintainer  : noiioiu@cocaine.ninja
Stability   : experimental

Given a comonad \(W\) on a category \(\mathcal{D}\) with counit \(\varepsilon\) and
comultiplication \(\Delta\) and a functor \(F\) from \(\mathcal{C}\) to \(\mathcal{D}\),
a left (or outer) comonad coaction of \(W\) on \(F\) is a natural
transformation \(\Sigma: F \to W \circ F\) such that the following two laws hold:

* \((\varepsilon \circ F) \cdot \Sigma  = \mathrm{id}_F\)
* \((\Delta \circ F) \cdot \Sigma   = (W \circ \Sigma) \cdot \Sigma\)

We also say that \(F\) is a left comodule over \(W\).  In the
case \(\mathcal{C} = \mathcal{D}\), a left comonad comodule is a left comonoid
comodule object in the category of endofunctors on \(\mathcal{C}\). Right
(or inner) comonad coactions are defined similarly.
-}
module Control.Comonad.Coaction
  ( LeftComodule (..),
    RightComodule (..),
    BiComodule (..),
    ComonadTransStack (..),
  )
where

import Control.Comonad (Comonad (..))
import Control.Comonad.Density (Density (..))
import Control.Comonad.Env.Class (ComonadEnv (..))
import Control.Comonad.Identity (Identity (..))
import Control.Comonad.Store.Class (ComonadStore (..))
import Control.Comonad.Traced.Class (ComonadTraced (..))
import Control.Comonad.Trans.Store (Store, store)
import Control.Comonad.Trans.Traced (Traced, traced)
import Control.Comonad.TransformerStack (ComonadTransStack (..))
import Control.Monad (liftM2)
import Data.Functor.Compose (Compose (..))
import Data.Functor.Rep (Representable (..))
import Data.Functor.Sum (Sum (..))

{-| Instances must satisfy the following laws:

* @'duplicate' '.' 'lduplicate' = 'fmap' 'lduplicate' '.' 'lduplicate'@

* @'extract' '.' 'lduplicate' = 'id'@
-}
class (Comonad w, Functor f) => LeftComodule w f where
  lduplicate ::
    f a ->
    -- | left comonad coaction
    w (f a)
  lduplicate = lextend id
  lextend :: (f a -> b) -> f a -> w b
  lextend f = fmap f . lduplicate
  {-# MINIMAL lduplicate | lextend #-}

{-| Instances must satisfy the following laws:

* @'fmap' 'duplicate' '.' 'rduplicate' = 'rduplicate' '.' 'rduplicate'@

* @'fmap' 'extract' '.' 'lduplicate' = 'id'@
-}
class (Comonad w, Functor f) => RightComodule w f where
  rduplicate ::
    f a ->
    -- | right comonad coaction
    f (w a)
  rduplicate = rextend id
  rextend :: (w a -> b) -> f a -> f b
  rextend f = fmap f . rduplicate
  {-# MINIMAL rduplicate | rextend #-}

{-| Given two comonads @r@ and @s@, an @(r, s)@ bicomodule is a functor that is a left comodule over @r@ and a right comodule over @s@, where the two coactions are compatible.
  Instances must satisfy the following law in addition to the laws for @'LeftComodule'@ and @'RightComodule'@:

* @'lduplicate' '.' 'rduplicate' = 'fmap' 'rduplicate' '.' 'lduplicate' = 'biduplicate'@
-}
class (LeftComodule r f, RightComodule s f) => BiComodule r s f where
  biduplicate ::
    f a ->
    -- | two-sided comonad coaction
    r (f (s a))
  biduplicate = lduplicate . rduplicate

instance {-# INCOHERENT #-} (Comonad w) => LeftComodule Identity w where
  lduplicate = Identity

instance {-# INCOHERENT #-} (Comonad w) => RightComodule Identity w where
  rduplicate = fmap Identity

instance {-# INCOHERENT #-} (Comonad w) => BiComodule Identity Identity w where
  biduplicate = Identity . fmap Identity

instance {-# INCOHERENT #-} (Comonad w, Functor f, LeftComodule w v) => LeftComodule w (Compose v f) where
  lduplicate = fmap Compose . lduplicate . getCompose
  lextend f = lextend (f . Compose) . getCompose

instance {-# INCOHERENT #-} (Comonad w, Functor f, RightComodule w v) => RightComodule w (Compose f v) where
  rduplicate = Compose . fmap rduplicate . getCompose
  rextend f = Compose . fmap (rextend f) . getCompose

instance {-# INCOHERENT #-} (Comonad s, Comonad t, Functor f, LeftComodule s u, RightComodule t v) => BiComodule s t (Compose u (Compose f v))

{-| Proof that @f@ is always a left comodule over @t'Density' f@:

  * @   'duplicate' ('lduplicate' w)
      = 'duplicate' ('Density' 'id' w)
      = 'Density' ('Density' 'id') w
      = 'Density' 'lduplicate' w
      = 'fmap' 'lduplicate' ('Density' 'id' w)
      = 'fmap' 'lduplicate' ('lduplicate' w)@

  * @'extract' ('lduplicate' w) = 'extract' ('Density' 'id' w) = w@
-}
instance (Functor f) => LeftComodule (Density f) f where
  lduplicate = Density id

instance {-# INCOHERENT #-} (Comonad q, Comonad w, ComonadTransStack w q) => LeftComodule w q where
  lduplicate = lowerStack . duplicate
  lextend f = lowerStack . extend f

instance {-# INCOHERENT #-} (Comonad q, Comonad w, ComonadTransStack w q) => RightComodule w q where
  rduplicate = lextend lowerStack
  rextend f = extend $ f . lowerStack

instance {-# INCOHERENT #-} (Comonad q, Comonad w, ComonadTransStack w q) => BiComodule w w q

instance {-# INCOHERENT #-} (ComonadStore s w) => LeftComodule (Store s) w where
  lduplicate = liftM2 store (flip peek) pos . duplicate
  lextend f = liftM2 store (flip peek) pos . extend f

-- instance {-# INCOHERENT #-} (ComonadStore s w) => RightComodule (Store s) w where
--   rduplicate = extend $ liftM2 store (flip peek) pos
--   rextend f = extend $ f . liftM2 store (flip peek) pos

-- instance {-# INCOHERENT #-} (ComonadStore s w) => BiComodule (Store s) (Store s) w

instance {-# INCOHERENT #-} (ComonadEnv e w) => LeftComodule ((,) e) w where
  lduplicate = liftM2 (,) ask extract . duplicate
  lextend f = liftM2 (,) ask extract . extend f

instance {-# INCOHERENT #-} (ComonadEnv e w) => RightComodule ((,) e) w where
  rduplicate = extend $ liftM2 (,) ask extract
  rextend f = extend $ f . liftM2 (,) ask extract

instance {-# INCOHERENT #-} (ComonadEnv e w) => BiComodule ((,) e) ((,) e) w

instance {-# INCOHERENT #-} (ComonadTraced m w, Monoid m) => LeftComodule (Traced m) w where
  lduplicate = traced . flip trace . duplicate
  lextend f = traced . flip trace . extend f

instance {-# INCOHERENT #-} (ComonadTraced m w, Monoid m) => RightComodule (Traced m) w where
  rduplicate = extend $ traced . flip trace
  rextend f = extend $ f . traced . flip trace

instance {-# INCOHERENT #-} (ComonadTraced m w, Monoid m) => BiComodule (Traced m) (Traced m) w

instance {-# INCOHERENT #-} (LeftComodule w f, LeftComodule w g) => LeftComodule w (Sum f g) where
  lduplicate = \case
    InL x -> InL <$> lduplicate x
    InR x -> InR <$> lduplicate x
  lextend f = \case
    InL x -> lextend @w (f . InL) x
    InR x -> lextend @w (f . InR) x

instance {-# INCOHERENT #-} (RightComodule w f, RightComodule w g) => RightComodule w (Sum f g) where
  rduplicate = \case
    InL x -> InL $ rduplicate x
    InR x -> InR $ rduplicate x
  rextend f = \case
    InL x -> InL $ rextend @w f x
    InR x -> InR $ rextend @w f x

instance {-# INCOHERENT #-} (BiComodule w q f, BiComodule w q g) => BiComodule w q (Sum f g) where
  biduplicate = \case
    InL x -> InL <$> biduplicate x
    InR x -> InR <$> biduplicate x

instance (Representable f, Rep f ~ s) => RightComodule (Store s) f where
  rduplicate = tabulate . store . index