Rewind monad

Rs.hs

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}

module Rs where

import           Control.Monad.Free
import qualified Data.Map as M

data RsF m next = ∀ a. RsCheckpoint Int (m a) (a → next) | RsRewind Int

deriving instance Functor (RsF m)

type Rs m = Free (RsF m)

checkpoint ∷ Int → m a → Rs m a
checkpoint ch m = liftF (RsCheckpoint ch m id)

rewind ∷ Int → Rs m a
rewind ch = liftF (RsRewind ch)

runRs ∷ Monad m ⇒ M.Map Int (Rs m a) → Rs m a → m a
runRs m (Pure a) = return a
runRs m cnt@(Free (RsCheckpoint ch action next)) = do
  a ← action
  runRs (M.insert ch cnt m) (next a)
runRs m (Free (RsRewind ch)) = do
  case M.lookup ch m of
    Just cnt → runRs m cnt
    Nothing  → error "Invalid checkpoint"

example ∷ IO ∅
example = runRs M.empty $ do
  checkpoint 1 $ putStrLn "Enter command: "
  a ← checkpoint 2 $ getLine
  if a ≡ "rewind"
    then rewind 1
    else checkpoint 3 $ putStrLn "Bye"