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

module Control.Effect.Counter(Z, S, Counter, tick, (:+)) where

import Control.Effect
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 -}

{-| Define type constructors for natural numbers -}
data Z
data S n

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

{-| Type-level addition -}
type family n :+ m 
type instance n :+ Z     = n
type instance n :+ (S m) = S (n :+ m)

instance Effect Counter where
    type Inv Counter n m = ()

    {-| Trivial effect annotation is 0 -}
    type Unit Counter = Z
    {-| 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 (S Z) a
tick x = Counter x