content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE QuantifiedConstraints #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- | Use this module to provide an ad-hoc interpreter for a capability using
  -- type class reflection.
  --
  -- Use the functions 'interpret_' or 'interpret' for ad-hoc interpretation of
  -- capabilities.
  --
  -- Refer to 'Reflected' if you would like to enable reflection for a new
  -- capability.
  --
  -- More complex examples using this module can be found in the
  -- [Reflection example
  -- module](https://github.com/tweag/capability/blob/master/examples/Reflection.hs).
  --
  -- For details on reflection refer to the tutorial at
  -- <https://www.tweag.io/posts/2017-12-21-reflection-tutorial.html> and the
  -- @reflection@ library at <https://hackage.haskell.org/package/reflection>.
  
  module Capability.Reflection
    ( -- * Reflection
      interpret_
    , interpret
    , Reified
    , Reflected (..)
    , reified
      -- * Re-exported
    , Reifies
    , reify
    , reflect
    , Proxy (..)
    ) where
  
  import Capability.Constraints
  import Capability.Derive
  import Data.Kind (Type)
  import Data.Proxy
  import Data.Reflection
  
  -- | @interpret_ \@tag dict action@
  --
  -- Execute @action@ using the ad-hoc interpretation of a capability @c@ under
  -- @tag@ defined by @dict@, where @dict@ is a value of type @'Reified' tag c@,
  -- i.e. a record providing the implementation of the methods of capability @c@.
  --
  -- For example, the following provides an ad-hoc interpretation for the
  -- 'Capability.Source.HasSource' capability.
  --
  -- >>> :{
  --   interpret_ @"my-source"
  --     ReifiedSource { _await = pure "capabilities" }
  --     (replicateM 3 (await @"my-source"))
  --   :}
  -- ["capabilities", "capabilities", "capabilities"]
  interpret_ ::
    forall tag c m a.
    ( Monad m,
      forall s. Reifies s (Reified tag c m) => c (Reflected s c m)
    ) =>
    Reified tag c m ->
    (forall m'. c m' => m' a) ->
    m a
  interpret_ dict action = interpret @tag @'[] @c dict action
  {-# INLINE interpret_ #-}
  
  -- | @interpret \@tag \@ambient dict action@
  --
  -- Like 'interpret_' but forwards the ambient capabilities @ambient@ into the
  -- context of @action@ as well.
  --
  -- For example, the following provides an ad-hoc interpretation for the
  -- 'Capability.Source.HasSource' capability, while using an ambient
  -- 'Capability.Sink.HasSink' capability.
  --
  -- >>> :{
  --   interpret @"my-source" @'[HasSink "my-sink" String]
  --     ReifiedSource { _await = pure "capabilities" }
  --     (replicateM_ 3 (await @"my-source" >>= yield @"my-sink"))
  --   :}
  interpret ::
    forall tag (cs :: [Capability]) c m a.
    ( Monad m,
      All cs m,
      forall s. Reifies s (Reified tag c m) => c (Reflected s c m)
    ) =>
    Reified tag c m ->
    (forall m'. All (c ': cs) m' => m' a) ->
    m a
  interpret dict action =
    reify dict $ \(_ :: Proxy s) ->
      derive @(Reflected s c) @'[c] @cs action
  {-# INLINE interpret #-}
  
  -- | @Reified tag capability m@
  --
  -- Defines the dictionary type for the methods of @capability@ under @tag@ in
  -- the monad @m@. Refer to 'interpret_' for an example use-case.
  --
  -- For example, the 'Capability.Sink.HasSink' capability has the method
  -- @'Capability.Sink.yield' :: a -> m ()@. The corresponding dictionary type is
  -- defined as follows.
  --
  -- >>> :{
  --   data instance Reified tag (HasSink tag a) m =
  --     ReifiedSink { _yield :: forall a. a -> m () }
  --   :}
  --
  -- Superclass dictionaries are represented as nested records. For example, the
  -- 'Capability.State.HasState' capability has the superclasses
  -- 'Capability.Source.HasSource' and 'Capability.Sink.HasSink' and the method
  -- @'Capability.State.state' :: (s -> (a, s)) -> m a@. The corresponding
  -- dictionary type is defined as follows.
  --
  -- >>> :{
  --   data instance Reified tag (HasState tag s) m =
  --     ReifiedState
  --       { _stateSource :: Reified tag (HasSource tag s) m,
  --         _stateSink :: Reified tag (HasSink tag s) m,
  --         _state :: forall a. (s -> (a, s)) -> m a
  --       }
  --   :}
  data family Reified (tag :: k) (c :: Capability) (m :: Type -> Type)
  
  -- | @Reflected s capability m@
  --
  -- Carries the type class instance for @capability@ in the monad @m@ defined by
  -- the dictionary reflected in @s@ in the type system.
  --
  -- For most use-cases it is not necessary to use this type directly. Use
  -- 'interpret_' or 'interpret' instead.
  --
  -- If you wish to enable reflection for a new capability, then you will need to
  -- define a type class instance for @Reflected@ for the new capability. Note,
  -- you will also need to define an instance of 'Reified' which defines the
  -- dictionary type of the new capability. Hint, you can use @'reified' \@s@ to
  -- obtain the dictionary from the context in the instance implementation.
  --
  -- For example, the @Reflected@ instance for the 'Capability.Sink.HasSink'
  -- capability can be defined as follows. Assuming the dictionary described in
  -- 'Reified'.
  --
  -- >>> :{
  --   instance
  --     (Monad m, Reifies s (Reified tag (HasSink tag a) m)) =>
  --     HasSink tag a (Reflected s (HasSink tag a) m)
  --     where
  --     yield a = Reflect $ _yield (reified @s) a
  --   :}
  newtype Reflected (s :: Type) (c :: Capability) (m :: Type -> Type) (a :: Type) = Reflect (m a)
    deriving (Functor, Applicative, Monad)
  
  -- | @reified \@s@
  --
  -- Obtain the dictionary that is reflected in the type system under @s@.
  --
  -- This is a convenience wrapper around 'Data.Reflection.reflect'.
  reified :: forall s tag c m. Reifies s (Reified tag c m) => Reified tag c m
  reified = reflect (Proxy @s)
  {-# INLINE reified #-}
  