{-# language ConstraintKinds #-}
{-# language DataKinds #-}
{-# language DefaultSignatures #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language FunctionalDependencies #-}
{-# language GADTs #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language KindSignatures #-}
{-# language MultiParamTypeClasses #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

module IO.Effects.Internal ( Effect, Program(..), Member(..), ProgramWithHandler, interpret, Handled, HandlerInScope ) where

import Data.Coerce ( Coercible, coerce )
import Unsafe.Coerce ( unsafeCoerce )

class ( forall x y a. Coercible ( e ( Program x ) a ) ( e ( Program y ) a ) ) => Effect e where
  coerceEffect :: e ( Program x ) a -> e ( Program y ) a

  {-# inline coerceEffect #-}
  default coerceEffect :: Coercible ( e ( Program x ) a ) ( e ( Program y ) a ) => e ( Program x ) a -> e ( Program y ) a
  coerceEffect =
    coerce


instance ( forall x y a. Coercible ( e ( Program x ) a ) ( e ( Program y ) a ) ) => Effect e where


newtype Tagged a b =
  Tagged b


class HandlerInScope s e es | s -> e es where
  reflect :: Tagged s ( Handler e es )


data Skolem


newtype Magic e es r =
  Magic ( HandlerInScope Skolem e es => Tagged Skolem r )


{-# inline withHandler #-}
withHandler
  :: forall e es r.
     Handler e es
  -> ( forall s. HandlerInScope s e es => Tagged s r )
  -> r
withHandler a k =
  unsafeCoerce ( Magic k :: Magic e es r ) a


-- | A @Handled@ effect has the same capabilities as the effect @e@, but this
-- provides evidence to GHC that an effect handler for this effect is in scope.
newtype Handled e s m a =
  Handled ( e ( m :: * -> * ) a )

-- | The @Program@ monad is where you will type your effectful programs. The
-- parameter @es@ is an /effect list/ - the list of all possible effects that
-- your program has access to.
--
-- When writing computations in the @Program@ monad, you should keep @es@
-- polymorphic and add constraints using the 'Member' type class. For example,
-- prefer:
--
-- @
-- myApp :: Member HTTP es => Program es a
-- @
--
-- over
--
-- @
-- myApp :: Program ( HTTP : es ) a
-- @
--
-- as the former is much more composable.
newtype Program ( es :: [ ( * -> * ) -> * -> * ] ) a =
  Program
    { programToIO :: IO a
      -- ^ Any @Program@ can be reduced at any time to 'IO', at which point all
      -- in scope handlers will be used to provide interpretations to the
      -- effects in @es@.
    }
  deriving
    ( Functor, Applicative, Monad )


-- | You provide an interpretation of an individual effect using @interpret@.
{-# inline interpret #-}
interpret
  :: Effect e
  => ( forall x. e ( Program es ) x -> Program es x )
     -- ^ This function pattern matches on the effect signature @e@, and
     -- interprets each individual effect method into a program with access
     -- to the effects in the effect list @es@.
  -> ProgramWithHandler e es a
     -- ^ The program to supply this interpretation to.
  -> Program es a
interpret f p =
  withHandler ( Nat ( f . coerceEffect ) ) ( reduceAndTag p )

  where

    reduceAndTag :: forall s e es a. Program ( Handled e s ': es ) a -> Tagged s ( Program es a )
    reduceAndTag =
      coerce


-- | A 'Handler' of the effect 'e' using effects in the effect set 'es'.
newtype Handler e es =
  Nat ( forall a s. e ( Program ( Handled e s ': es ) ) a -> Program es a )


-- | A @ProgramWithHandler e es@ computation similar to a normal
-- @Program ( e : es)@ computation, but with the added information that an
-- effect handler for @e@ is in scope.
--
-- You will typically not write programs with this type, but you will use it
-- whenever you provide an interpretation using 'interpret'.
type ProgramWithHandler e es a =
  forall s. HandlerInScope s e es => Program ( Handled e s ': es ) a


-- | The @Member e es@ constraint witnesses that the effect @e@ can be found
-- in the effect list @es@.
class Member e es where
  -- | Send a single effect method call into a @Program@.
  send :: e ( Program es ) a -> Program es a


instance {-# overlaps #-} ( Effect e, HandlerInScope s e es ) => Member e ( Handled e s ': es ) where
  {-# inline send #-}
  send e =
    case reflect @s of
      Tagged ( Nat f ) ->
        coerce ( f e )


instance {-# overlaps #-} ( Effect e, Member e es ) => Member e ( f ': es ) where
  {-# inline send #-}
  send e =
    coerce ( send ( toEs e ) )

    where

      toEs :: forall a. e ( Program ( f ': es ) ) a -> e ( Program es ) a
      toEs =
        coerceEffect