{-# 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 = iextend id
iextend :: (f a ~~> b) -> (f a ~~> f b)
iextend f = imap f . iduplicate
{-# MINIMAL iextract, (iduplicate | iextend) #-}
instance IComonad (Product a) where
iextract (Pair _ b) = b
iduplicate (Pair a b) = Pair a (Pair a b)