{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

{- | For lifting arbitrary monadic computations into an algebraic effect setting.
-}

module Effects.Lift (
    Lift(..)
  , lift
  , handleLift) where

import Prog ( call, Member(prj), Prog(..) )
import Data.Function (fix)

-- | Lift a monadic computation @m a@ into the effect @Lift m@
newtype Lift m a = Lift (m a)

-- | Wrapper function for calling @Lift@
lift :: (Member (Lift m) es) => m a -> Prog es a
lift :: forall (m :: * -> *) (es :: [* -> *]) a.
Member (Lift m) es =>
m a -> Prog es a
lift = Lift m a -> Prog es a
forall (e :: * -> *) (es :: [* -> *]) x.
Member e es =>
e x -> Prog es x
call (Lift m a -> Prog es a) -> (m a -> Lift m a) -> m a -> Prog es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> Lift m a
forall (m :: * -> *) a. m a -> Lift m a
Lift

-- | Handle @Lift m@ as the last effect
handleLift :: forall m w. Monad m => Prog '[Lift m] w -> m w
handleLift :: forall (m :: * -> *) w. Monad m => Prog '[Lift m] w -> m w
handleLift (Val w
x) = w -> m w
forall (m :: * -> *) a. Monad m => a -> m a
return w
x
handleLift (Op EffectSum '[Lift m] x
u x -> Prog '[Lift m] w
q) = case EffectSum '[Lift m] x -> Maybe (Lift m x)
forall (e :: * -> *) (es :: [* -> *]) x.
Member e es =>
EffectSum es x -> Maybe (e x)
prj EffectSum '[Lift m] x
u of
     Just (Lift m x
m) -> m x
m m x -> (x -> m w) -> m w
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Prog '[Lift m] w -> m w
forall (m :: * -> *) w. Monad m => Prog '[Lift m] w -> m w
handleLift (Prog '[Lift m] w -> m w) -> (x -> Prog '[Lift m] w) -> x -> m w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Prog '[Lift m] w
q
     Maybe (Lift m x)
Nothing -> [Char] -> m w
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: Nothing cannot occur"