Control.Effect.Counter

Documentation

data Z

Provides a way to count in the type-level with a monadic interface to sum up the individual counts of subcomputations

Define type constructors for natural numbers

Instances

type n :+ Z = n

data S n

Instances

type n :+ (S m) = S ((:+) n m)

data Counter n a

The counter has no semantic meaning

Instances

Effect * Counter

type Unit * Counter = Z

type Plus * Counter n m = (:+) n m

type Inv * Counter n m = ()

tick :: a -> Counter (S Z) a

A tick provides a way to increment the counter

type family n :+ m

Type-level addition

Instances

type n :+ Z = n

type n :+ (S m) = S ((:+) n m)