Cleff.Internal.Stack

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.

Documentation

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

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])

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

newtype HandlerPtr (e :: Effect)

A pointer to an effect handler.

Constructors

HandlerPtr

Fields

• unHandlerPtr :: Int

Construction

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

Type level list concatenation.

Equations

'[] ++ ys = ys

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

empty :: Stack '[]

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

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

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

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

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

Deconstruction

class KnownList (es :: [Effect])

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

Instances

KnownList ('[] :: [Effect])

Defined in Cleff.Internal.Stack

Methods

reifyLen :: Int

KnownList es => KnownList (e ': es)

Defined in Cleff.Internal.Stack

Methods

reifyLen :: Int

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

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

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

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

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

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

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

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

Retrieval and updating

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

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

Instances

(TypeError (ElemNotFound e) :: Constraint) => e :> ('[] :: [Effect])

Defined in Cleff.Internal.Stack

Methods

reifyIndex :: Int

e :> es => e :> (e' ': es)

Defined in Cleff.Internal.Stack

Methods

reifyIndex :: Int

e :> (e ': es)

The element closer to the head takes priority.

Defined in Cleff.Internal.Stack

Methods

reifyIndex :: Int

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

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])

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

Instances

Subset ('[] :: [Effect]) es

Defined in Cleff.Internal.Stack

Methods

reifyIndices :: [Int]

(Subset es es', e :> es') => Subset (e ': es) es'

Defined in Cleff.Internal.Stack

Methods

reifyIndices :: [Int]

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

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

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

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

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

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