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
Witness :: (Token s b -> a) -> Witness s a
instance Functor (Witness s) where
fmap f (Witness g) = Witness (f . g)
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 (Witness id)
runWitness :: (forall s. Effect (Witness s :+ l) a) -> Effect l a
runWitness effect = run effect
where
run = eliminate return $ \(Witness k) ->
k $ Token $ unsafePerformIO newUnique