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

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

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

import           Data.Functor.Product (Product (Pair))
import           Data.Functor.Sum     (Sum (InL, InR))
import           Data.IFunction       (type (~~>))

-- | Functor in the category of dependent types
class IFunctor f where
    imap :: (a ~~> b) -> (f a ~~> f b)

instance IFunctor (Sum a) where
    imap :: (a ~~> b) -> Sum a a ~~> Sum a b
imap _ (InL x :: a ix
x) = a ix -> Sum a b ix
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL a ix
x
    imap f :: a ~~> b
f (InR x :: a ix
x) = b ix -> Sum a b ix
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (a ix -> b ix
a ~~> b
f a ix
x)

instance IFunctor (Product a) where
    imap :: (a ~~> b) -> Product a a ~~> Product a b
imap f :: a ~~> b
f (Pair a :: a ix
a b :: a ix
b) = a ix -> b ix -> Product a b ix
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair a ix
a (a ix -> b ix
a ~~> b
f a ix
b)