{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE DeriveFoldable            #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE Rank2Types                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE IncoherentInstances       #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.HFunctor
-- Copyright   :  Original (c) 2011 Patrick Bahr; modifications (c) 2020 James Koppel
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines higher-order functors (Johann, Ghani, POPL
-- '08), i.e. endofunctors on the category of endofunctors.
--
--------------------------------------------------------------------------------

module Data.Comp.Multi.HFunctor
    (
     HFunctor (..),
     (:->),
     (:=>),
     NatM,
     I (..),
     K (..),
     A (..),
     E (..),
     runE,
     rewriteE,
     rewriteEM,
     (:.:)(..),
     HMonad(..)
     ) where

import Data.Functor.Compose
import Data.Comp.Multi.Kinds

-- | The identity Functor.
newtype I a = I {forall a. I a -> a
unI :: a} deriving ((forall a b. (a -> b) -> I a -> I b)
-> (forall a b. a -> I b -> I a) -> Functor I
forall a b. a -> I b -> I a
forall a b. (a -> b) -> I a -> I b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> I a -> I b
fmap :: forall a b. (a -> b) -> I a -> I b
$c<$ :: forall a b. a -> I b -> I a
<$ :: forall a b. a -> I b -> I a
Functor, (forall m. Monoid m => I m -> m)
-> (forall m a. Monoid m => (a -> m) -> I a -> m)
-> (forall m a. Monoid m => (a -> m) -> I a -> m)
-> (forall a b. (a -> b -> b) -> b -> I a -> b)
-> (forall a b. (a -> b -> b) -> b -> I a -> b)
-> (forall b a. (b -> a -> b) -> b -> I a -> b)
-> (forall b a. (b -> a -> b) -> b -> I a -> b)
-> (forall a. (a -> a -> a) -> I a -> a)
-> (forall a. (a -> a -> a) -> I a -> a)
-> (forall a. I a -> [a])
-> (forall a. I a -> Bool)
-> (forall a. I a -> Int)
-> (forall a. Eq a => a -> I a -> Bool)
-> (forall a. Ord a => I a -> a)
-> (forall a. Ord a => I a -> a)
-> (forall a. Num a => I a -> a)
-> (forall a. Num a => I a -> a)
-> Foldable I
forall a. Eq a => a -> I a -> Bool
forall a. Num a => I a -> a
forall a. Ord a => I a -> a
forall m. Monoid m => I m -> m
forall a. I a -> Bool
forall a. I a -> Int
forall a. I a -> [a]
forall a. (a -> a -> a) -> I a -> a
forall m a. Monoid m => (a -> m) -> I a -> m
forall b a. (b -> a -> b) -> b -> I a -> b
forall a b. (a -> b -> b) -> b -> I a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => I m -> m
fold :: forall m. Monoid m => I m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> I a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> I a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> I a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> I a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> I a -> b
foldr :: forall a b. (a -> b -> b) -> b -> I a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> I a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> I a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> I a -> b
foldl :: forall b a. (b -> a -> b) -> b -> I a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> I a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> I a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> I a -> a
foldr1 :: forall a. (a -> a -> a) -> I a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> I a -> a
foldl1 :: forall a. (a -> a -> a) -> I a -> a
$ctoList :: forall a. I a -> [a]
toList :: forall a. I a -> [a]
$cnull :: forall a. I a -> Bool
null :: forall a. I a -> Bool
$clength :: forall a. I a -> Int
length :: forall a. I a -> Int
$celem :: forall a. Eq a => a -> I a -> Bool
elem :: forall a. Eq a => a -> I a -> Bool
$cmaximum :: forall a. Ord a => I a -> a
maximum :: forall a. Ord a => I a -> a
$cminimum :: forall a. Ord a => I a -> a
minimum :: forall a. Ord a => I a -> a
$csum :: forall a. Num a => I a -> a
sum :: forall a. Num a => I a -> a
$cproduct :: forall a. Num a => I a -> a
product :: forall a. Num a => I a -> a
Foldable, Functor I
Foldable I
(Functor I, Foldable I) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> I a -> f (I b))
-> (forall (f :: * -> *) a. Applicative f => I (f a) -> f (I a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> I a -> m (I b))
-> (forall (m :: * -> *) a. Monad m => I (m a) -> m (I a))
-> Traversable I
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => I (m a) -> m (I a)
forall (f :: * -> *) a. Applicative f => I (f a) -> f (I a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> I a -> m (I b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> I a -> f (I b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> I a -> f (I b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> I a -> f (I b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => I (f a) -> f (I a)
sequenceA :: forall (f :: * -> *) a. Applicative f => I (f a) -> f (I a)
$cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> I a -> m (I b)
mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> I a -> m (I b)
$csequence :: forall (m :: * -> *) a. Monad m => I (m a) -> m (I a)
sequence :: forall (m :: * -> *) a. Monad m => I (m a) -> m (I a)
Traversable)


-- | The parametrised constant functor.
newtype K a i = K {forall a i. K a i -> a
unK :: a} deriving ((forall a b. (a -> b) -> K a a -> K a b)
-> (forall a b. a -> K a b -> K a a) -> Functor (K a)
forall a b. a -> K a b -> K a a
forall a b. (a -> b) -> K a a -> K a b
forall a a b. a -> K a b -> K a a
forall a a b. (a -> b) -> K a a -> K a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> K a a -> K a b
fmap :: forall a b. (a -> b) -> K a a -> K a b
$c<$ :: forall a a b. a -> K a b -> K a a
<$ :: forall a b. a -> K a b -> K a a
Functor, (forall m. Monoid m => K a m -> m)
-> (forall m a. Monoid m => (a -> m) -> K a a -> m)
-> (forall m a. Monoid m => (a -> m) -> K a a -> m)
-> (forall a b. (a -> b -> b) -> b -> K a a -> b)
-> (forall a b. (a -> b -> b) -> b -> K a a -> b)
-> (forall b a. (b -> a -> b) -> b -> K a a -> b)
-> (forall b a. (b -> a -> b) -> b -> K a a -> b)
-> (forall a. (a -> a -> a) -> K a a -> a)
-> (forall a. (a -> a -> a) -> K a a -> a)
-> (forall a. K a a -> [a])
-> (forall a. K a a -> Bool)
-> (forall a. K a a -> Int)
-> (forall a. Eq a => a -> K a a -> Bool)
-> (forall a. Ord a => K a a -> a)
-> (forall a. Ord a => K a a -> a)
-> (forall a. Num a => K a a -> a)
-> (forall a. Num a => K a a -> a)
-> Foldable (K a)
forall a. Eq a => a -> K a a -> Bool
forall a. Num a => K a a -> a
forall a. Ord a => K a a -> a
forall m. Monoid m => K a m -> m
forall a. K a a -> Bool
forall a. K a a -> Int
forall a. K a a -> [a]
forall a. (a -> a -> a) -> K a a -> a
forall a a. Eq a => a -> K a a -> Bool
forall a a. Num a => K a a -> a
forall a a. Ord a => K a a -> a
forall a m. Monoid m => K a m -> m
forall m a. Monoid m => (a -> m) -> K a a -> m
forall a a. K a a -> Bool
forall a a. K a a -> Int
forall a a. K a a -> [a]
forall b a. (b -> a -> b) -> b -> K a a -> b
forall a b. (a -> b -> b) -> b -> K a a -> b
forall a a. (a -> a -> a) -> K a a -> a
forall a m a. Monoid m => (a -> m) -> K a a -> m
forall a b a. (b -> a -> b) -> b -> K a a -> b
forall a a b. (a -> b -> b) -> b -> K a a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall a m. Monoid m => K a m -> m
fold :: forall m. Monoid m => K a m -> m
$cfoldMap :: forall a m a. Monoid m => (a -> m) -> K a a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> K a a -> m
$cfoldMap' :: forall a m a. Monoid m => (a -> m) -> K a a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> K a a -> m
$cfoldr :: forall a a b. (a -> b -> b) -> b -> K a a -> b
foldr :: forall a b. (a -> b -> b) -> b -> K a a -> b
$cfoldr' :: forall a a b. (a -> b -> b) -> b -> K a a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> K a a -> b
$cfoldl :: forall a b a. (b -> a -> b) -> b -> K a a -> b
foldl :: forall b a. (b -> a -> b) -> b -> K a a -> b
$cfoldl' :: forall a b a. (b -> a -> b) -> b -> K a a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> K a a -> b
$cfoldr1 :: forall a a. (a -> a -> a) -> K a a -> a
foldr1 :: forall a. (a -> a -> a) -> K a a -> a
$cfoldl1 :: forall a a. (a -> a -> a) -> K a a -> a
foldl1 :: forall a. (a -> a -> a) -> K a a -> a
$ctoList :: forall a a. K a a -> [a]
toList :: forall a. K a a -> [a]
$cnull :: forall a a. K a a -> Bool
null :: forall a. K a a -> Bool
$clength :: forall a a. K a a -> Int
length :: forall a. K a a -> Int
$celem :: forall a a. Eq a => a -> K a a -> Bool
elem :: forall a. Eq a => a -> K a a -> Bool
$cmaximum :: forall a a. Ord a => K a a -> a
maximum :: forall a. Ord a => K a a -> a
$cminimum :: forall a a. Ord a => K a a -> a
minimum :: forall a. Ord a => K a a -> a
$csum :: forall a a. Num a => K a a -> a
sum :: forall a. Num a => K a a -> a
$cproduct :: forall a a. Num a => K a a -> a
product :: forall a. Num a => K a a -> a
Foldable, Functor (K a)
Foldable (K a)
(Functor (K a), Foldable (K a)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> K a a -> f (K a b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    K a (f a) -> f (K a a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> K a a -> m (K a b))
-> (forall (m :: * -> *) a. Monad m => K a (m a) -> m (K a a))
-> Traversable (K a)
forall a. Functor (K a)
forall a. Foldable (K a)
forall a (m :: * -> *) a. Monad m => K a (m a) -> m (K a a)
forall a (f :: * -> *) a. Applicative f => K a (f a) -> f (K a a)
forall a (m :: * -> *) a b.
Monad m =>
(a -> m b) -> K a a -> m (K a b)
forall a (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> K a a -> f (K a b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => K a (m a) -> m (K a a)
forall (f :: * -> *) a. Applicative f => K a (f a) -> f (K a a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> K a a -> m (K a b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> K a a -> f (K a b)
$ctraverse :: forall a (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> K a a -> f (K a b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> K a a -> f (K a b)
$csequenceA :: forall a (f :: * -> *) a. Applicative f => K a (f a) -> f (K a a)
sequenceA :: forall (f :: * -> *) a. Applicative f => K a (f a) -> f (K a a)
$cmapM :: forall a (m :: * -> *) a b.
Monad m =>
(a -> m b) -> K a a -> m (K a b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> K a a -> m (K a b)
$csequence :: forall a (m :: * -> *) a. Monad m => K a (m a) -> m (K a a)
sequence :: forall (m :: * -> *) a. Monad m => K a (m a) -> m (K a a)
Traversable)

data E f = forall i. E {()
unE :: f i}

runE :: (f :=> b) -> E f -> b
runE :: forall (f :: * -> *) b. (f :=> b) -> E f -> b
runE f :=> b
f (E f i
x) = f i -> b
f :=> b
f f i
x

rewriteE :: (forall l. f l -> f l) -> E f -> E f
rewriteE :: forall (f :: * -> *). (forall l. f l -> f l) -> E f -> E f
rewriteE forall l. f l -> f l
f (E f i
x) = f i -> E f
forall (f :: * -> *) i. f i -> E f
E (f i -> f i
forall l. f l -> f l
f f i
x)

rewriteEM :: (Functor m) =>  (forall l. f l -> m (f l)) -> E f -> m (E f)
rewriteEM :: forall (m :: * -> *) (f :: * -> *).
Functor m =>
(forall l. f l -> m (f l)) -> E f -> m (E f)
rewriteEM forall l. f l -> m (f l)
f (E f i
x) = f i -> E f
forall (f :: * -> *) i. f i -> E f
E (f i -> E f) -> m (f i) -> m (E f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f i -> m (f i)
forall l. f l -> m (f l)
f f i
x

data A f = A {forall (f :: * -> *). A f -> forall i. f i
unA :: forall i. f i}

instance Eq a => Eq (K a i) where
    K a
x == :: K a i -> K a i -> Bool
== K a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y
    K a
x /= :: K a i -> K a i -> Bool
/= K a
y = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y

instance Ord a => Ord (K a i) where
    K a
x < :: K a i -> K a i -> Bool
< K a
y = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
    K a
x > :: K a i -> K a i -> Bool
> K a
y = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
y
    K a
x <= :: K a i -> K a i -> Bool
<= K a
y = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
y
    K a
x >= :: K a i -> K a i -> Bool
>= K a
y = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y
    min :: K a i -> K a i -> K a i
min (K a
x) (K a
y) = a -> K a i
forall a i. a -> K a i
K (a -> K a i) -> a -> K a i
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Ord a => a -> a -> a
min a
x a
y
    max :: K a i -> K a i -> K a i
max (K a
x) (K a
y) = a -> K a i
forall a i. a -> K a i
K (a -> K a i) -> a -> K a i
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Ord a => a -> a -> a
max a
x a
y
    compare :: K a i -> K a i -> Ordering
compare (K a
x) (K a
y) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y


infixr 0 :-> -- same precedence as function space operator ->
infixr 0 :=> -- same precedence as function space operator ->

-- | This type represents natural transformations.
type f :-> g = forall i . f i -> g i

-- | This type represents co-cones from @f@ to @a@. @f :=> a@ is
-- isomorphic to f :-> K a
type f :=> a = forall i . f i -> a


type NatM m f g = forall i. f i -> m (g i)

-- | This class represents higher-order functors (Johann, Ghani, POPL
-- '08) which are endofunctors on the category of endofunctors.
class HFunctor h where
    -- A higher-order functor @f@ maps every functor @g@ to a
    -- functor @f g@.
    --
    -- @ffmap :: (Functor g) => (a -> b) -> f g a -> f g b@
    --
    -- We omit this, as it does not work for GADTs (see Johand and
    -- Ghani 2008).

    -- | A higher-order functor @f@ also maps a natural transformation
    -- @g :-> h@ to a natural transformation @f g :-> f h@
    hfmap :: (f :-> g) -> h f :-> h g

instance (Functor f) => HFunctor (Compose f) where hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> Compose f f :-> Compose f g
hfmap f :-> g
f (Compose f (f i)
xs) = f (g i) -> Compose f g i
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose ((f i -> g i) -> f (f i) -> f (g i)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f i -> g i
f :-> g
f f (f i)
xs)

infixl 5 :.:

-- | This data type denotes the composition of two functor families.
data (:.:) (f :: Node) (g :: Node) e t = Comp (f (g e) t)

newtype HMonad m f i = HMonad { forall (m :: * -> *) (f :: * -> *) i. HMonad m f i -> m (f i)
unHMonad :: m (f i) }