{-# LANGUAGE AllowAmbiguousTypes #-}

-- SPDX-License-Identifier: MPL-2.0 AND BSD-3-Clause

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King; 2024 Sayo Koyoneda
License     :  MPL-2.0 (see the LICENSE file) AND BSD-3-Clause (see the LICENSE.BSD3 file)
Maintainer  :  ymdfield@outlook.jp

This module provides functions for interpretation.
Please refer to the documentation of the [top-level module]("Control.Monad.Hefty").
-}
module Control.Monad.Hefty.Interpret where

import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Monad ((>=>))
import Control.Monad.Hefty.Types (
    Eff (Op, Val),
    Elaborator,
    Interpreter,
    send0,
    sendUnion,
    sendUnionBy,
    sendUnionH,
    sendUnionHBy,
    type (~~>),
 )
import Data.Effect.HFunctor (HFunctor, hfmap)
import Data.Effect.OpenUnion.Internal (IsSuffixOf, WeakenN)
import Data.Effect.OpenUnion.Internal.FO (
    Member (prj),
    Union,
    extract,
    nil,
    weakenN,
    weakens,
    (!+),
    type (<|),
 )
import Data.Effect.OpenUnion.Internal.HO (
    MemberH (prjH),
    UnionH,
    extractH,
    hfmapUnion,
    nilH,
    weakenNH,
    weakensH,
    (!!+),
    type (<<|),
 )
import Data.FTCQueue (FTCQueue, ViewL (TOne, (:|)), tviewl, (><))

-- * Running t`Eff`

