{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds #-}

module Control.Effect.CounterNat where

import Control.Effect
import GHC.TypeLits
import Prelude hiding (Monad(..))

{-| 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 'GHC.TypeLits' -}

{-| The counter has no semantic meaning -}
data Counter (n :: Nat) a = Counter { forget :: a }

instance Effect Counter where
    type Inv Counter n m = ()
    {-| Trivial effect annotation is 0 -}
    type Unit Counter = 0
    {-| Compose effects by addition -}
    type Plus Counter n m = n + m

    return a = Counter a   
    (Counter a) >>= k = Counter . forget $ k a

{-| A 'tick' provides a way to increment the counter -}
tick :: a -> Counter 1 a
tick x = Counter x