InfiniteHigherOrderEffect.hs

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds, DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE UndecidableInstances #-}
module InfiniteHigherOrderEffect where

import Data.Kind (Type)
import Data.Functor.Contravariant (Contravariant)
import GHC.Generics hiding (type (:+:))
import qualified GHC.Generics

infix 7 ~>
type (~>) f g = forall x. f x -> g x

newtype
    HyperFree
        (f :: InsClass -> Type -> Type)
        (e :: ASigClass)
        (a :: Type) = HyperFree
    {unHyperFree :: (f (GetSigClass e (HyperFree f) e)) a}

type InsClass = Type -> Type
type SigClass = HyperFunctorClass -> ASigClass -> Type -> Type
type HyperFunctorClass = ASigClass -> Type -> Type
newtype ASigClass = ASigClass SigClass

type family GetSigClass (a :: ASigClass) where
    GetSigClass ('ASigClass e) = e

infixr 4 #
type f # e = f ('ASigClass e)

type SigMorphism :: SigClass -> SigClass -> Type
newtype SigMorphism e1 e2 = SigMorphism {
  runSigMorphism :: forall h e0.
       (HyperFunctor h, SFunctor e0) => (e1 h # e0) ~> (e2 h # e0)
  }

type HyperFunctorMorphism :: HyperFunctorClass -> HyperFunctorClass -> Type
newtype HyperFunctorMorphism h1 h2 = HyperFunctorMorphism {
    runHyperFunctorMorphism :: forall e.
      (SFunctor e) => (h1 # e) ~> (h2 # e)
  }

class HyperFunctor (h :: HyperFunctorClass) where
    hyfmap :: (SFunctor e1, SFunctor e2) => SigMorphism e1 e2 -> (h # e1) ~> (h # e2)

class SFunctor (e :: SigClass) where
    sfmap ::
        (HyperFunctor h, SFunctor e1, SFunctor e2) =>
        SigMorphism e1 e2 ->
        (e h # e1) ~> (e h # e2)
    transHyper ::
        (HyperFunctor h, HyperFunctor h', SFunctor e') =>
        HyperFunctorMorphism h h' ->
        (e h # e') ~> (e h' # e')

instance Freer f => HyperFunctor (HyperFree f) where
    hyfmap f (HyperFree a) = HyperFree (transFreer (sfmap f . runSigMorphism f) a)
    {-# INLINE hyfmap #-}

----

class Freer f where
    pureFreer :: a -> f c a
    wrapFreer :: c a -> (a -> f c b) -> f c b
    transFreer :: (c ~> d) -> (f c ~> f d)

type (+) = (GHC.Generics.:+:)

caseSum :: (f ~> h) -> (g ~> h) -> ((f + g) ~> h)
caseSum fh gh sumFG = case sumFG of
  L1 fx -> fh fx
  R1 gx -> gh gx

----

infixr 5 #+#, #+, +#, :+:

newtype LiftIns i h e a = LiftIns { unliftIns :: i a }
    deriving newtype (Generic, Generic1, Contravariant, Eq, Ord, Functor, Foldable)
    deriving stock (Traversable, Read, Show)

newtype
    (:+:)
        (e1 :: SigClass)
        (e2 :: SigClass)
        (h :: ASigClass -> Type -> Type)
        (e :: ASigClass)
        (a :: Type) = SumH {unSumH :: (e1 h e + e2 h e) a}
    deriving newtype (Generic, Generic1, Contravariant, Eq, Ord, Functor, Foldable)
    deriving stock (Traversable, Read, Show)

type (e1 :: SigClass) +# (e2 :: ASigClass) = 'ASigClass (e1 :+: GetSigClass e2)
type (e1 :: ASigClass) #+ (e2 :: SigClass) = 'ASigClass (GetSigClass e1 :+: e2)
type (e1 :: ASigClass) #+# (e2 :: ASigClass) = 'ASigClass (GetSigClass e1 :+: GetSigClass e2)

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

instance (SFunctor e1, SFunctor e2) => SFunctor (e1 :+: e2) where
    sfmap f = SumH . caseSum (L1 . sfmap f) (R1 . sfmap f) . unSumH
    {-# INLINE sfmap #-}

    transHyper f = SumH . caseSum (L1 . transHyper f) (R1 . transHyper f) . unSumH
    {-# INLINE transHyper #-}

data StateI s a where
    Put :: s -> StateI s ()
    Get :: StateI s s

data RunState s h e a where
    RunState :: h (LiftIns (StateI s) +# e) a -> RunState s h e (s, a)

instance SFunctor (RunState s) where
    sfmap f (RunState a) = RunState $
      hyfmap (SigMorphism $ SumH . caseSum L1 (R1 . runSigMorphism f) . unSumH) a
    transHyper f (RunState a) = RunState $ runHyperFunctorMorphism f a