{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Effects.Lift (
Lift(..)
, lift
, handleLift) where
import Prog ( call, Member(prj), Prog(..) )
import Data.Function (fix)
newtype Lift m a = Lift (m a)
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
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"