{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilyDependencies#-}
{-# LANGUAGE DefaultSignatures   #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ImpredicativeTypes  #-}
module Control.Applicative.Trans.Class(ApplicativeTrans(..)) where
import Data.Functor.Contravariant
import Data.Kind

import Data.Coerce
type FTransformer = ((Type -> Type) -> Type -> Type)

type FunctorTrans :: FTransformer -> Constraint
class (forall f. (Functor f) => Functor (hf f)) => FunctorTrans hf 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@
    liftNT :: forall f g a. (forall i. f i -> g i) -> hf f a -> hf g a


class (forall f. Applicative f => Applicative (hf f)) => ApplicativeTrans hf where
    liftPure :: f a -> hf f a
    (<^*^>) :: hf (f :-> g) a -> hf f a -> hf g a
    liftLiftA2 ::forall f1 f2 g a. (forall i. f1 i -> f2 i -> g i) -> hf f1 a -> hf f2 a -> hf g a
    default liftLiftA2 :: forall f1 f2 g a. (FunctorTrans hf) => (forall i. f1 i -> f2 i -> g i) -> hf f1 a -> hf f2 a -> hf g a
    liftLiftA2 f x = (<^*^>) (liftNT (coerce f :: (forall i. f1 i -> (f2 :-> g) i)) x)
type (:->):: (Type -> Type) -> (Type -> Type) -> (Type -> Type)
newtype (f :-> g) i = Comp (f i -> g i)
infixr 0 :->