SFunctorV3.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

module Control.Hefty where

import Control.Applicative (Alternative)
import Control.Effect.Class (LiftIns (LiftIns), NopS, unliftIns, type (~>))
import Control.Effect.Class.Except (CatchS)
import Control.Effect.Class.Machinery.HFunctor (HFunctor, caseH, hfmap, (:+:) (Inl, Inr))
import Control.Effect.Free (InsClass)
import Control.Freer (Freer, interpretFreer, liftIns, transformFreer)
import Control.Monad (MonadPlus)
import Control.Monad.Base (MonadBase)
import Control.Monad.IO.Class (MonadIO)
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))

newtype
    Hefty
        (f :: InsClass -> Type -> Type)
        (e :: SigClass)
        (a :: Type) = Hefty
    {unHefty :: f (e (Hefty f e)) a}

type SigClass = (Type -> Type) -> Type -> Type

deriving newtype instance Functor (f (e (Hefty f e))) => Functor (Hefty f e)
deriving newtype instance Applicative (f (e (Hefty f e))) => Applicative (Hefty f e)
deriving newtype instance Alternative (f (e (Hefty f e))) => Alternative (Hefty f e)
deriving newtype instance Monad (f (e (Hefty f e))) => Monad (Hefty f e)
deriving newtype instance MonadPlus (f (e (Hefty f e))) => MonadPlus (Hefty f e)
deriving newtype instance (MonadBase b (f (e (Hefty f e))), Monad b) => MonadBase b (Hefty f e)
deriving newtype instance MonadIO (f (e (Hefty f e))) => MonadIO (Hefty f e)
deriving newtype instance MonadFail (f (e (Hefty f e))) => MonadFail (Hefty f e)

deriving stock instance Foldable (f (e (Hefty f e))) => Foldable (Hefty f e)
deriving stock instance Traversable (f (e (Hefty f e))) => Traversable (Hefty f e)

deriving newtype instance Eq (f (e (Hefty f e)) a) => Eq (Hefty f e a)
deriving newtype instance Ord (f (e (Hefty f e)) a) => Ord (Hefty f e a)
deriving newtype instance Read (f (e (Hefty f e)) a) => Read (Hefty f e a)
deriving newtype instance Show (f (e (Hefty f e)) a) => Show (Hefty f e a)

overHefty ::
    (f (e (Hefty f e)) a -> f' (e' (Hefty f' e')) b) ->
    Hefty f e a ->
    Hefty f' e' b
