{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}

module Data.IComonad
    ( IComonad (..)
    -- * Re-exports
    , module Data.IFunctor
    ) where

import           Data.Functor.Product (Product (Pair))
import           Data.IFunctor        (IFunctor (imap), type (~~>))

-- | Comonoid in the category of dependent endofunctors
class IFunctor f => IComonad f where
    iextract :: f a ~~> a
    iduplicate :: f a ~~> f (f a)
    iduplicate = (f a ~~> f a) -> f a ~~> f (f a)
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IComonad f =>
(f a ~~> b) -> f a ~~> f b
iextend f a ~~> f a
forall a. a -> a
id
    iextend :: (f a ~~> b) -> (f a ~~> f b)
    iextend f :: f a ~~> b
f = (f a ~~> b) -> f (f a) ~~> f b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap f a ~~> b
f (f (f a) ix -> f b ix)
-> (f a ix -> f (f a) ix) -> f a ix -> f b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a ix -> f (f a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate
    {-# MINIMAL iextract, (iduplicate | iextend) #-}

instance IComonad (Product a) where
    iextract :: Product a a ix -> a ix
iextract (Pair _ b :: a ix
b) = a ix
b
    iduplicate :: Product a a ix -> Product a (Product a a) ix
iduplicate (Pair a :: a ix
a b :: a ix
b) = a ix -> Product a a ix -> Product a (Product a a) ix
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair a ix
a (a ix -> a ix -> Product a a ix
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair a ix
a a ix
b)