module Control.Effect.Witness (
EffectWitness, Witness, runWitness,
Token, newToken
) where
import Control.Monad.Effect
import Data.Type.Equality ((:~:) (..), TestEquality (..))
import Data.Unique (Unique, newUnique)
import System.IO.Unsafe (unsafePerformIO)
import Unsafe.Coerce (unsafeCoerce)
newtype Token s a = Token Unique
deriving Eq
instance TestEquality (Token s) where
testEquality (Token i) (Token j)
| i == j = Just unsafeRefl
| otherwise = Nothing
unsafeRefl :: a :~: b
unsafeRefl = unsafeCoerce Refl
data Witness s a where
NewToken :: Witness s (Token s a)
type instance Is Witness f = IsWitness f
type family IsWitness f where
IsWitness (Witness s) = 'True
IsWitness f = 'False
class MemberEffect Witness (Witness s) l => EffectWitness s l
instance MemberEffect Witness (Witness s) l => EffectWitness s l
type family WitnessType l where
WitnessType (Witness s ': l) = s
WitnessType (e ': l) = WitnessType l
newToken :: EffectWitness s l => Effect l (Token s a)
newToken = send NewToken
runWitness :: (forall s. Effect (Witness s ':+ l) a) -> Effect l a
runWitness effect = run effect
where
run = eliminate return $ \NewToken k ->
k $ Token $ unsafePerformIO newUnique