Control.Effect.CounterNat

Documentation

data Counter (n :: Nat) a

Provides a way to count in the type-level with a monadic interface to sum up the individual counts of subcomputations. Instead of using our own inductive natural number typ, this uses the Nat kind from TypeLits

The counter has no semantic meaning

Constructors

Counter

Fields

• forget :: a

Instances

Effect Nat Counter

Associated Types

type Unit Counter (m :: Counter -> * -> *) :: k

type Plus Counter (m :: Counter -> * -> *) (f :: Counter) (g :: Counter) :: k

type Inv Counter (m :: Counter -> * -> *) (f :: Counter) (g :: Counter) :: Constraint

Methods

return :: a -> m (Unit Counter m) a

(>>=) :: Inv Counter m f g => m f a -> (a -> m g b) -> m (Plus Counter m f g) b

(>>) :: Inv Counter m f g => m f a -> m g b -> m (Plus Counter m f g) b

type Unit Nat Counter

type Unit Nat Counter = 0

type Plus Nat Counter n m

type Plus Nat Counter n m = (+) n m

type Inv Nat Counter n m

type Inv Nat Counter n m = ()

tick :: a -> Counter 1 a

A tick provides a way to increment the counter