Example.hs

{-# language BlockArguments #-}
{-# language FlexibleContexts #-}
{-# language GADTs #-}
{-# language ImpredicativeTypes #-}
{-# language LambdaCase #-}
{-# language PolyKinds #-}
{-# language RankNTypes #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}

{-# options_ghc -ddump-simpl -dsuppress-all #-}

module Example ( test ) where

import Data.Functor.Identity
import Control.Monad.Trans.Except ( ExceptT(..), runExceptT )
import Reflected


data Error e m a where
  Throw :: e -> Error e m a
  TryCatch :: m a -> ( e -> m a ) -> Error e m a


instance AnEffect ( Error e ) where
  handle2 ctx eta = \case
    Throw e ->
      Coyoneda ( <$ ctx ) ( Throw e )

    TryCatch m f ->
      Coyoneda id ( TryCatch ( eta ( m <$ ctx ) ) ( eta . ( <$ ctx ) . f ) )


runError
  :: forall e a m g.
     ( Effect g, Carrier g m )
  => ( forall s. Reifies s ( Handler ( Error e + g ) ( ExceptT e m ) ) => Program ( Error e + g ) ( ScopedT s ( ExceptT e m ) ) a
     )
  -> m ( Either e a )
runError =
  interpretT runExceptT ( either ( return . Left ) runExceptT ) \case
    Throw e ->
      ExceptT ( return ( Left e ) )

    TryCatch m f ->
      ExceptT $ runExceptT m >>= \case
        Left e -> runExceptT ( f e )
        Right ok -> return ( Right ok )


test
  :: ( forall s. Reifies s ( Handler ( Error Bool + Pure ) ( ExceptT Bool Identity ) )
         => Program ( Error Bool + Pure ) ( ScopedT s ( ExceptT Bool Identity ) ) Bool
     )
  -> Either Bool Bool
test p =
  run . runError $ p

Reflected.hs

{-# language BlockArguments #-}
{-# language EmptyCase #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
{-# language GADTs #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language LambdaCase #-}
{-# language PolyKinds #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

{-# options_ghc -Wall -fwarn-redundant-constraints #-}

module Reflected where

import Data.Tuple ( swap )
import Control.Monad.Trans.Except ( ExceptT(..), runExceptT )
import Control.Monad.Trans.State.Strict ( StateT(..) )
import Data.Coerce ( coerce )
import Data.Functor.Identity
import Unsafe.Coerce ( unsafeCoerce )


-- monad-trans-control, but functorially

class ( Functor f, forall m. Monad m => ( Monad ( t m ) ) ) => Transformer t f | t -> f where
  liftWithRun
    :: Monad m
    => ( ( forall x. t m x -> m ( f x ) ) -> m a )
    -> t m a

  restore :: Monad m => m ( f a ) -> t m a


instance Transformer ( ExceptT e ) ( Either e ) where
  liftWithRun f =
    ExceptT ( Right <$> f runExceptT )

  restore =
    ExceptT


instance Transformer ( StateT s ) ( (,) s ) where
  liftWithRun f =
    StateT ( \s -> (,) <$> f ( \( StateT g ) -> swap <$> g s ) <*> pure s )

  restore m =
    StateT ( \_ -> swap <$> m )



-- Programs

newtype Program sig carrier a =
  Program { runProgram :: carrier a }
  deriving
    ( Functor, Applicative, Monad )



interpretT
  :: forall e m g a t f.
     ( Transformer t f, AnEffect e, Carrier g m, Effect g )
  => ( forall x. t m x -> m ( f x ) )
  -> ( forall x. f ( t m x ) -> m ( f x ) )
  -> ( forall x. e ( t m ) x -> t m x )
  -> ( forall s. Reifies s ( Handler ( e + g ) ( t m ) ) => Program ( e + g ) ( ScopedT s ( t m ) ) a )
  -> m ( f a )
interpretT out distribute runOp p =
  reify ( Handler handler ) ( go p )

  where

    handler
      :: forall s x.
         ( e + g ) ( Program ( e + g ) ( ScopedT s ( t m ) ) ) x
      -> Program ( e + g ) ( ScopedT s ( t m ) ) x
    handler = \case
      L ( Coyoneda f a ) ->
        coerce $ fmap f $
        case handle2 ( Identity () ) ( fmap Identity . coerce ) a of
          Coyoneda g e ->
            runIdentity . g <$> runOp e

      R a -> Program $ ScopedT $ do
        ctx <-
          liftWithRun \f -> f ( return () )

        restore ( eff ( handle ctx ( distribute . fmap ( unScopedT . runProgram ) ) a ) )


    go
      :: forall x s.
         Program ( e + g ) ( ScopedT s ( t m ) ) x
      -> Tagged s ( m ( f x ) )
    go p' =
      Tagged ( out ( coerce ( p' :: Program ( e + g ) ( ScopedT s ( t m ) ) x ) ) )


newtype ScopedT ( s :: * ) m a =
  ScopedT { unScopedT :: m a }
  deriving
    ( Functor, Applicative, Monad)



-- Coyoneda


data Coyoneda f a where
  Coyoneda :: ( a -> b ) -> f a -> Coyoneda f b


instance Functor ( Coyoneda f ) where
  fmap f ( Coyoneda g a ) =
    Coyoneda ( f . g ) a



-- Effect sums


data ( f + g ) m a =
  L ( Coyoneda ( f m ) a ) | R ( g m a )


class Member e sig where
  inj :: e m a -> sig m a


instance {-# overlaps #-} Member e ( e + f ) where
  inj =
    L . Coyoneda id


instance {-# overlappable #-} Member e g => Member e ( f + g ) where
  inj = R . inj



-- Reified handlers for signatures


newtype Handler sig m =
  Handler
    { runHandler
        :: forall s a. sig ( Program sig ( ScopedT s m ) ) a
        -> Program sig ( ScopedT s m ) a
    }



-- reflection


newtype Tagged a b =
  Tagged { unTag :: b }


class Reifies ( s :: * ) a | s -> a where
  reflect :: Tagged s a


data Skolem


newtype Magic a r =
  Magic ( Reifies Skolem a => Tagged Skolem r )


reify :: forall a r. a -> ( forall s. Reifies s a => Tagged s r ) -> r
reify a k =
  unsafeCoerce ( Magic @a k ) a



-- Carriers

class Monad m => Carrier sig m | m -> sig where
  eff :: sig m a -> m a


instance ( Monad m, Reifies s ( Handler sig m ) ) => Carrier sig ( Program sig ( ScopedT s m ) ) where
  eff =
    runHandler ( unTag ( reflect @s ) )



-- Effects


class Effect e where
  handle
    :: ( Functor f )
    => f ()
    -> ( forall x. f ( m x ) -> n ( f x ) )
    -> e m a
    -> e n ( f a )


class AnEffect e where
  handle2
    :: ( Functor f )
    => f ()
    -> ( forall x. f ( m x ) -> n ( f x ) )
    -> e m a
    -> Coyoneda ( e n ) ( f a )


instance ( AnEffect f, Effect g ) => Effect ( f + g ) where
  handle ctx eta = \case
    L ( Coyoneda f a ) ->
      L ( fmap ( fmap f ) ( handle2 ctx eta a ) )

    R a ->
      R ( handle ctx eta a )



-- PURE

data Pure m a


instance Effect Pure where
  handle _ _ = \case {}


instance Carrier Pure Identity where
  eff = \case {}


run :: Identity a -> a
run p =
  coerce p



-- STATE

data State s m a where
  Get :: State s m s
  Put :: s -> State s m ()


instance AnEffect ( State s ) where
  handle2 ctx _ = \case
    Get -> Coyoneda ( <$ ctx ) Get
    Put s -> Coyoneda ( <$ ctx ) ( Put s )


get :: ( Carrier sig m, Member ( State s ) sig ) => m s
get =
  eff ( inj Get )


put :: ( Carrier sig m, Member ( State s ) sig ) => s -> m ()
put s =
  eff ( inj ( Put s ) )


modify :: ( Carrier sig m, Member ( State s ) sig ) => ( s -> s ) -> m ()
modify f =
  get >>= put . f


{-# inline execState #-}
execState
  :: forall s m sig a.
     ( Carrier sig m, Effect sig )
  => s
  -> ( forall x. Reifies x ( Handler ( State s + sig ) ( StateT s m ) ) => Program ( State s + sig ) ( ScopedT x ( StateT s m ) ) a )
  -> m s
execState s0 p =
  fmap fst $
  interpretT
    ( \m -> swap <$> runStateT m s0 )
    ( \( s, m ) -> swap <$> runStateT m s )
    ( \case
        Get ->
          StateT ( \s -> return ( s, s ) )

        Put s' ->
          StateT ( \_ -> return ( (), s' ) )
    )
    p


-- WRITER

data Writer w m a where
  Tell :: w -> Writer w m ()


instance AnEffect ( Writer w ) where
  handle2 ctx _ ( Tell w ) = Coyoneda ( <$ ctx ) ( Tell w )


tell :: ( Carrier sig m, Member ( Writer w ) sig ) => w -> m ()
tell =
  eff . inj . Tell


{-# inline execWriter #-}
execWriter
  :: forall w m sig a.
     ( Monoid w, Carrier sig m, Effect sig )
  => ( forall x. Reifies x ( Handler ( Writer w + sig ) ( StateT w m ) ) => Program ( Writer w + sig ) ( ScopedT x ( StateT w m ) ) a )
  -> m w
execWriter p =
  fmap fst $
  interpretT
    ( \m -> swap <$> runStateT m mempty )
    ( \( w, s ) -> swap <$> runStateT s w )
    ( \case
        Tell w ->
          StateT ( \s -> return ( (), s <> w ) )
    )
    p