{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Description: The 'Tagged' effect and its interpreters
module Polysemy.Tagged
  (
    -- * Effect
    Tagged (..)

    -- * Actions
  , tag
  , tagged

    -- * Interpretations
  , untag
  , retag
  ) where

import Polysemy
import Polysemy.Internal
import Polysemy.Internal.Union


------------------------------------------------------------------------------
-- | An effect for annotating effects and disambiguating identical effects.
newtype Tagged k e m a where
  Tagged :: forall k e m a. e m a -> Tagged k e m a


------------------------------------------------------------------------------
-- | Tag uses of an effect, effectively gaining access to the
-- tagged effect locally.
--
-- This may be used to create @tagged-@ variants of regular actions.
--
-- For example:
--
-- @
-- taggedLocal :: forall k i r a
--              . 'Member' ('Tagged' k ('Polysemy.Reader.Reader' i)) r
--             => (i -> i)
--             -> 'Sem' r a
--             -> 'Sem' r a
-- taggedLocal f m =
--   'tag' \@k \@('Polysemy.Reader.Reader' i) $ 'Polysemy.Reader.local' @i f ('raise' m)
-- @
--
tag
    :: forall k e r a
     . Member (Tagged k e) r
    => Sem (e ': r) a
    -> Sem r a
tag :: forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Member (Tagged k e) r =>
Sem (e : r) a -> Sem r a
tag = forall (r :: EffectRow) (r' :: EffectRow) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem forall a b. (a -> b) -> a -> b
$ \Union (e : r) (Sem (e : r)) x
u -> case forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Union (e : r) m a -> Either (Union r m a) (Weaving e m a)
decomp Union (e : r) (Sem (e : r)) x
u of
  Right (Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> Sem (e : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) ->
    forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving (forall {k} {k} {k} (k :: k) (e :: k -> k -> *) (m :: k) (a :: k).
e m a -> Tagged k e m a
Tagged @k e (Sem rInitial) a
e) f ()
s (forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Member (Tagged k e) r =>
Sem (e : r) a -> Sem r a
tag @k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. f (Sem rInitial x) -> Sem (e : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
  Left Union r (Sem (e : r)) x
g -> forall (m :: * -> *) (n :: * -> *) (r :: EffectRow) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist (forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Member (Tagged k e) r =>
Sem (e : r) a -> Sem r a
tag @k) Union r (Sem (e : r)) x
g
{-# INLINE tag #-}


------------------------------------------------------------------------------
-- | A reinterpreting version of 'tag'.
tagged
    :: forall k e r a
     . Sem (e ': r) a
    -> Sem (Tagged k e ': r) a
tagged :: forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e : r) a -> Sem (Tagged k e : r) a
tagged = forall (r :: EffectRow) (r' :: EffectRow) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem forall a b. (a -> b) -> a -> b
$ \Union (e : r) (Sem (e : r)) x
u ->
  case forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a
       (f :: (* -> *) -> * -> *).
Union (e : r) m a -> Either (Union (f : r) m a) (Weaving e m a)
decompCoerce Union (e : r) (Sem (e : r)) x
u of
    Right (Weaving e (Sem rInitial) a
e f ()
s forall x. f (Sem rInitial x) -> Sem (e : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) ->
      forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving (forall {k} {k} {k} (k :: k) (e :: k -> k -> *) (m :: k) (a :: k).
e m a -> Tagged k e m a
Tagged @k e (Sem rInitial) a
e) f ()
s (forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e : r) a -> Sem (Tagged k e : r) a
tagged @k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. f (Sem rInitial x) -> Sem (e : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
    Left Union (Tagged k e : r) (Sem (e : r)) x
g -> forall (m :: * -> *) (n :: * -> *) (r :: EffectRow) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist (forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (e : r) a -> Sem (Tagged k e : r) a
tagged @k) Union (Tagged k e : r) (Sem (e : r)) x
g
{-# INLINE tagged #-}



------------------------------------------------------------------------------
-- | Run a @'Tagged' k e@ effect through reinterpreting it to @e@
untag
    :: forall k e r a
     . Sem (Tagged k e ': r) a
    -> Sem (e ': r) a
-- TODO(KingoftheHomeless): I think this is safe to replace with 'unsafeCoerce',
-- but doing so probably worsens performance, as it hampers optimizations.
-- Once GHC 8.10 rolls out, I will benchmark and compare.
untag :: forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (Tagged k e : r) a -> Sem (e : r) a
untag = forall (r :: EffectRow) (r' :: EffectRow) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem forall a b. (a -> b) -> a -> b
$ \Union (Tagged k e : r) (Sem (Tagged k e : r)) x
u -> case forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a
       (f :: (* -> *) -> * -> *).
Union (e : r) m a -> Either (Union (f : r) m a) (Weaving e m a)
decompCoerce Union (Tagged k e : r) (Sem (Tagged k e : r)) x
u of
  Right (Weaving (Tagged e (Sem rInitial) a
e) f ()
s forall x. f (Sem rInitial x) -> Sem (Tagged k e : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) ->
    forall (e :: (* -> *) -> * -> *) (r :: EffectRow)
       (mWoven :: * -> *) a.
ElemOf e r -> Weaving e mWoven a -> Union r mWoven a
Union forall {k} (r :: [k]) (e :: k) (r' :: [k]).
(r ~ (e : r')) =>
ElemOf e r
Here (forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving e (Sem rInitial) a
e f ()
s (forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (Tagged k e : r) a -> Sem (e : r) a
untag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. f (Sem rInitial x) -> Sem (Tagged k e : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins)
  Left Union (e : r) (Sem (Tagged k e : r)) x
g -> forall (m :: * -> *) (n :: * -> *) (r :: EffectRow) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist forall {k} (k :: k) (e :: (* -> *) -> * -> *) (r :: EffectRow) a.
Sem (Tagged k e : r) a -> Sem (e : r) a
untag Union (e : r) (Sem (Tagged k e : r)) x
g
{-# INLINE untag #-}


------------------------------------------------------------------------------
-- | Transform a @'Tagged' k1 e@ effect into a @'Tagged' k2 e@ effect
retag
    :: forall k1 k2 e r a
     . Member (Tagged k2 e) r
    => Sem (Tagged k1 e ': r) a
    -> Sem r a
retag :: forall {k} {k} (k1 :: k) (k2 :: k) (e :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Member (Tagged k2 e) r =>
Sem (Tagged k1 e : r) a -> Sem r a
retag = forall (r :: EffectRow) (r' :: EffectRow) a.
(forall x. Union r (Sem r) x -> Union r' (Sem r') x)
-> Sem r a -> Sem r' a
hoistSem forall a b. (a -> b) -> a -> b
$ \Union (Tagged k1 e : r) (Sem (Tagged k1 e : r)) x
u -> case forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Union (e : r) m a -> Either (Union r m a) (Weaving e m a)
decomp Union (Tagged k1 e : r) (Sem (Tagged k1 e : r)) x
u of
  Right (Weaving (Tagged e (Sem rInitial) a
e) f ()
s forall x. f (Sem rInitial x) -> Sem (Tagged k1 e : r) (f x)
wv f a -> x
ex forall x. f x -> Maybe x
ins) ->
    forall (e :: (* -> *) -> * -> *) (r :: EffectRow) (m :: * -> *) a.
Member e r =>
Weaving e m a -> Union r m a
injWeaving forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (e :: (* -> *) -> * -> *)
       (rInitial :: EffectRow) a resultType (mAfter :: * -> *).
Functor f =>
e (Sem rInitial) a
-> f ()
-> (forall x. f (Sem rInitial x) -> mAfter (f x))
-> (f a -> resultType)
-> (forall x. f x -> Maybe x)
-> Weaving e mAfter resultType
Weaving (forall {k} {k} {k} (k :: k) (e :: k -> k -> *) (m :: k) (a :: k).
e m a -> Tagged k e m a
Tagged @k2 e (Sem rInitial) a
e) f ()
s (forall {k} {k} (k1 :: k) (k2 :: k) (e :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Member (Tagged k2 e) r =>
Sem (Tagged k1 e : r) a -> Sem r a
retag @_ @k2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. f (Sem rInitial x) -> Sem (Tagged k1 e : r) (f x)
wv) f a -> x
ex forall x. f x -> Maybe x
ins
  Left Union r (Sem (Tagged k1 e : r)) x
g -> forall (m :: * -> *) (n :: * -> *) (r :: EffectRow) a.
(forall x. m x -> n x) -> Union r m a -> Union r n a
hoist (forall {k} {k} (k1 :: k) (k2 :: k) (e :: (* -> *) -> * -> *)
       (r :: EffectRow) a.
Member (Tagged k2 e) r =>
Sem (Tagged k1 e : r) a -> Sem r a
retag @_ @k2) Union r (Sem (Tagged k1 e : r)) x
g
{-# INLINE retag #-}