To clarify coolsunglasses's note that it is actually possible to hide side effects behind a pure interface (when they can be proven pure) here's the "counter" e

To clarify coolsunglasses's note that it is actually possible to hide side effects behind a pure interface (when they can be proven pure) here's the "counter" example in the paper import Control.Monad.ST import Data.STRef data Counter s = Counter { get :: ST s a, inc :: ST s () } mkCounter :: STRef s Int -> Counter s mkCounter v = Counter (readSTRef v) (incRef v) where incRef ref = do i <- readSTRef v writeSTRef v (i + 1) A little noisier since we note that reading the ref is an impure action and we track a phantom `s` parameter around in order to convince Haskell that certain uses of counters are pure. Now comp :: ST s Int comp = do v <- newSTRef 0 let c = mkCounter v inc c inc c inc c get c This is technically a pure computation despite using an impure mechanism internally. We can get Haskell to prove this for us pureComp :: Int pureComp = runST comp Here `runST :: (forall s . ST s a) -> a` completes the proof that if the `s` variables in a computation are completely undetermined then that computation must be pure.