Playing with state effects in Idris

output

$ idris state.idr -p effects
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 0.9.14.3
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
*state> testAdd 1
12 : Nat

state.idr

import Effect.State

addFive : { [STATE Nat] } Eff (Nat)
addFive = do i <- get
             put (i + 5)
             pure 42 -- Communicate using shared state. Return a meaningless value.

addSix : { [STATE Nat] } Eff (Nat)
addSix = do i <- get
            put (i + 6)
            pure 24 -- Communicate using shared state. Return a meaningless value.

testAdd : Nat -> Nat
testAdd n = runPure (do put n
                        addFive
                        addSix
                        n' <- get
                        pure n')