overHefty f = Hefty . f . unHefty
{-# INLINE overHefty #-}

data ((e :: SigClass) +# (f :: Type -> Type)) (a :: Type) where
    HyperFunctorPlusT :: h (e :+: r) a -> (e +# h r) a

class HyperFunctor (h :: SigClass -> Type -> Type) where
    hyfmap :: (e (h e) ~> e' (h e')) -> h e ~> h e'

instance Freer c f => HyperFunctor (Hefty f) where
    hyfmap f = Hefty . transformFreer f . unHefty
    {-# INLINE hyfmap #-}

class SigConstraint c => SFunctor (c :: SigClass -> Constraint) (e :: SigClass) where
    sfmap ::
        (HyperFunctor h, SFunctor c e1, SFunctor c e2, c e1, c e2) =>
        (forall r. (SFunctor c r, c r) => h (r :+: e1) ~> h (r :+: e2)) ->
        e (h e1) ~> e (h e2)

type SigConstraint c = (c NopS, forall x1 x2. (c x1, c x2) => c (x1 :+: x2)) :: Constraint

hysfmap ::
    forall c e1 e2 h.
    ( SFunctor c e1
    , SFunctor c e2
    , c e1
    , c e2
    , HyperFunctor h
    ) =>
    (forall x. (SFunctor c x, c x) => e1 (h x) ~> e2 (h x)) ->
    h e1 ~> h e2
hysfmap f = hyfmap $ shyfmap @c f . f
{-# INLINE hysfmap #-}

shyfmap ::
    forall c e e1 e2 h.
    ( SFunctor c e
    , SFunctor c e1
    , SFunctor c e2
    , c e1
    , c e2
    , HyperFunctor h
    ) =>
    (forall x. (SFunctor c x, c x) => e1 (h x) ~> e2 (h x)) ->
    e (h e1) ~> e (h e2)
shyfmap f = sfmap @c $ hysfmap @c $ caseH Inl (Inr . f)
{-# INLINE shyfmap #-}

hsfmap ::
    forall c e e' h.
    (HyperFunctor h, SFunctor c e, SFunctor c e', c e, c e') =>
    (forall f. e f ~> e' f) ->
    h e ~> h e'
hsfmap f = hyfmap $ f . sfmap @c (rightHyperFunctor @c f)
{-# INLINE hsfmap #-}

rightHyperFunctor ::
    forall c l r r' h.
    (HyperFunctor h, SFunctor c l, SFunctor c r, SFunctor c r', c l, c r, c r') =>
    (forall e. (SFunctor c e, c e) => r (h (e :+: r')) ~> r' (h (e :+: r'))) ->
    h (l :+: r) ~> h (l :+: r')
rightHyperFunctor f =
    hyfmap $ caseH (Inl . sfmapR @c f) (Inr . f . sfmapR @c f)

sfmapR ::
    forall c e l r r' h.
    (HyperFunctor h, SFunctor c e, SFunctor c l, SFunctor c r, SFunctor c r', c l, c r, c r') =>
    (forall e'. (SFunctor c e', c e') => r (h (e' :+: r')) ~> r' (h (e' :+: r'))) ->
    e (h (l :+: r)) ~> e (h (l :+: r'))
sfmapR f =
    sfmap @c $
        assocHyperFunctorR @c
            . rightHyperFunctor @c f
            . assocHyperFunctorL @c

assocHyperFunctorL ::
    forall c e1 e2 e3 h.
    (HyperFunctor h, SFunctor c e1, SFunctor c e2, SFunctor c e3, c e1, c e2, c e3) =>
    h (e1 :+: (e2 :+: e3)) ~> h ((e1 :+: e2) :+: e3)
assocHyperFunctorL = hysfmap @c assocLSumH

assocHyperFunctorR ::
    forall c e1 e2 e3 h.
    (HyperFunctor h, SFunctor c e1, SFunctor c e2, SFunctor c e3, c e1, c e2, c e3) =>
    h ((e1 :+: e2) :+: e3) ~> h (e1 :+: (e2 :+: e3))
assocHyperFunctorR = hysfmap @c assocRSumH

instance SigConstraint c => SFunctor c (LiftIns e) where
    sfmap _ = LiftIns . unliftIns
    {-# INLINE sfmap #-}

instance
    (SFunctor c e1, SFunctor c e2) =>
    SFunctor c (e1 :+: e2)
    where
    sfmap f = caseH (Inl . sfmap @c f) (Inr . sfmap @c f)
    {-# INLINE sfmap #-}

newtype ViaHFunctor (e :: SigClass) f a = ViaHFunctor {unViaHFunctor :: e f a}
    deriving (HFunctor)

instance (HFunctor e, SigConstraint c) => SFunctor c (ViaHFunctor e) where
    sfmap f = hfmap $ absurdHyperFunctorL @c @NopS . f . weakenHyperFunctorL @c
    {-# INLINE sfmap #-}

absurdHyperFunctorL ::
    forall c l r h.
    ( HyperFunctor h
    , SFunctor c r
    , SFunctor c l
    , IsNopS l
    , c l
    , c r
    ) =>
    h (l :+: r) ~> h r
absurdHyperFunctorL = hsfmap @c $ caseH absurdNopS id
{-# INLINE absurdHyperFunctorL #-}

weakenHyperFunctorL ::
    forall c l r h.
    (HyperFunctor h, SFunctor c l, SFunctor c r, c l, c r) =>
    h r ~> h (l :+: r)
weakenHyperFunctorL = hsfmap @c Inr
{-# INLINE weakenHyperFunctorL #-}

class IsNopS (e :: SigClass) where
    absurdNopS :: e f a -> r

instance IsNopS NopS where
    absurdNopS = \case {}
    {-# INLINE absurdNopS #-}

instance (IsNopS e1, IsNopS e2) => IsNopS (e1 :+: e2) where
    absurdNopS = caseH absurdNopS absurdNopS
    {-# INLINE absurdNopS #-}

assocLSumH :: (e1 :+: (e2 :+: e3)) f ~> ((e1 :+: e2) :+: e3) f
assocLSumH = caseH (Inl . Inl) (caseH (Inl . Inr) Inr)

assocRSumH :: ((e1 :+: e2) :+: e3) f ~> (e1 :+: (e2 :+: e3)) f
assocRSumH = caseH (caseH Inl (Inr . Inl)) (Inr . Inr)

data RunCatch err m a where
    RunCatch :: (CatchS err +# m) a -> RunCatch err m (Either err a)

deriving via ViaHFunctor (CatchS err) instance SigConstraint c => SFunctor c (CatchS err)

instance
    ( c (CatchS err)
    , SigConstraint c
    ) =>
    SFunctor c (RunCatch err)
    where
    sfmap f (RunCatch (HyperFunctorPlusT a)) =
        RunCatch $ HyperFunctorPlusT $ f a
    {-# INLINE sfmap #-}

interpretR ::
    forall cs r l f cf.
    (Freer cf f, SFunctor cs l, SFunctor cs r, cs l, cs r) =>
    (forall x. (SFunctor cs x, cs x) => Proxy x -> r (Hefty f (x :+: l)) ~> Hefty f (x :+: l)) ->
    Hefty f (l :+: r) ~> Hefty f l
interpretR i =
    overHefty $
        interpretFreer $
            caseH
                (liftIns . sfmap @cs int)
                ( unHefty
                    . absurdHyperFunctorL @cs @NopS
                    . i Proxy
                    . sfmap @cs (hysfmap @cs (caseH Inl (Inr . Inr)) . int)
                )
  where
    int :: forall x. (SFunctor cs x, cs x) => Hefty f (x :+: (l :+: r)) ~> Hefty f (x :+: l)
    int =
        interpretR @cs @r
            ( \(_ :: Proxy x') ->
                hysfmap @cs @((x' :+: x) :+: l) assocRSumH
                    . i Proxy
                    . shyfmap @cs assocLSumH
            )
            . hysfmap @cs assocLSumH