Safe Haskell	None
Language	Haskell2010

Control.Monad.Stack.Internal

Synopsis

type family Pop (c :: k) (m :: k') :: k'
type family IteratePop (n :: Nat) (c :: k) (m :: Type -> Type) :: Type -> Type where ...
type family StackConstraints (n :: Nat) (c :: k) (cSucc :: k' -> Constraint) (m :: k') where ...
predNat :: forall (n :: Nat). KnownNat n => Either (n :~: 0) (Dict (KnownNat (n - 1)))
nonZeroNat :: forall {k} (n :: Natural) (c :: k) cSucc (m :: Type -> Type) a. KnownNat (n - 1) => (IteratePop n c m a :~: IteratePop (n - 1) c (Pop c m) a, StackConstraints n c cSucc m :~: (cSucc m, StackConstraints (n - 1) c cSucc (Pop c m)))
depth :: forall {k} (n :: Nat) (c :: k) cSucc m a. (KnownNat n, StackConstraints n c cSucc m) => (forall (m1 :: Type -> Type). cSucc m1 => Pop c m1 a -> m1 a) -> IteratePop n c m a -> m a
data ContTag
module GHC.TypeNats

Documentation

type family Pop (c :: k) (m :: k') :: k' Source #

Instances details

type Pop ContTag (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Cont type Pop ContTag (m :: Type -> Type) = PopCont m
type Pop MaybeT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Fail type Pop MaybeT (m :: Type -> Type) = PopFail m
type Pop AccumT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Accum type Pop AccumT (m :: Type -> Type) = PopAccum m
type Pop ExceptT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Error type Pop ExceptT (m :: Type -> Type) = PopError m
type Pop ReaderT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Reader type Pop ReaderT (m :: Type -> Type) = PopReader m
type Pop SelectT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Select type Pop SelectT (m :: Type -> Type) = PopSelect m
type Pop StateT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.State type Pop StateT (m :: Type -> Type) = PopState m
type Pop WriterT (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Writer type Pop WriterT (m :: Type -> Type) = PopWriter m

type family IteratePop (n :: Nat) (c :: k) (m :: Type -> Type) :: Type -> Type where ... Source #

Equations

IteratePop 0 (c :: k) m = m
IteratePop n (c :: k) m = IteratePop (n - 1) c (Pop c m)

type family StackConstraints (n :: Nat) (c :: k) (cSucc :: k' -> Constraint) (m :: k') where ... Source #

Equations

StackConstraints 0 (c :: k) (cSucc :: k' -> Constraint) (m :: k') = ()
StackConstraints n (c :: k) (cSucc :: k' -> Constraint) (m :: k') = (cSucc m, StackConstraints (n - 1) c cSucc (Pop c m))

predNat :: forall (n :: Nat). KnownNat n => Either (n :~: 0) (Dict (KnownNat (n - 1))) Source #

nonZeroNat :: forall {k} (n :: Natural) (c :: k) cSucc (m :: Type -> Type) a. KnownNat (n - 1) => (IteratePop n c m a :~: IteratePop (n - 1) c (Pop c m) a, StackConstraints n c cSucc m :~: (cSucc m, StackConstraints (n - 1) c cSucc (Pop c m))) Source #

depth :: forall {k} (n :: Nat) (c :: k) cSucc m a. (KnownNat n, StackConstraints n c cSucc m) => (forall (m1 :: Type -> Type). cSucc m1 => Pop c m1 a -> m1 a) -> IteratePop n c m a -> m a Source #

ContT is polykinded, which leads to issues checking that ContT ~ ContT!

Instances details

type Pop ContTag (m :: Type -> Type) Source #
Instance details Defined in Control.Monad.Stack.Cont type Pop ContTag (m :: Type -> Type) = PopCont m