effect-monad-0.7.0.0: examples/Counter.hs

{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators, ScopedTypeVariables, ImplicitParams #-}

import Prelude hiding (Monad(..),map)
import Control.Effect
import Control.Effect.Counter

import Debug.Trace

{-

The 'Counter' graded monad is useful for counting computations
of a particular kind (e.g., counting number of calls to a websocket)
or estimating resource usage (e.g., a websocket call is more expensive
than a disk write).

By default, zero counts are tracked, e.g.,

-}

foo :: Counter Z Int
foo = do x <- return 2
         y <- return 4
         return (x + y)

{- the 'tick' function lifts a value to be counted once, e.g. -}

-- foo2 :: Counter (S Z) Int
foo2 = do x <- tick 2
          y <- return 3
          return (x * y)

zero :: Counter Z Int
zero = do x <- return 2
          y <- return 4
          return (x + y)

{- This can be used for other cool things, like proving that 'map' has
 linear complexity of 'map' at the type-level!

For this we need sized lists:
-}

data Vector n a where
    Nil :: Vector Z a
    Cons :: a -> Vector n a -> Vector (S n) a

type family n :* m where
            Z     :* m = Z
            (S n) :* m = m :+ (n :* m)

map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)
map' f Nil         = return Nil
map' f (Cons x xs) = do x' <- f x
                        xs' <- map' f xs
                        return (Cons x' xs')











map :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)
map f Nil         = return Nil
map f (Cons x xs) = do x' <- f x
                       xs' <- map f xs
                       return (Cons x' xs')

class Bar n where
instance Bar Z where
instance Bar n => Bar (S n) where

data Listy n a where
    Nily :: Listy Z a
    Consy :: (Bar n) => a -> Listy n a -> Listy (S n) a

fooo :: Listy n a -> Int
fooo Nily = 0
fooo (Consy x (Consy y xs)) = 2 + (fooo xs)
fooo (Consy x xs) = 1 + (fooo xs)

{- The types show us that if the function counts 't' things, then applying 'map
to an n-vector counts 'tn' things -}

{- Example: web socket calls- how many do we do per instances #-}

call :: Int -> Counter (S Z) ()
call = undefined

singleCall = map call (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))

doubleCall x = map (\n -> do {a <- call n; b <- call n; return ()}) x

doubleCallExample = doubleCall (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))




{- are we definitely linear in the number of elements, even if we have closed over the vector? -}

class LT n m
instance LT Z (S n)
instance LT n m => LT (S n) (S m)

lineraMap :: LT t n => (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)
lineraMap = map