-- | Lowers the computation into a monad @m@ by treating the effect as a monad.
runEff :: (Monad m) => Eff '[] '[m] ~> m
runEff :: forall (m :: * -> *). Monad m => Eff '[] '[m] ~> m
runEff = (x -> m x) -> Interpreter m m x -> Eff '[] '[m] x -> m x
forall (e :: * -> *) (m :: * -> *) ans a.
Monad m =>
(a -> m ans) -> Interpreter e m ans -> Eff '[] '[e] a -> m ans
iterEffBy x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Interpreter m m x -> Eff '[] '[m] x -> m x)
-> Interpreter m m x -> Eff '[] '[m] x -> m x
forall a b. (a -> b) -> a -> b
$ (m ~> m) -> Interpreter m m x
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless m x -> m x
forall a. a -> a
m ~> m
id
{-# INLINE runEff #-}

-- | Extracts the value from a computation that contains only pure values without any effect.
runPure :: Eff '[] '[] a -> a
runPure :: forall a. Eff '[] '[] a -> a
runPure = \case
    Val a
x -> a
x
    Op Either (UnionH '[] (Eff '[] '[]) x) (Union '[] x)
u FTCQueue (Eff '[] '[]) x a
_ -> case Either (UnionH '[] (Eff '[] '[]) x) (Union '[] x)
u of
        Left UnionH '[] (Eff '[] '[]) x
u' -> UnionH '[] (Eff '[] '[]) x -> a
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH UnionH '[] (Eff '[] '[]) x
u'
        Right Union '[] x
u' -> Union '[] x -> a
forall a r. Union '[] a -> r
nil Union '[] x
u'
{-# INLINE runPure #-}

-- * Standard interpretation functions

-- ** For first-order effects

-- | Interprets the first-order effect @e@ at the head of the list using the provided natural transformation style handler.
interpret
    :: forall e ef eh
     . (e ~> Eff eh ef)
    -- ^ Effect handler
    -> Eff eh (e ': ef) ~> Eff eh ef
interpret :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]).
(e ~> Eff eh ef) -> Eff eh (e : ef) ~> Eff eh ef
interpret = (e ~> Eff eh ef) -> Eff eh (e : ef) ~> Eff eh ef
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]).
IsSuffixOf ef ef' =>
(e ~> Eff eh ef') -> Eff eh (e : ef) ~> Eff eh ef'
reinterpret
{-# INLINE interpret #-}

-- | Interprets the first-order effect @e@ at the head of the list using the provided continuational stateful handler.
interpretWith
    :: forall e ef a
     . Interpreter e (Eff '[] ef) a
    -- ^ Effect handler
    -> Eff '[] (e ': ef) a
    -> Eff '[] ef a
interpretWith :: forall (e :: * -> *) (ef :: [* -> *]) a.
Interpreter e (Eff '[] ef) a -> Eff '[] (e : ef) a -> Eff '[] ef a
interpretWith = Interpreter e (Eff '[] ef) a -> Eff '[] (e : ef) a -> Eff '[] ef a
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) a.
IsSuffixOf ef ef' =>
Interpreter e (Eff eh ef') a -> Eff '[] (e : ef) a -> Eff eh ef' a
reinterpretWith
{-# INLINE interpretWith #-}

-- | Interprets the first-order effect @e@ at the head of the list using the provided value handler and continuational stateful handler.
interpretBy
    :: forall e ef ans a
     . (a -> Eff '[] ef ans)
    -- ^ Value handler
    -> Interpreter e (Eff '[] ef) ans
    -- ^ Effect handler
    -> Eff '[] (e ': ef) a
    -> Eff '[] ef ans
interpretBy :: forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy = (a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) ans a.
IsSuffixOf ef ef' =>
(a -> Eff eh ef' ans)
-> Interpreter e (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
reinterpretBy
{-# INLINE interpretBy #-}

{- | Interprets the first-order effect @e@ at the head of the list using the provided continuational stateful handler.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.
Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.
-}
interpretRecWith
    :: forall e ef eh a
     . (forall ans. Interpreter e (Eff eh ef) ans)
    -- ^ Effect handler
    -> Eff eh (e ': ef) a
    -> Eff eh ef a
interpretRecWith :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) a.
(forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh (e : ef) a -> Eff eh ef a
interpretRecWith = (forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh (e : ef) a -> Eff eh ef a
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) a.
IsSuffixOf ef ef' =>
(forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) a -> Eff eh ef' a
reinterpretRecWith
{-# INLINE interpretRecWith #-}

-- ** For higher-order effects

-- | Interprets the higher-order effect @e@ at the head of the list using the provided natural transformation style elaborator.
interpretH
    :: forall e eh ef
     . (HFunctor e)
    => e ~~> Eff eh ef
    -- ^ Effect elaborator
    -> Eff (e ': eh) ef ~> Eff eh ef
interpretH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH = (e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]).
(HFunctor e, IsSuffixOf eh eh') =>
(e ~~> Eff eh' ef) -> Eff (e : eh) ef ~> Eff eh' ef
reinterpretH
{-# INLINE interpretH #-}

-- | Interprets the single higher-order effect @e@ using the provided continuational stateful elaborator.
interpretHWith
    :: forall e eh ef a
     . (HFunctor e)
    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
    -- ^ Effect elaborator
    -> Eff '[e] ef a
    -> Eff eh ef a
interpretHWith :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
HFunctor e =>
Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
interpretHWith = Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
HFunctor e =>
Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
reinterpretHWith
{-# INLINE interpretHWith #-}

-- | Interprets the single higher-order effect @e@ using the provided value handler and continuational stateful elaborator.
interpretHBy
    :: forall e eh ef ans a
     . (HFunctor e)
    => (a -> Eff eh ef ans)
    -- ^ Value handler
    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
    -- ^ Effect elaborator
    -> Eff '[e] ef a
    -> Eff eh ef ans
interpretHBy :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) ans a.
HFunctor e =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
interpretHBy = (a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) ans a.
HFunctor e =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
reinterpretHBy
{-# INLINE interpretHBy #-}

{- | Interprets the higher-order effect @e@ at the head of the list using the provided continuational stateful elaborator.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.
Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.
-}
interpretRecHWith
    :: forall e eh ef a
     . (HFunctor e)
    => (forall ans. Elaborator e (Eff eh ef) ans)
    -- ^ Effect elaborator
    -> Eff (e ': eh) ef a
    -> Eff eh ef a
interpretRecHWith :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
HFunctor e =>
(forall ans x.
 e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff (e : eh) ef a -> Eff eh ef a
interpretRecHWith = (forall ans x.
 e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff (e : eh) ef a -> Eff eh ef a
forall (e :: EffectH) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]) a.
(HFunctor e, IsSuffixOf eh eh') =>
(forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef a -> Eff eh' ef a
reinterpretRecHWith
{-# INLINE interpretRecHWith #-}

-- * Reinterpretation functions

-- ** For first-order effects

reinterpret
    :: forall e ef' ef eh
     . (ef `IsSuffixOf` ef')
    => (e ~> Eff eh ef')
    -> Eff eh (e ': ef) ~> Eff eh ef'
reinterpret :: forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]).
IsSuffixOf ef ef' =>
(e ~> Eff eh ef') -> Eff eh (e : ef) ~> Eff eh ef'
reinterpret e ~> Eff eh ef'
f = (forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) x -> Eff eh ef' x
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) a.
IsSuffixOf ef ef' =>
(forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) a -> Eff eh ef' a
reinterpretRecWith ((e ~> Eff eh ef') -> Interpreter e (Eff eh ef') ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e x -> Eff eh ef' x
e ~> Eff eh ef'
f)
{-# INLINE reinterpret #-}

reinterpretN
    :: forall n e ef' ef eh
     . (WeakenN n ef ef')
    => (e ~> Eff eh ef')
    -> Eff eh (e ': ef) ~> Eff eh ef'
reinterpretN :: forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]).
WeakenN n ef ef' =>
(e ~> Eff eh ef') -> Eff eh (e : ef) ~> Eff eh ef'
reinterpretN e ~> Eff eh ef'
f = forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]) a.
WeakenN n ef ef' =>
(forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) a -> Eff eh ef' a
reinterpretRecNWith @n ((e ~> Eff eh ef') -> Interpreter e (Eff eh ef') ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e x -> Eff eh ef' x
e ~> Eff eh ef'
f)
{-# INLINE reinterpretN #-}

reinterpretWith
    :: forall e ef' ef eh a
     . (ef `IsSuffixOf` ef')
    => Interpreter e (Eff eh ef') a
    -> Eff '[] (e ': ef) a
    -> Eff eh ef' a
reinterpretWith :: forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) a.
IsSuffixOf ef ef' =>
Interpreter e (Eff eh ef') a -> Eff '[] (e : ef) a -> Eff eh ef' a
reinterpretWith = (a -> Eff eh ef' a)
-> Interpreter e (Eff eh ef') a
-> Eff '[] (e : ef) a
-> Eff eh ef' a
forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) ans a.
IsSuffixOf ef ef' =>
(a -> Eff eh ef' ans)
-> Interpreter e (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
reinterpretBy a -> Eff eh ef' a
forall a. a -> Eff eh ef' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE reinterpretWith #-}

reinterpretNWith
    :: forall n e ef' ef eh a
     . (WeakenN n ef ef')
    => Interpreter e (Eff eh ef') a
    -> Eff '[] (e ': ef) a
    -> Eff eh ef' a
reinterpretNWith :: forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]) a.
WeakenN n ef ef' =>
Interpreter e (Eff eh ef') a -> Eff '[] (e : ef) a -> Eff eh ef' a
reinterpretNWith = forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]) ans a.
WeakenN n ef ef' =>
(a -> Eff eh ef' ans)
-> Interpreter e (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
reinterpretNBy @n a -> Eff eh ef' a
forall a. a -> Eff eh ef' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE reinterpretNWith #-}

reinterpretBy
    :: forall e ef' ef eh ans a
     . (ef `IsSuffixOf` ef')
    => (a -> Eff eh ef' ans)
    -> Interpreter e (Eff eh ef') ans
    -> Eff '[] (e ': ef) a
    -> Eff eh ef' ans
reinterpretBy :: forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) ans a.
IsSuffixOf ef ef' =>
(a -> Eff eh ef' ans)
-> Interpreter e (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
reinterpretBy a -> Eff eh ef' ans
ret Interpreter e (Eff eh ef') ans
hdl = (a -> Eff eh ef' ans)
-> Interpreter (UnionH '[] (Eff '[] (e : ef))) (Eff eh ef') ans
-> Interpreter (Union (e : ef)) (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> Eff eh ef' ans
ret UnionH '[] (Eff '[] (e : ef)) x
-> (x -> Eff eh ef' ans) -> Eff eh ef' ans
Interpreter (UnionH '[] (Eff '[] (e : ef))) (Eff eh ef') ans
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH (e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
Interpreter e (Eff eh ef') ans
hdl (e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> (Union ef x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Union (e : ef) x
-> (x -> Eff eh ef' ans)
-> Eff eh ef' ans
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ ((x -> Eff eh ef' ans) -> Union ef' x -> Eff eh ef' ans)
-> Union ef' x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' ans) -> Union ef' x -> Eff eh ef' ans
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy (Union ef' x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> (Union ef x -> Union ef' x)
-> Union ef x
-> (x -> Eff eh ef' ans)
-> Eff eh ef' ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union ef x -> Union ef' x
forall (es :: [* -> *]) (es' :: [* -> *]) a.
IsSuffixOf es es' =>
Union es a -> Union es' a
weakens)
{-# INLINE reinterpretBy #-}

reinterpretNBy
    :: forall n e ef' ef eh ans a
     . (WeakenN n ef ef')
    => (a -> Eff eh ef' ans)
    -> Interpreter e (Eff eh ef') ans
    -> Eff '[] (e ': ef) a
    -> Eff eh ef' ans
reinterpretNBy :: forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]) ans a.
WeakenN n ef ef' =>
(a -> Eff eh ef' ans)
-> Interpreter e (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
reinterpretNBy a -> Eff eh ef' ans
ret Interpreter e (Eff eh ef') ans
hdl = (a -> Eff eh ef' ans)
-> Interpreter (UnionH '[] (Eff '[] (e : ef))) (Eff eh ef') ans
-> Interpreter (Union (e : ef)) (Eff eh ef') ans
-> Eff '[] (e : ef) a
-> Eff eh ef' ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> Eff eh ef' ans
ret UnionH '[] (Eff '[] (e : ef)) x
-> (x -> Eff eh ef' ans) -> Eff eh ef' ans
Interpreter (UnionH '[] (Eff '[] (e : ef))) (Eff eh ef') ans
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH (e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
Interpreter e (Eff eh ef') ans
hdl (e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> (Union ef x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Union (e : ef) x
-> (x -> Eff eh ef' ans)
-> Eff eh ef' ans
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ ((x -> Eff eh ef' ans) -> Union ef' x -> Eff eh ef' ans)
-> Union ef' x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' ans) -> Union ef' x -> Eff eh ef' ans
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy (Union ef' x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> (Union ef x -> Union ef' x)
-> Union ef x
-> (x -> Eff eh ef' ans)
-> Eff eh ef' ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (len :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenN len es es' =>
Union es a -> Union es' a
weakenN @n)
{-# INLINE reinterpretNBy #-}

reinterpretRecWith
    :: forall e ef' ef eh a
     . (ef `IsSuffixOf` ef')
    => (forall ans. Interpreter e (Eff eh ef') ans)
    -> Eff eh (e ': ef) a
    -> Eff eh ef' a
reinterpretRecWith :: forall (e :: * -> *) (ef' :: [* -> *]) (ef :: [* -> *])
       (eh :: [EffectH]) a.
IsSuffixOf ef ef' =>
(forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) a -> Eff eh ef' a
reinterpretRecWith forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
hdl = Eff eh (e : ef) a -> Eff eh ef' a
Eff eh (e : ef) ~> Eff eh ef'
loop
  where
    loop :: Eff eh (e ': ef) ~> Eff eh ef'
    loop :: Eff eh (e : ef) ~> Eff eh ef'
loop = (x -> Eff eh ef' x)
-> Interpreter (UnionH eh (Eff eh (e : ef))) (Eff eh ef') x
-> Interpreter (Union (e : ef)) (Eff eh ef') x
-> Eff eh (e : ef) x
-> Eff eh ef' x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy x -> Eff eh ef' x
forall a. a -> Eff eh ef' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((x -> Eff eh ef' x) -> UnionH eh (Eff eh ef') x -> Eff eh ef' x)
-> UnionH eh (Eff eh ef') x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' x) -> UnionH eh (Eff eh ef') x -> Eff eh ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh (Eff eh ef') x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (UnionH eh (Eff eh (e : ef)) x -> UnionH eh (Eff eh ef') x)
-> UnionH eh (Eff eh (e : ef)) x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff eh (e : ef) ~> Eff eh ef')
-> UnionH eh (Eff eh (e : ef)) x -> UnionH eh (Eff eh ef') x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh (e : ef) x -> Eff eh ef' x
Eff eh (e : ef) ~> Eff eh ef'
loop) (e x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
hdl (e x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (Union ef x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> Union (e : ef) x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ ((x -> Eff eh ef' x) -> Union ef' x -> Eff eh ef' x)
-> Union ef' x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' x) -> Union ef' x -> Eff eh ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy (Union ef' x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (Union ef x -> Union ef' x)
-> Union ef x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union ef x -> Union ef' x
forall (es :: [* -> *]) (es' :: [* -> *]) a.
IsSuffixOf es es' =>
Union es a -> Union es' a
weakens)
{-# INLINE reinterpretRecWith #-}

reinterpretRecNWith
    :: forall n e ef' ef eh a
     . (WeakenN n ef ef')
    => (forall ans. Interpreter e (Eff eh ef') ans)
    -> Eff eh (e ': ef) a
    -> Eff eh ef' a
reinterpretRecNWith :: forall (n :: Natural) (e :: * -> *) (ef' :: [* -> *])
       (ef :: [* -> *]) (eh :: [EffectH]) a.
WeakenN n ef ef' =>
(forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans)
-> Eff eh (e : ef) a -> Eff eh ef' a
reinterpretRecNWith forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
hdl = Eff eh (e : ef) a -> Eff eh ef' a
Eff eh (e : ef) ~> Eff eh ef'
loop
  where
    loop :: Eff eh (e ': ef) ~> Eff eh ef'
    loop :: Eff eh (e : ef) ~> Eff eh ef'
loop = (x -> Eff eh ef' x)
-> Interpreter (UnionH eh (Eff eh (e : ef))) (Eff eh ef') x
-> Interpreter (Union (e : ef)) (Eff eh ef') x
-> Eff eh (e : ef) x
-> Eff eh ef' x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy x -> Eff eh ef' x
forall a. a -> Eff eh ef' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((x -> Eff eh ef' x) -> UnionH eh (Eff eh ef') x -> Eff eh ef' x)
-> UnionH eh (Eff eh ef') x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' x) -> UnionH eh (Eff eh ef') x -> Eff eh ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh (Eff eh ef') x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (UnionH eh (Eff eh (e : ef)) x -> UnionH eh (Eff eh ef') x)
-> UnionH eh (Eff eh (e : ef)) x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff eh (e : ef) ~> Eff eh ef')
-> UnionH eh (Eff eh (e : ef)) x -> UnionH eh (Eff eh ef') x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh (e : ef) x -> Eff eh ef' x
Eff eh (e : ef) ~> Eff eh ef'
loop) (e x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall ans x. e x -> (x -> Eff eh ef' ans) -> Eff eh ef' ans
hdl (e x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (Union ef x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> Union (e : ef) x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ ((x -> Eff eh ef' x) -> Union ef' x -> Eff eh ef' x)
-> Union ef' x -> (x -> Eff eh ef' x) -> Eff eh ef' x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef' x) -> Union ef' x -> Eff eh ef' x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy (Union ef' x -> (x -> Eff eh ef' x) -> Eff eh ef' x)
-> (Union ef x -> Union ef' x)
-> Union ef x
-> (x -> Eff eh ef' x)
-> Eff eh ef' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (len :: Natural) (es :: [* -> *]) (es' :: [* -> *]) a.
WeakenN len es es' =>
Union es a -> Union es' a
weakenN @n)
{-# INLINE reinterpretRecNWith #-}

-- ** For higher-order effects

reinterpretH
    :: forall e eh eh' ef
     . (HFunctor e, eh `IsSuffixOf` eh')
    => e ~~> Eff eh' ef
    -> Eff (e ': eh) ef ~> Eff eh' ef
reinterpretH :: forall (e :: EffectH) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]).
(HFunctor e, IsSuffixOf eh eh') =>
(e ~~> Eff eh' ef) -> Eff (e : eh) ef ~> Eff eh' ef
reinterpretH e ~~> Eff eh' ef
elb = (forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef x -> Eff eh' ef x
forall (e :: EffectH) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]) a.
(HFunctor e, IsSuffixOf eh eh') =>
(forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef a -> Eff eh' ef a
reinterpretRecHWith ((e ~~> Eff eh' ef) -> Interpreter (e (Eff eh' ef)) (Eff eh' ef) ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e (Eff eh' ef) x -> Eff eh' ef x
e ~~> Eff eh' ef
elb)
{-# INLINE reinterpretH #-}

reinterpretNH
    :: forall n e eh eh' ef
     . (HFunctor e, WeakenN n eh eh')
    => e ~~> Eff eh' ef
    -> Eff (e ': eh) ef ~> Eff eh' ef
reinterpretNH :: forall (n :: Natural) (e :: EffectH) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]).
(HFunctor e, WeakenN n eh eh') =>
(e ~~> Eff eh' ef) -> Eff (e : eh) ef ~> Eff eh' ef
reinterpretNH e ~~> Eff eh' ef
elb = forall (n :: Natural) (e :: EffectH) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]) a.
(HFunctor e, WeakenN n eh eh') =>
(forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef a -> Eff eh' ef a
reinterpretRecNHWith @n ((e ~~> Eff eh' ef) -> Interpreter (e (Eff eh' ef)) (Eff eh' ef) ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e (Eff eh' ef) x -> Eff eh' ef x
e ~~> Eff eh' ef
elb)
{-# INLINE reinterpretNH #-}

reinterpretHWith
    :: forall e eh ef a
     . (HFunctor e)
    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
    -> Eff '[e] ef a
    -> Eff eh ef a
reinterpretHWith :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
HFunctor e =>
Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
reinterpretHWith = (a -> Eff eh ef a)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a
-> Eff eh ef a
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) ans a.
HFunctor e =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
reinterpretHBy a -> Eff eh ef a
forall a. a -> Eff eh ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE reinterpretHWith #-}

reinterpretNHWith
    :: forall n e eh ef a
     . (HFunctor e, WeakenN n '[] eh)
    => Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
    -> Eff '[e] ef a
    -> Eff eh ef a
reinterpretNHWith :: forall (n :: Natural) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]) a.
(HFunctor e, WeakenN n '[] eh) =>
Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
reinterpretNHWith = Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
HFunctor e =>
Interpreter (e (Eff '[e] ef)) (Eff eh ef) a
-> Eff '[e] ef a -> Eff eh ef a
reinterpretHWith
{-# INLINE reinterpretNHWith #-}

reinterpretHBy
    :: forall e eh ef ans a
     . (HFunctor e)
    => (a -> Eff eh ef ans)
    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
    -> Eff '[e] ef a
    -> Eff eh ef ans
reinterpretHBy :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) ans a.
HFunctor e =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
reinterpretHBy a -> Eff eh ef ans
ret Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
elb = (a -> Eff eh ef ans)
-> Interpreter (UnionH '[e] (Eff '[e] ef)) (Eff eh ef) ans
-> Interpreter (Union ef) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> Eff eh ef ans
ret (e (Eff '[e] ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans
Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
elb (e (Eff '[e] ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> (UnionH '[e] (Eff '[e] ef) x -> e (Eff '[e] ef) x)
-> UnionH '[e] (Eff '[e] ef) x
-> (x -> Eff eh ef ans)
-> Eff eh ef ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH '[e] (Eff '[e] ef) x -> e (Eff '[e] ef) x
forall (e :: EffectH) (f :: * -> *) a.
HFunctor e =>
UnionH '[e] f a -> e f a
extractH) (((x -> Eff eh ef ans) -> Union ef x -> Eff eh ef ans)
-> Union ef x -> (x -> Eff eh ef ans) -> Eff eh ef ans
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef ans) -> Union ef x -> Eff eh ef ans
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy)
{-# INLINE reinterpretHBy #-}

reinterpretNHBy
    :: forall n e eh ef ans a
     . (HFunctor e, WeakenN n '[] eh)
    => (a -> Eff eh ef ans)
    -> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
    -> Eff '[e] ef a
    -> Eff eh ef ans
reinterpretNHBy :: forall (n :: Natural) (e :: EffectH) (eh :: [EffectH])
       (ef :: [* -> *]) ans a.
(HFunctor e, WeakenN n '[] eh) =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
reinterpretNHBy = (a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) ans a.
HFunctor e =>
(a -> Eff eh ef ans)
-> Interpreter (e (Eff '[e] ef)) (Eff eh ef) ans
-> Eff '[e] ef a
-> Eff eh ef ans
reinterpretHBy
{-# INLINE reinterpretNHBy #-}

reinterpretRecHWith
    :: forall e eh eh' ef a
     . (HFunctor e, eh `IsSuffixOf` eh')
    => (forall ans. Elaborator e (Eff eh' ef) ans)
    -> Eff (e ': eh) ef a
    -> Eff eh' ef a
reinterpretRecHWith :: forall (e :: EffectH) (eh :: [EffectH]) (eh' :: [EffectH])
       (ef :: [* -> *]) a.
(HFunctor e, IsSuffixOf eh eh') =>
(forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef a -> Eff eh' ef a
reinterpretRecHWith forall ans x.
e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans
elb = Eff (e : eh) ef a -> Eff eh' ef a
Eff (e : eh) ef ~> Eff eh' ef
loop
  where
    loop :: Eff (e ': eh) ef ~> Eff eh' ef
    loop :: Eff (e : eh) ef ~> Eff eh' ef
loop =
        (x -> Eff eh' ef x)
-> Interpreter (UnionH (e : eh) (Eff (e : eh) ef)) (Eff eh' ef) x
-> Interpreter (Union ef) (Eff eh' ef) x
-> Eff (e : eh) ef x
-> Eff eh' ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
            x -> Eff eh' ef x
forall a. a -> Eff eh' ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (e (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall ans x.
e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans
elb (e (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (e (Eff (e : eh) ef) x -> e (Eff eh' ef) x)
-> e (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff (e : eh) ef ~> Eff eh' ef)
-> e (Eff (e : eh) ef) :-> e (Eff eh' ef)
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Eff (e : eh) ef i -> Eff eh' ef i
Eff (e : eh) ef ~> Eff eh' ef
loop (e (Eff (e : eh) ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (UnionH eh (Eff (e : eh) ef) x
    -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> UnionH (e : eh) (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall (e :: EffectH) (f :: * -> *) a r (es :: [EffectH]).
HFunctor e =>
(e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r
!!+ ((x -> Eff eh' ef x) -> UnionH eh' (Eff eh' ef) x -> Eff eh' ef x)
-> UnionH eh' (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef x) -> UnionH eh' (Eff eh' ef) x -> Eff eh' ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh' (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (UnionH eh (Eff (e : eh) ef) x -> UnionH eh' (Eff eh' ef) x)
-> UnionH eh (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x
forall (es :: [EffectH]) (es' :: [EffectH]) (f :: * -> *) a.
IsSuffixOf es es' =>
UnionH es f a -> UnionH es' f a
weakensH (UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x)
-> (UnionH eh (Eff (e : eh) ef) x -> UnionH eh (Eff eh' ef) x)
-> UnionH eh (Eff (e : eh) ef) x
-> UnionH eh' (Eff eh' ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff (e : eh) ef ~> Eff eh' ef)
-> UnionH eh (Eff (e : eh) ef) x -> UnionH eh (Eff eh' ef) x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff (e : eh) ef x -> Eff eh' ef x
Eff (e : eh) ef ~> Eff eh' ef
loop)
            (((x -> Eff eh' ef x) -> Union ef x -> Eff eh' ef x)
-> Union ef x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef x) -> Union ef x -> Eff eh' ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy)
{-# INLINE reinterpretRecHWith #-}

reinterpretRecNHWith
    :: forall n e eh eh' ef a
     . (HFunctor e, WeakenN n eh eh')
    => (forall ans. Elaborator e (Eff eh' ef) ans)
    -> Eff (e ': eh) ef a
    -> Eff eh' ef a
reinterpretRecNHWith :: forall (n :: Natural) (e :: EffectH) (eh :: [EffectH])
       (eh' :: [EffectH]) (ef :: [* -> *]) a.
(HFunctor e, WeakenN n eh eh') =>
(forall ans x.
 e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans)
-> Eff (e : eh) ef a -> Eff eh' ef a
reinterpretRecNHWith forall ans x.
e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans
elb = Eff (e : eh) ef a -> Eff eh' ef a
Eff (e : eh) ef ~> Eff eh' ef
loop
  where
    loop :: Eff (e ': eh) ef ~> Eff eh' ef
    loop :: Eff (e : eh) ef ~> Eff eh' ef
loop =
        (x -> Eff eh' ef x)
-> Interpreter (UnionH (e : eh) (Eff (e : eh) ef)) (Eff eh' ef) x
-> Interpreter (Union ef) (Eff eh' ef) x
-> Eff (e : eh) ef x
-> Eff eh' ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
            x -> Eff eh' ef x
forall a. a -> Eff eh' ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (e (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall ans x.
e (Eff eh' ef) x -> (x -> Eff eh' ef ans) -> Eff eh' ef ans
elb (e (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (e (Eff (e : eh) ef) x -> e (Eff eh' ef) x)
-> e (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff (e : eh) ef ~> Eff eh' ef)
-> e (Eff (e : eh) ef) :-> e (Eff eh' ef)
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Eff (e : eh) ef i -> Eff eh' ef i
Eff (e : eh) ef ~> Eff eh' ef
loop (e (Eff (e : eh) ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (UnionH eh (Eff (e : eh) ef) x
    -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> UnionH (e : eh) (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall (e :: EffectH) (f :: * -> *) a r (es :: [EffectH]).
HFunctor e =>
(e f a -> r) -> (UnionH es f a -> r) -> UnionH (e : es) f a -> r
!!+ ((x -> Eff eh' ef x) -> UnionH eh' (Eff eh' ef) x -> Eff eh' ef x)
-> UnionH eh' (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef x) -> UnionH eh' (Eff eh' ef) x -> Eff eh' ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh' (Eff eh' ef) x -> (x -> Eff eh' ef x) -> Eff eh' ef x)
-> (UnionH eh (Eff (e : eh) ef) x -> UnionH eh' (Eff eh' ef) x)
-> UnionH eh (Eff (e : eh) ef) x
-> (x -> Eff eh' ef x)
-> Eff eh' ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (len :: Natural) (es :: [EffectH]) (es' :: [EffectH])
       (f :: * -> *) a.
WeakenN len es es' =>
UnionH es f a -> UnionH es' f a
weakenNH @n (UnionH eh (Eff eh' ef) x -> UnionH eh' (Eff eh' ef) x)
-> (UnionH eh (Eff (e : eh) ef) x -> UnionH eh (Eff eh' ef) x)
-> UnionH eh (Eff (e : eh) ef) x
-> UnionH eh' (Eff eh' ef) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff (e : eh) ef ~> Eff eh' ef)
-> UnionH eh (Eff (e : eh) ef) x -> UnionH eh (Eff eh' ef) x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff (e : eh) ef x -> Eff eh' ef x
Eff (e : eh) ef ~> Eff eh' ef
loop)
            (((x -> Eff eh' ef x) -> Union ef x -> Eff eh' ef x)
-> Union ef x -> (x -> Eff eh' ef x) -> Eff eh' ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh' ef x) -> Union ef x -> Eff eh' ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy)
{-# INLINE reinterpretRecNHWith #-}

-- * Interposition functions

-- ** For first-order effects

{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided natural transformation style handler.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interpose
    :: forall e ef eh
     . (e <| ef)
    => (e ~> Eff eh ef)
    -- ^ Effect handler
    -> Eff eh ef ~> Eff eh ef
interpose :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]).
(e <| ef) =>
(e ~> Eff eh ef) -> Eff eh ef ~> Eff eh ef
interpose e ~> Eff eh ef
f = (forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef x -> Eff eh ef x
forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) a.
(e <| ef) =>
(forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef a -> Eff eh ef a
interposeRecWith ((e ~> Eff eh ef) -> Interpreter e (Eff eh ef) ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e x -> Eff eh ef x
e ~> Eff eh ef
f)
{-# INLINE interpose #-}

{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided continuational stateful handler.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interposeWith
    :: forall e ef a
     . (e <| ef)
    => Interpreter e (Eff '[] ef) a
    -- ^ Effect handler
    -> Eff '[] ef a
    -> Eff '[] ef a
interposeWith :: forall (e :: * -> *) (ef :: [* -> *]) a.
(e <| ef) =>
Interpreter e (Eff '[] ef) a -> Eff '[] ef a -> Eff '[] ef a
interposeWith = (a -> Eff '[] ef a)
-> (forall {x}. e x -> (x -> Eff '[] ef a) -> Eff '[] ef a)
-> Eff '[] ef a
-> Eff '[] ef a
forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) ans a.
(e <| ef) =>
(a -> Eff eh ef ans)
-> Interpreter e (Eff eh ef) ans -> Eff '[] ef a -> Eff eh ef ans
interposeBy a -> Eff '[] ef a
forall a. a -> Eff '[] ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE interposeWith #-}

{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided value handler and continuational stateful handler.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interposeBy
    :: forall e ef eh ans a
     . (e <| ef)
    => (a -> Eff eh ef ans)
    -- ^ Value handler
    -> Interpreter e (Eff eh ef) ans
    -- ^ Effect handler
    -> Eff '[] ef a
    -> Eff eh ef ans
interposeBy :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) ans a.
(e <| ef) =>
(a -> Eff eh ef ans)
-> Interpreter e (Eff eh ef) ans -> Eff '[] ef a -> Eff eh ef ans
interposeBy a -> Eff eh ef ans
ret Interpreter e (Eff eh ef) ans
f = (a -> Eff eh ef ans)
-> Interpreter (UnionH '[] (Eff '[] ef)) (Eff eh ef) ans
-> Interpreter (Union ef) (Eff eh ef) ans
-> Eff '[] ef a
-> Eff eh ef ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> Eff eh ef ans
ret UnionH '[] (Eff '[] ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans
Interpreter (UnionH '[] (Eff '[] ef)) (Eff eh ef) ans
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH \Union ef x
u -> ((x -> Eff eh ef ans) -> Eff eh ef ans)
-> (e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Maybe (e x)
-> (x -> Eff eh ef ans)
-> Eff eh ef ans
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((x -> Eff eh ef ans) -> Union ef x -> Eff eh ef ans
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
`sendUnionBy` Union ef x
u) e x -> (x -> Eff eh ef ans) -> Eff eh ef ans
Interpreter e (Eff eh ef) ans
f (forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
Union es a -> Maybe (e a)
prj @e Union ef x
u)
{-# INLINE interposeBy #-}

{- | Reinterprets (hooks) the first-order effect @e@ in the list using the provided continuational stateful handler.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.
Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interposeRecWith
    :: forall e ef eh a
     . (e <| ef)
    => (forall ans. Interpreter e (Eff eh ef) ans)
    -- ^ Effect handler
    -> Eff eh ef a
    -> Eff eh ef a
interposeRecWith :: forall (e :: * -> *) (ef :: [* -> *]) (eh :: [EffectH]) a.
(e <| ef) =>
(forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef a -> Eff eh ef a
interposeRecWith forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans
f = Eff eh ef a -> Eff eh ef a
Eff eh ef ~> Eff eh ef
loop
  where
    loop :: Eff eh ef ~> Eff eh ef
    loop :: Eff eh ef ~> Eff eh ef
loop = (x -> Eff eh ef x)
-> Interpreter (UnionH eh (Eff eh ef)) (Eff eh ef) x
-> Interpreter (Union ef) (Eff eh ef) x
-> Eff eh ef x
-> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
        x -> Eff eh ef x
forall a. a -> Eff eh ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (((x -> Eff eh ef x) -> UnionH eh (Eff eh ef) x -> Eff eh ef x)
-> UnionH eh (Eff eh ef) x -> (x -> Eff eh ef x) -> Eff eh ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef x) -> UnionH eh (Eff eh ef) x -> Eff eh ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
sendUnionHBy (UnionH eh (Eff eh ef) x -> (x -> Eff eh ef x) -> Eff eh ef x)
-> (UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> UnionH eh (Eff eh ef) x
-> (x -> Eff eh ef x)
-> Eff eh ef x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff eh ef ~> Eff eh ef)
-> UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh ef x -> Eff eh ef x
Eff eh ef ~> Eff eh ef
loop)
        \Union ef x
u -> ((x -> Eff eh ef x) -> Eff eh ef x)
-> (e x -> (x -> Eff eh ef x) -> Eff eh ef x)
-> Maybe (e x)
-> (x -> Eff eh ef x)
-> Eff eh ef x
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((x -> Eff eh ef x) -> Union ef x -> Eff eh ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
`sendUnionBy` Union ef x
u) e x -> (x -> Eff eh ef x) -> Eff eh ef x
forall ans x. e x -> (x -> Eff eh ef ans) -> Eff eh ef ans
f (forall (e :: * -> *) (es :: [* -> *]) a.
Member e es =>
Union es a -> Maybe (e a)
prj @e Union ef x
u)
{-# INLINE interposeRecWith #-}

-- ** For higher-order effects

{- | Reinterprets (hooks) the higher-order effect @e@ in the list using the provided natural transformation style elaborator.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interposeH
    :: forall e eh ef
     . (e <<| eh, HFunctor e)
    => e ~~> Eff eh ef
    -- ^ Effect elaborator
    -> Eff eh ef ~> Eff eh ef
interposeH :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
(e <<| eh, HFunctor e) =>
(e ~~> Eff eh ef) -> Eff eh ef ~> Eff eh ef
interposeH e ~~> Eff eh ef
f = (forall ans x.
 e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef x -> Eff eh ef x
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
(e <<| eh, HFunctor e) =>
(forall ans x.
 e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef a -> Eff eh ef a
interposeRecHWith ((e ~~> Eff eh ef) -> Interpreter (e (Eff eh ef)) (Eff eh ef) ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e (Eff eh ef) x -> Eff eh ef x
e ~~> Eff eh ef
f)
{-# INLINE interposeH #-}

{- | Reinterprets (hooks) the higher-order effect @e@ in the list using the provided continuational stateful elaborator.

Interpretation is performed recursively with respect to the scopes of unelaborated higher-order effects @eh@.
Note that during interpretation, the continuational state is reset (delimited) and does not persist beyond scopes.

If multiple instances of @e@ exist in the list, the one closest to the head (with the smallest index) will be targeted.
-}
interposeRecHWith
    :: forall e eh ef a
     . (e <<| eh, HFunctor e)
    => (forall ans. Elaborator e (Eff eh ef) ans)
    -- ^ Effect elaborator
    -> Eff eh ef a
    -> Eff eh ef a
interposeRecHWith :: forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]) a.
(e <<| eh, HFunctor e) =>
(forall ans x.
 e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans)
-> Eff eh ef a -> Eff eh ef a
interposeRecHWith forall ans x.
e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans
f = Eff eh ef a -> Eff eh ef a
Eff eh ef ~> Eff eh ef
loop
  where
    loop :: Eff eh ef ~> Eff eh ef
    loop :: Eff eh ef ~> Eff eh ef
loop =
        (x -> Eff eh ef x)
-> Interpreter (UnionH eh (Eff eh ef)) (Eff eh ef) x
-> Interpreter (Union ef) (Eff eh ef) x
-> Eff eh ef x
-> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
            x -> Eff eh ef x
forall a. a -> Eff eh ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ((Eff eh ef ~> Eff eh ef)
-> UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh ef x -> Eff eh ef x
Eff eh ef ~> Eff eh ef
loop (UnionH eh (Eff eh ef) x -> UnionH eh (Eff eh ef) x)
-> (UnionH eh (Eff eh ef) x -> (x -> Eff eh ef x) -> Eff eh ef x)
-> UnionH eh (Eff eh ef) x
-> (x -> Eff eh ef x)
-> Eff eh ef x
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> \UnionH eh (Eff eh ef) x
u -> ((x -> Eff eh ef x) -> Eff eh ef x)
-> (e (Eff eh ef) x -> (x -> Eff eh ef x) -> Eff eh ef x)
-> Maybe (e (Eff eh ef) x)
-> (x -> Eff eh ef x)
-> Eff eh ef x
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((x -> Eff eh ef x) -> UnionH eh (Eff eh ef) x -> Eff eh ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> UnionH eh (Eff eh ef) a -> Eff eh ef ans
`sendUnionHBy` UnionH eh (Eff eh ef) x
u) e (Eff eh ef) x -> (x -> Eff eh ef x) -> Eff eh ef x
forall ans x.
e (Eff eh ef) x -> (x -> Eff eh ef ans) -> Eff eh ef ans
f (forall (e :: EffectH) (es :: [EffectH]) (f :: * -> *) a.
(MemberH e es, HFunctor e) =>
UnionH es f a -> Maybe (e f a)
prjH @e UnionH eh (Eff eh ef) x
u))
            (((x -> Eff eh ef x) -> Union ef x -> Eff eh ef x)
-> Union ef x -> (x -> Eff eh ef x) -> Eff eh ef x
forall a b c. (a -> b -> c) -> b -> a -> c
flip (x -> Eff eh ef x) -> Union ef x -> Eff eh ef x
forall a (eh :: [EffectH]) (ef :: [* -> *]) ans.
(a -> Eff eh ef ans) -> Union ef a -> Eff eh ef ans
sendUnionBy)
{-# INLINE interposeRecHWith #-}

-- * Transformation to monads

-- | Traverses a computation containing only a single first-order effect @e@ using the provided value handler and continuational stateful handler, transforming it into a monad @m@.
iterEffBy
    :: forall e m ans a
     . (Monad m)
    => (a -> m ans)
    -- ^ Value handler
    -> Interpreter e m ans
    -- ^ Effect handler
    -> Eff '[] '[e] a
    -> m ans
iterEffBy :: forall (e :: * -> *) (m :: * -> *) ans a.
Monad m =>
(a -> m ans) -> Interpreter e m ans -> Eff '[] '[e] a -> m ans
iterEffBy a -> m ans
ret Interpreter e m ans
hdl = (a -> m ans)
-> Interpreter (UnionH '[] (Eff '[] '[e])) m ans
-> Interpreter (Union '[e]) m ans
-> Eff '[] '[e] a
-> m ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> m ans
ret UnionH '[] (Eff '[] '[e]) x -> (x -> m ans) -> m ans
Interpreter (UnionH '[] (Eff '[] '[e])) m ans
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH (e x -> (x -> m ans) -> m ans
Interpreter e m ans
hdl (e x -> (x -> m ans) -> m ans)
-> (Union '[e] x -> e x) -> Union '[e] x -> (x -> m ans) -> m ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union '[e] x -> e x
forall (e :: * -> *) a. Union '[e] a -> e a
extract)
{-# INLINE iterEffBy #-}

-- | Traverses a computation containing only a single higher-order effect @e@ using the provided value handler and continuational stateful elaborator, transforming it into a monad @m@.
iterEffHBy
    :: forall e m ans a
     . (Monad m, HFunctor e)
    => (a -> m ans)
    -- ^ Value handler
    -> Interpreter (e (Eff '[e] '[])) m ans
    -- ^ Effect handler
    -> Eff '[e] '[] a
    -> m ans
iterEffHBy :: forall (e :: EffectH) (m :: * -> *) ans a.
(Monad m, HFunctor e) =>
(a -> m ans)
-> Interpreter (e (Eff '[e] '[])) m ans -> Eff '[e] '[] a -> m ans
iterEffHBy a -> m ans
ret Interpreter (e (Eff '[e] '[])) m ans
elb = (a -> m ans)
-> Interpreter (UnionH '[e] (Eff '[e] '[])) m ans
-> Interpreter (Union '[]) m ans
-> Eff '[e] '[] a
-> m ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> m ans
ret (e (Eff '[e] '[]) x -> (x -> m ans) -> m ans
Interpreter (e (Eff '[e] '[])) m ans
elb (e (Eff '[e] '[]) x -> (x -> m ans) -> m ans)
-> (UnionH '[e] (Eff '[e] '[]) x -> e (Eff '[e] '[]) x)
-> UnionH '[e] (Eff '[e] '[]) x
-> (x -> m ans)
-> m ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH '[e] (Eff '[e] '[]) x -> e (Eff '[e] '[]) x
forall (e :: EffectH) (f :: * -> *) a.
HFunctor e =>
UnionH '[e] f a -> e f a
extractH) Union '[] x -> (x -> m ans) -> m ans
Interpreter (Union '[]) m ans
forall a r. Union '[] a -> r
nil
{-# INLINE iterEffHBy #-}

{- | Traverses a computation containing only a single higher-order effect @e@ using the provided natural transformation elaborator, transforming it into a monad @m@.

Traversal is performed recursively with respect to the scope of the higher-order effect @e@.
Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.
-}
iterEffRecH
    :: forall e m
     . (Monad m, HFunctor e)
    => e ~~> m
    -- ^ Effect elaborator
    -> Eff '[e] '[] ~> m
iterEffRecH :: forall (e :: EffectH) (m :: * -> *).
(Monad m, HFunctor e) =>
(e ~~> m) -> Eff '[e] '[] ~> m
iterEffRecH e ~~> m
elb = (forall ans x. e m x -> (x -> m ans) -> m ans) -> Eff '[e] '[] ~> m
forall (e :: EffectH) (m :: * -> *).
(Monad m, HFunctor e) =>
(forall ans x. e m x -> (x -> m ans) -> m ans) -> Eff '[e] '[] ~> m
iterEffRecHWith ((forall ans x. e m x -> (x -> m ans) -> m ans)
 -> Eff '[e] '[] ~> m)
-> (forall ans x. e m x -> (x -> m ans) -> m ans)
-> Eff '[e] '[] ~> m
forall a b. (a -> b) -> a -> b
$ (e ~~> m) -> Interpreter (e m) m ans
forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e m x -> m x
e ~~> m
elb
{-# INLINE iterEffRecH #-}

{- | Traverses a computation containing only a single higher-order effect @e@ using the provided continuational stateful elaborator, transforming it into a monad @m@.

Traversal is performed recursively with respect to the scope of the higher-order effect @e@.
Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.
-}
iterEffRecHWith
    :: forall e m
     . (Monad m, HFunctor e)
    => (forall ans. Elaborator e m ans)
    -- ^ Effect elaborator
    -> Eff '[e] '[] ~> m
iterEffRecHWith :: forall (e :: EffectH) (m :: * -> *).
(Monad m, HFunctor e) =>
(forall ans x. e m x -> (x -> m ans) -> m ans) -> Eff '[e] '[] ~> m
iterEffRecHWith forall ans x. e m x -> (x -> m ans) -> m ans
elb = Eff '[e] '[] x -> m x
Eff '[e] '[] ~> m
loop
  where
    loop :: Eff '[e] '[] ~> m
    loop :: Eff '[e] '[] ~> m
loop = (x -> m x)
-> Interpreter (e (Eff '[e] '[])) m x -> Eff '[e] '[] x -> m x
forall (e :: EffectH) (m :: * -> *) ans a.
(Monad m, HFunctor e) =>
(a -> m ans)
-> Interpreter (e (Eff '[e] '[])) m ans -> Eff '[e] '[] a -> m ans
iterEffHBy x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (e m x -> (x -> m x) -> m x
forall ans x. e m x -> (x -> m ans) -> m ans
elb (e m x -> (x -> m x) -> m x)
-> (e (Eff '[e] '[]) x -> e m x)
-> e (Eff '[e] '[]) x
-> (x -> m x)
-> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff '[e] '[] ~> m) -> e (Eff '[e] '[]) :-> e m
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> e f :-> e g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Eff '[e] '[] i -> m i
Eff '[e] '[] ~> m
loop)
{-# INLINE iterEffRecHWith #-}

{- | Traverses a computation containing only higher-order effects @eh@ and first-order effects @ef@ using the provided continuational stateful elaborator, transforming it into a monad @m@.

Traversal is performed recursively with respect to the scopes of higher-order effects.
Note that during traversal, the continuational state is reset (delimited) and does not persist beyond scopes.
-}
iterEffRecHFWith
    :: forall eh ef m
     . (Monad m, HFunctor eh)
    => (forall ans. Elaborator eh m ans)
    -- ^ Effect elaborator
    -> (forall ans. Interpreter ef m ans)
    -- ^ Effect handler
    -> Eff '[eh] '[ef] ~> m
iterEffRecHFWith :: forall (eh :: EffectH) (ef :: * -> *) (m :: * -> *).
(Monad m, HFunctor eh) =>
(forall ans x. eh m x -> (x -> m ans) -> m ans)
-> (forall ans x. ef x -> (x -> m ans) -> m ans)
-> Eff '[eh] '[ef] ~> m
iterEffRecHFWith forall ans x. eh m x -> (x -> m ans) -> m ans
fh forall ans x. ef x -> (x -> m ans) -> m ans
ff = Eff '[eh] '[ef] x -> m x
Eff '[eh] '[ef] ~> m
loop
  where
    loop :: Eff '[eh] '[ef] ~> m
    loop :: Eff '[eh] '[ef] ~> m
loop = (x -> m x)
-> Interpreter (eh (Eff '[eh] '[ef])) m x
-> Interpreter ef m x
-> Eff '[eh] '[ef] x
-> m x
forall (eh :: EffectH) (ef :: * -> *) (m :: * -> *) ans a.
(Monad m, HFunctor eh) =>
(a -> m ans)
-> Interpreter (eh (Eff '[eh] '[ef])) m ans
-> Interpreter ef m ans
-> Eff '[eh] '[ef] a
-> m ans
iterEffHFBy x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (eh m x -> (x -> m x) -> m x
forall ans x. eh m x -> (x -> m ans) -> m ans
fh (eh m x -> (x -> m x) -> m x)
-> (eh (Eff '[eh] '[ef]) x -> eh m x)
-> eh (Eff '[eh] '[ef]) x
-> (x -> m x)
-> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff '[eh] '[ef] ~> m) -> eh (Eff '[eh] '[ef]) :-> eh m
forall (f :: * -> *) (g :: * -> *). (f :-> g) -> eh f :-> eh g
forall (h :: EffectH) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Eff '[eh] '[ef] i -> m i
Eff '[eh] '[ef] ~> m
loop) ef x -> (x -> m x) -> m x
Interpreter ef m x
forall ans x. ef x -> (x -> m ans) -> m ans
ff
{-# INLINE iterEffRecHFWith #-}

{- | Traverses a computation containing only higher-order effects @eh@ and first-order effects @ef@ using the provided value handler,
continuational stateful elaborator, and handler, transforming it into a monad @m@.
-}
iterEffHFBy
    :: forall eh ef m ans a
     . (Monad m, HFunctor eh)
    => (a -> m ans)
    -- ^ Value handler
    -> Interpreter (eh (Eff '[eh] '[ef])) m ans
    -- ^ Effect elaborator
    -> Interpreter ef m ans
    -- ^ Effect handler
    -> Eff '[eh] '[ef] a
    -> m ans
iterEffHFBy :: forall (eh :: EffectH) (ef :: * -> *) (m :: * -> *) ans a.
(Monad m, HFunctor eh) =>
(a -> m ans)
-> Interpreter (eh (Eff '[eh] '[ef])) m ans
-> Interpreter ef m ans
-> Eff '[eh] '[ef] a
-> m ans
iterEffHFBy a -> m ans
ret Interpreter (eh (Eff '[eh] '[ef])) m ans
elb Interpreter ef m ans
hdl = (a -> m ans)
-> Interpreter (UnionH '[eh] (Eff '[eh] '[ef])) m ans
-> Interpreter (Union '[ef]) m ans
-> Eff '[eh] '[ef] a
-> m ans
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> m ans
ret (eh (Eff '[eh] '[ef]) x -> (x -> m ans) -> m ans
Interpreter (eh (Eff '[eh] '[ef])) m ans
elb (eh (Eff '[eh] '[ef]) x -> (x -> m ans) -> m ans)
-> (UnionH '[eh] (Eff '[eh] '[ef]) x -> eh (Eff '[eh] '[ef]) x)
-> UnionH '[eh] (Eff '[eh] '[ef]) x
-> (x -> m ans)
-> m ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnionH '[eh] (Eff '[eh] '[ef]) x -> eh (Eff '[eh] '[ef]) x
forall (e :: EffectH) (f :: * -> *) a.
HFunctor e =>
UnionH '[e] f a -> e f a
extractH) (ef x -> (x -> m ans) -> m ans
Interpreter ef m ans
hdl (ef x -> (x -> m ans) -> m ans)
-> (Union '[ef] x -> ef x)
-> Union '[ef] x
-> (x -> m ans)
-> m ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Union '[ef] x -> ef x
forall (e :: * -> *) a. Union '[e] a -> e a
extract)
{-# INLINE iterEffHFBy #-}

-- | Traverses all effects using the provided value handler, continuational stateful elaborator, and handler, transforming them into a monad @m@.
iterAllEffHFBy
    :: forall eh ef m ans a
     . (Monad m)
    => (a -> m ans)
    -- ^ Value handler
    -> Interpreter (UnionH eh (Eff eh ef)) m ans
    -- ^ Effect elaborator
    -> Interpreter (Union ef) m ans
    -- ^ Effect handler
    -> Eff eh ef a
    -> m ans
iterAllEffHFBy :: forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy a -> m ans
ret Interpreter (UnionH eh (Eff eh ef)) m ans
fh Interpreter (Union ef) m ans
ff = Eff eh ef a -> m ans
loop
  where
    loop :: Eff eh ef a -> m ans
loop = \case
        Val a
x -> a -> m ans
ret a
x
        Op Either (UnionH eh (Eff eh ef) x) (Union ef x)
u FTCQueue (Eff eh ef) x a
q -> (UnionH eh (Eff eh ef) x -> (x -> m ans) -> m ans)
-> (Union ef x -> (x -> m ans) -> m ans)
-> Either (UnionH eh (Eff eh ef) x) (Union ef x)
-> (x -> m ans)
-> m ans
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either UnionH eh (Eff eh ef) x -> (x -> m ans) -> m ans
Interpreter (UnionH eh (Eff eh ef)) m ans
fh Union ef x -> (x -> m ans) -> m ans
Interpreter (Union ef) m ans
ff Either (UnionH eh (Eff eh ef) x) (Union ef x)
u x -> m ans
k
          where
            k :: x -> m ans
k = Eff eh ef a -> m ans
loop (Eff eh ef a -> m ans) -> (x -> Eff eh ef a) -> x -> m ans
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FTCQueue (Eff eh ef) x a -> x -> Eff eh ef a
forall (eh :: [EffectH]) (ef :: [* -> *]) a b.
FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
qApp FTCQueue (Eff eh ef) x a
q
{-# INLINE iterAllEffHFBy #-}

-- | Traverses all effects using the provided natural-transformation style elaborator and handler, transforming them into a monad @m@.
iterAllEffHF
    :: forall eh ef m
     . (Monad m)
    => UnionH eh ~~> m
    -- ^ Effect elaborator
    -> Union ef ~> m
    -- ^ Effect handler
    -> Eff eh ef ~> m
iterAllEffHF :: forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *).
Monad m =>
(UnionH eh ~~> m) -> (Union ef ~> m) -> Eff eh ef ~> m
iterAllEffHF UnionH eh ~~> m
fh Union ef ~> m
ff = Eff eh ef x -> m x
Eff eh ef ~> m
loop
  where
    loop :: Eff eh ef ~> m
    loop :: Eff eh ef ~> m
loop = \case
        Val x
x -> x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
x
        Op Either (UnionH eh (Eff eh ef) x) (Union ef x)
u FTCQueue (Eff eh ef) x x
q -> (UnionH eh (Eff eh ef) x -> m x)
-> (Union ef x -> m x)
-> Either (UnionH eh (Eff eh ef) x) (Union ef x)
-> m x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (UnionH eh m x -> m x
UnionH eh ~~> m
fh (UnionH eh m x -> m x)
-> (UnionH eh (Eff eh ef) x -> UnionH eh m x)
-> UnionH eh (Eff eh ef) x
-> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Eff eh ef ~> m) -> UnionH eh (Eff eh ef) x -> UnionH eh m x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh ef x -> m x
Eff eh ef ~> m
loop (UnionH eh (Eff eh ef) x -> m x)
-> (x -> m x) -> UnionH eh (Eff eh ef) x -> m x
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> x -> m x
k) (Union ef x -> m x
Union ef ~> m
ff (Union ef x -> m x) -> (x -> m x) -> Union ef x -> m x
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> x -> m x
k) Either (UnionH eh (Eff eh ef) x) (Union ef x)
u
          where
            k :: x -> m x
k = Eff eh ef x -> m x
Eff eh ef ~> m
loop (Eff eh ef x -> m x) -> (x -> Eff eh ef x) -> x -> m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FTCQueue (Eff eh ef) x x -> x -> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) a b.
FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
qApp FTCQueue (Eff eh ef) x x
q
{-# INLINE iterAllEffHF #-}

-- * Layer manipulation

splitLayer :: Eff '[] ef ~> Eff eh '[Eff '[] ef]
splitLayer :: forall (ef :: [* -> *]) (eh :: [EffectH]) x.
Eff '[] ef x -> Eff eh '[Eff '[] ef] x
splitLayer =
    (x -> Eff eh '[Eff '[] ef] x)
-> Interpreter (UnionH '[] (Eff '[] ef)) (Eff eh '[Eff '[] ef]) x
-> Interpreter (Union ef) (Eff eh '[Eff '[] ef]) x
-> Eff '[] ef x
-> Eff eh '[Eff '[] ef] x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy x -> Eff eh '[Eff '[] ef] x
forall a. a -> Eff eh '[Eff '[] ef] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UnionH '[] (Eff '[] ef) x
-> (x -> Eff eh '[Eff '[] ef] x) -> Eff eh '[Eff '[] ef] x
Interpreter (UnionH '[] (Eff '[] ef)) (Eff eh '[Eff '[] ef]) x
forall (f :: * -> *) a r. UnionH '[] f a -> r
nilH (\Union ef x
u x -> Eff eh '[Eff '[] ef] x
k -> Eff '[] ef x -> Eff eh '[Eff '[] ef] x
forall (e :: * -> *) (eh :: [EffectH]) (ef :: [* -> *]) x.
e x -> Eff eh (e : ef) x
send0 (Union ef x -> Eff '[] ef x
forall (ef :: [* -> *]) a (eh :: [EffectH]).
Union ef a -> Eff eh ef a
sendUnion Union ef x
u) Eff eh '[Eff '[] ef] x
-> (x -> Eff eh '[Eff '[] ef] x) -> Eff eh '[Eff '[] ef] x
forall a b.
Eff eh '[Eff '[] ef] a
-> (a -> Eff eh '[Eff '[] ef] b) -> Eff eh '[Eff '[] ef] b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Eff eh '[Eff '[] ef] x
k)

mergeLayer :: Eff eh '[Eff eh ef] ~> Eff eh ef
mergeLayer :: forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh '[Eff eh ef] x -> Eff eh ef x
mergeLayer =
    (x -> Eff eh ef x)
-> Interpreter (UnionH eh (Eff eh '[Eff eh ef])) (Eff eh ef) x
-> Interpreter (Union '[Eff eh ef]) (Eff eh ef) x
-> Eff eh '[Eff eh ef] x
-> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) (m :: * -> *) ans a.
Monad m =>
(a -> m ans)
-> Interpreter (UnionH eh (Eff eh ef)) m ans
-> Interpreter (Union ef) m ans
-> Eff eh ef a
-> m ans
iterAllEffHFBy
        x -> Eff eh ef x
forall a. a -> Eff eh ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (\UnionH eh (Eff eh '[Eff eh ef]) x
u x -> Eff eh ef x
k -> UnionH eh (Eff eh ef) x -> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) a.
UnionH eh (Eff eh ef) a -> Eff eh ef a
sendUnionH ((Eff eh '[Eff eh ef] ~> Eff eh ef)
-> UnionH eh (Eff eh '[Eff eh ef]) x -> UnionH eh (Eff eh ef) x
forall (f :: * -> *) (g :: * -> *) (es :: [EffectH]) a.
(f ~> g) -> UnionH es f a -> UnionH es g a
hfmapUnion Eff eh '[Eff eh ef] x -> Eff eh ef x
forall (eh :: [EffectH]) (ef :: [* -> *]) x.
Eff eh '[Eff eh ef] x -> Eff eh ef x
Eff eh '[Eff eh ef] ~> Eff eh ef
mergeLayer UnionH eh (Eff eh '[Eff eh ef]) x
u) Eff eh ef x -> (x -> Eff eh ef x) -> Eff eh ef x
forall a b. Eff eh ef a -> (a -> Eff eh ef b) -> Eff eh ef b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Eff eh ef x
k)
        (\Union '[Eff eh ef] x
u x -> Eff eh ef x
k -> Union '[Eff eh ef] x -> Eff eh ef x
forall (e :: * -> *) a. Union '[e] a -> e a
extract Union '[Eff eh ef] x
u Eff eh ef x -> (x -> Eff eh ef x) -> Eff eh ef x
forall a b. Eff eh ef a -> (a -> Eff eh ef b) -> Eff eh ef b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Eff eh ef x
k)

-- * Utilities

-- | Lifts a natural transformation into a continuational stateful interpreter.
stateless :: forall e m ans. (Monad m) => (e ~> m) -> Interpreter e m ans
stateless :: forall (e :: * -> *) (m :: * -> *) ans.
Monad m =>
(e ~> m) -> Interpreter e m ans
stateless e ~> m
i e x
e x -> m ans
k = e x -> m x
e ~> m
i e x
e m x -> (x -> m ans) -> m ans
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> m ans
k
{-# INLINE stateless #-}

-- | Applies a value to a Kleisli arrow in 'FTCQueue' representation.
qApp :: FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
qApp :: forall (eh :: [EffectH]) (ef :: [* -> *]) a b.
FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
qApp FTCQueue (Eff eh ef) a b
q' a
x = case FTCQueue (Eff eh ef) a b -> ViewL (Eff eh ef) a b
forall (m :: * -> *) a b. FTCQueue m a b -> ViewL m a b
tviewl FTCQueue (Eff eh ef) a b
q' of
    TOne a -> Eff eh ef b
k -> a -> Eff eh ef b
k a
x
    a -> Eff eh ef x
k :| FTCQueue (Eff eh ef) x b
t -> case a -> Eff eh ef x
k a
x of
        Val x
y -> FTCQueue (Eff eh ef) x b -> x -> Eff eh ef b
forall (eh :: [EffectH]) (ef :: [* -> *]) a b.
FTCQueue (Eff eh ef) a b -> a -> Eff eh ef b
qApp FTCQueue (Eff eh ef) x b
t x
y
        Op Either (UnionH eh (Eff eh ef) x) (Union ef x)
u FTCQueue (Eff eh ef) x x
q -> Either (UnionH eh (Eff eh ef) x) (Union ef x)
-> FTCQueue (Eff eh ef) x b -> Eff eh ef b
forall (eh :: [EffectH]) (ef :: [* -> *]) a x.
Either (UnionH eh (Eff eh ef) x) (Union ef x)
-> FTCQueue (Eff eh ef) x a -> Eff eh ef a
Op Either (UnionH eh (Eff eh ef) x) (Union ef x)
u (FTCQueue (Eff eh ef) x x
q FTCQueue (Eff eh ef) x x
-> FTCQueue (Eff eh ef) x b -> FTCQueue (Eff eh ef) x b
forall (m :: * -> *) a x b.
FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
>< FTCQueue (Eff eh ef) x b
t)