Copyright	(c) 2021 Xy Ren
License	BSD3
Maintainer	xy.r@outlook.com
Stability	unstable
Portability	non-portable (GHC only)
Safe Haskell	None
Language	Haskell2010

Cleff.Internal.Stack

Contents

Construction
Deconstruction
Retrieval and updating

Description

This module defines the effect stack as an immutable extensible stack type, and provides functions for manipulating it. The effect stack type has the following time complexities:

Lookup: Amortized \( O(1) \).
Update: \( O(n) \).
Shrink: \( O(1) \).
Append: \( O(n) \).

This is an internal module and its API may change even between minor versions. Therefore you should be extra careful if you're to depend on this module.

Synopsis

type Effect = (Type -> Type) -> Type -> Type
data Stack (es :: [Effect])
newtype HandlerPtr (e :: Effect) = HandlerPtr {
- unHandlerPtr :: Int
}
type family xs ++ ys where ...
empty :: Stack '[]
cons :: HandlerPtr e -> Stack es -> Stack (e ': es)
concat :: Stack es -> Stack es' -> Stack (es ++ es')
class KnownList (es :: [Effect])
head :: Stack (e ': es) -> HandlerPtr e
take :: forall es es'. KnownList es => Stack (es ++ es') -> Stack es
tail :: Stack (e ': es) -> Stack es
drop :: forall es es'. KnownList es => Stack (es ++ es') -> Stack es'
class (e :: Effect) :> (es :: [Effect])
type family xs :>> es :: Constraint where ...
class KnownList es => Subset (es :: [Effect]) (es' :: [Effect])
index :: forall e es. e :> es => Stack es -> HandlerPtr e
pick :: forall es es'. Subset es es' => Stack es' -> Stack es
update :: forall e es. e :> es => HandlerPtr e -> Stack es -> Stack es

Documentation

type Effect = (Type -> Type) -> Type -> Type Source #

The type of effects. An effect e m a takes an effect monad type m :: Type -> Type and a result type a :: Type.

data Stack (es :: [Effect]) Source #

The effect stack, storing pointers to handlers. It is essentially an extensible stack type supporting efficient \( O(1) \) reads.

newtype HandlerPtr (e :: Effect) Source #

A pointer to an effect handler.

Constructors

HandlerPtr
Fields unHandlerPtr :: Int

Construction

type family xs ++ ys where ... infixr 5 Source #

Type level list concatenation.

Equations

'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)

empty :: Stack '[] Source #

Create an empty stack. \( O(1) \).

cons :: HandlerPtr e -> Stack es -> Stack (e ': es) Source #

Prepend one entry to the stack. \( O(n) \).

concat :: Stack es -> Stack es' -> Stack (es ++ es') Source #

Concatenate two stacks. \( O(m+n) \).

Deconstruction

class KnownList (es :: [Effect]) Source #

KnownList es means the list es is concrete, i.e. is of the form '[a1, a2, ..., an] instead of a type variable.

Instances

Instances details

KnownList ('[] :: [Effect]) Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyLen :: Int
KnownList es => KnownList (e ': es) Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyLen :: Int

head :: Stack (e ': es) -> HandlerPtr e Source #

Get the head of the stack. \( O(1) \).

take :: forall es es'. KnownList es => Stack (es ++ es') -> Stack es Source #

Take elements from the top of the stack. \( O(m) \).

tail :: Stack (e ': es) -> Stack es Source #

Slice off one entry from the top of the stack. \( O(1) \).

drop :: forall es es'. KnownList es => Stack (es ++ es') -> Stack es' Source #

Slice off several entries from the top of the stack. \( O(1) \).

Retrieval and updating

class (e :: Effect) :> (es :: [Effect]) infix 0 Source #

e :> es means the effect e is present in the effect stack es, and therefore can be sended in an Eff es computation.

Instances

Instances details

(TypeError (ElemNotFound e) :: Constraint) => e :> ('[] :: [Effect]) Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyIndex :: Int
e :> es => e :> (e' ': es) Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyIndex :: Int
e :> (e ': es) Source #	The element closer to the head takes priority.
Instance details Defined in Cleff.Internal.Stack Methods reifyIndex :: Int

type family xs :>> es :: Constraint where ... infix 0 Source #

xs :>> es means the list of effects xs are all present in the effect stack es. This is a convenient type alias for (e1 :> es, ..., en :> es).

Equations

'[] :>> _ = ()
(x ': xs) :>> es = (x :> es, xs :>> es)

class KnownList es => Subset (es :: [Effect]) (es' :: [Effect]) Source #

es is a subset of es', i.e. all elements of es are in es'.

Instances

Instances details

Subset ('[] :: [Effect]) es Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyIndices :: [Int]
(Subset es es', e :> es') => Subset (e ': es) es' Source #
Instance details Defined in Cleff.Internal.Stack Methods reifyIndices :: [Int]

index :: forall e es. e :> es => Stack es -> HandlerPtr e Source #

Get an element in the stack. Amortized \( O(1) \).

pick :: forall es es'. Subset es es' => Stack es' -> Stack es Source #

Get a subset of the stack. Amortized \( O(m) \).

update :: forall e es. e :> es => HandlerPtr e -> Stack es -> Stack es Source #

Update an entry in the stack. \( O(n) \).