{-# 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_ :: Reified tag c m -> (forall (m' :: * -> *). c m' => m' a) -> m a
interpret_ = forall k (tag :: k) (cs :: [Capability]) (c :: Capability)
       (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
forall (m :: * -> *) a.
(Monad m, All '[] m,
 forall s. Reifies s (Reified tag c m) => c (Reflected s c m)) =>
Reified tag c m
-> (forall (m' :: * -> *). All '[c] m' => m' a) -> m a
interpret @tag @'[] @c
{-# 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 :: Reified tag c m
-> (forall (m' :: * -> *). All (c : cs) m' => m' a) -> m a
interpret Reified tag c m
dict forall (m' :: * -> *). All (c : cs) m' => m' a
action =
  Reified tag c m
-> (forall s. Reifies s (Reified tag c m) => Proxy s -> m a) -> m a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify Reified tag c m
dict ((forall s. Reifies s (Reified tag c m) => Proxy s -> m a) -> m a)
-> (forall s. Reifies s (Reified tag c m) => Proxy s -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \(Proxy s
_ :: Proxy s) ->
    (forall (m' :: * -> *). (All '[c] m', All cs m') => m' a) -> m a
forall (t :: (* -> *) -> * -> *) (derived :: [Capability])
       (ambient :: [Capability]) (m :: * -> *) a.
(forall x. Coercible (t m x) (m x), All derived (t m),
 All ambient m) =>
(forall (m' :: * -> *). (All derived m', All ambient m') => m' a)
-> m a
derive @(Reflected s c) @'[c] @cs forall (m' :: * -> *). All (c : cs) m' => m' a
forall (m' :: * -> *). (All '[c] m', All cs m') => m' a
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 (a -> Reflected s c m b -> Reflected s c m a
(a -> b) -> Reflected s c m a -> Reflected s c m b
(forall a b. (a -> b) -> Reflected s c m a -> Reflected s c m b)
-> (forall a b. a -> Reflected s c m b -> Reflected s c m a)
-> Functor (Reflected s c m)
forall a b. a -> Reflected s c m b -> Reflected s c m a
forall a b. (a -> b) -> Reflected s c m a -> Reflected s c m b
forall s (c :: Capability) (m :: * -> *) a b.
Functor m =>
a -> Reflected s c m b -> Reflected s c m a
forall s (c :: Capability) (m :: * -> *) a b.
Functor m =>
(a -> b) -> Reflected s c m a -> Reflected s c m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Reflected s c m b -> Reflected s c m a
$c<$ :: forall s (c :: Capability) (m :: * -> *) a b.
Functor m =>
a -> Reflected s c m b -> Reflected s c m a
fmap :: (a -> b) -> Reflected s c m a -> Reflected s c m b
$cfmap :: forall s (c :: Capability) (m :: * -> *) a b.
Functor m =>
(a -> b) -> Reflected s c m a -> Reflected s c m b
Functor, Functor (Reflected s c m)
a -> Reflected s c m a
Functor (Reflected s c m)
-> (forall a. a -> Reflected s c m a)
-> (forall a b.
    Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b)
-> (forall a b c.
    (a -> b -> c)
    -> Reflected s c m a -> Reflected s c m b -> Reflected s c m c)
-> (forall a b.
    Reflected s c m a -> Reflected s c m b -> Reflected s c m b)
-> (forall a b.
    Reflected s c m a -> Reflected s c m b -> Reflected s c m a)
-> Applicative (Reflected s c m)
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
Reflected s c m a -> Reflected s c m b -> Reflected s c m a
Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b
(a -> b -> c)
-> Reflected s c m a -> Reflected s c m b -> Reflected s c m c
forall a. a -> Reflected s c m a
forall a b.
Reflected s c m a -> Reflected s c m b -> Reflected s c m a
forall a b.
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
forall a b.
Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b
forall a b c.
(a -> b -> c)
-> Reflected s c m a -> Reflected s c m b -> Reflected s c m c
forall s (c :: Capability) (m :: * -> *).
Applicative m =>
Functor (Reflected s c m)
forall s (c :: Capability) (m :: * -> *) a.
Applicative m =>
a -> Reflected s c m a
forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m a
forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b
forall s (c :: Capability) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Reflected s c m a -> Reflected s c m b -> Reflected s c m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Reflected s c m a -> Reflected s c m b -> Reflected s c m a
$c<* :: forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m a
*> :: Reflected s c m a -> Reflected s c m b -> Reflected s c m b
$c*> :: forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
liftA2 :: (a -> b -> c)
-> Reflected s c m a -> Reflected s c m b -> Reflected s c m c
$cliftA2 :: forall s (c :: Capability) (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Reflected s c m a -> Reflected s c m b -> Reflected s c m c
<*> :: Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b
$c<*> :: forall s (c :: Capability) (m :: * -> *) a b.
Applicative m =>
Reflected s c m (a -> b) -> Reflected s c m a -> Reflected s c m b
pure :: a -> Reflected s c m a
$cpure :: forall s (c :: Capability) (m :: * -> *) a.
Applicative m =>
a -> Reflected s c m a
$cp1Applicative :: forall s (c :: Capability) (m :: * -> *).
Applicative m =>
Functor (Reflected s c m)
Applicative, Applicative (Reflected s c m)
a -> Reflected s c m a
Applicative (Reflected s c m)
-> (forall a b.
    Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b)
-> (forall a b.
    Reflected s c m a -> Reflected s c m b -> Reflected s c m b)
-> (forall a. a -> Reflected s c m a)
-> Monad (Reflected s c m)
Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
forall a. a -> Reflected s c m a
forall a b.
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
forall a b.
Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b
forall s (c :: Capability) (m :: * -> *).
Monad m =>
Applicative (Reflected s c m)
forall s (c :: Capability) (m :: * -> *) a.
Monad m =>
a -> Reflected s c m a
forall s (c :: Capability) (m :: * -> *) a b.
Monad m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
forall s (c :: Capability) (m :: * -> *) a b.
Monad m =>
Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Reflected s c m a
$creturn :: forall s (c :: Capability) (m :: * -> *) a.
Monad m =>
a -> Reflected s c m a
>> :: Reflected s c m a -> Reflected s c m b -> Reflected s c m b
$c>> :: forall s (c :: Capability) (m :: * -> *) a b.
Monad m =>
Reflected s c m a -> Reflected s c m b -> Reflected s c m b
>>= :: Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b
$c>>= :: forall s (c :: Capability) (m :: * -> *) a b.
Monad m =>
Reflected s c m a -> (a -> Reflected s c m b) -> Reflected s c m b
$cp1Monad :: forall s (c :: Capability) (m :: * -> *).
Monad m =>
Applicative (Reflected s c m)
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 :: Reified tag c m
reified = Proxy s -> Reified tag c m
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s
forall k (t :: k). Proxy t
Proxy @s)
{-# INLINE reified #-}