examples from https://github.com/dorchard/effectful-explanations-talk

GradedMonad.idr

module GradedMonad

import Data.Vect

%default total
%access public export

interface GMonad (g : k -> Type -> Type) where
  Zero : k
  Plus : k -> k -> k
  pure : a -> g Zero a
  (>>=) : g x a -> (a -> g y b) -> g (Plus x y) b
  (>>) : g x a -> g y b -> g (Plus x y) b
  (>>) x y = x >>= const y

-- Counter  

record Counter (n : Nat) (a : Type) where
  constructor MkCounter 
  forget : a

GMonad Counter where
  Zero = Z
  Plus = (+)
  pure = MkCounter
  (MkCounter a) >>= k = MkCounter . forget $ k a  

tick : Counter (S Z) ()
tick = MkCounter ()  

example : Int -> Counter (S (S Z)) Int
example x = do tick
               tick
               pure {g=Counter} (2*x)

countmap : (a -> Counter t b) -> Vect n a -> Counter (n * t) (Vect n b)
countmap     _ []                = pure {g=Counter} Vect.Nil
countmap {t} f ((::) {len} x xs) = rewrite sym $ plusZeroRightNeutral (len*t) in 
                                   do y  <- f x
                                      ys <- countmap f xs
                                      pure {g=Counter} $ y::ys  

-- Security

data Lattice = Public | Private

record Level (l : Lattice) (a : Type) where
  constructor MkLevel
  unwrap : a
  
join : Lattice -> Lattice -> Lattice
join Private _       = Private
join _       Private = Private
join Public  Public  = Public  

GMonad Level where
  Zero = Public
  Plus = join
  pure = MkLevel
  (MkLevel x) >>= k = MkLevel . unwrap $ k x

upcast : Level Public a -> Level Private a
upcast (MkLevel x) = MkLevel x  

secretPin : Level Private Int
secretPin = upcast (pure {g=Level} 12345)

hash : Int -> Level Public Int
hash x = pure {g=Level} (x * x * x)

salt : Level Private Int
salt = do pin <- secretPin
          h   <- hash pin
          pure {g=Level} (h + 1234)