Replay with Freer

F.hs

{-# LANGUAGE
    RankNTypes,
    ScopedTypeVariables,
    KindSignatures,
    GADTs
  #-}

import Data.Foldable (for_)
import System.IO (hFlush, stdout)

--
-- Freer in 9 LOC (without the monad instance)
--

data Freer (f :: * -> *) (a :: *) where
  Pure :: a -> Freer f a
  Eff :: f x -> (x -> Freer f a) -> Freer f a

-- Not used here
interp :: Monad m => (forall x. f x -> m x) -> Freer f a -> m a
interp _ (Pure a) = pure a
interp f (Eff e k) = do
  x <- f e
  interp f (k x)

--
-- Replaying Freer computations
--

-- Events are pairs (f x, x) of an effect (f x) and its result x
data Event (f :: * -> *) where
  Event :: f x -> x -> Event f

-- Traces are lists of events, we want to generate them when interpreting a Freer
-- computation and use them to replay.
type Trace f = [Event f]

-- We'd also like to serialize events to store them (deserialization omitted)
class SerializableEvent f where
  serializeEvent :: Event f -> String

-- A variant of interp that records the trace of interactions
interpTraced :: Monad m => (forall x. f x -> m x) -> Freer f a -> m (Trace f, a)
interpTraced _ (Pure a) = pure ([], a)
interpTraced f (Eff e k) = do
  x <- f e
  (t, a) <- interpTraced f (k x)
  pure (Event e x : t, a)

-- For replay, we want to compare the (f x) from an Event to the (f y)
-- in the Freer computation, and obtain a coercion (x ~ y) when they are equal.
class IxCoercible f where
  ixcoerce :: f x -> f y -> x -> Maybe y
  -- Must satisfy:
  --   ixcoerce e e x = Just x

-- Replay a Freer computation with a trace
retrace :: IxCoercible f => Trace f -> Freer f a -> Maybe a
retrace _ (Pure a) = Just a
retrace [] (Eff _ _) = Nothing  -- fails if trace is too short
retrace (Event e' x' : t) (Eff e k) = do
  x <- ixcoerce e' e x'  -- fails if the effects e and e' are mismatched
  retrace t (k x)

--
-- An example
--

-- A dead simple input-output API
data Cmd a where
  Read :: Cmd Int
  Write :: Int -> Cmd ()

-- IO semantics for Cmd
cmdToIO :: Cmd a -> IO a
cmdToIO Read = do
  putStr "< (Enter a number) " >> hFlush stdout
  read <$> getLine
cmdToIO (Write n) = putStrLn $ "> " ++ show n

instance IxCoercible Cmd where
  ixcoerce Read Read = Just
  ixcoerce (Write _) (Write _) = Just
  ixcoerce _ _ = \_ -> Nothing

instance SerializableEvent Cmd where
  serializeEvent (Event Read n) = "Read -> " ++ show n
  serializeEvent (Event (Write n) ()) = "Write <- " ++ show n

-- Example program
foobar :: Freer Cmd Int
foobar =
  Eff Read $ \n ->
  Eff Read $ \m ->
  Eff (Write (m + n)) $ \() ->
  Pure (m * n)

-- Play and replay foobar
main :: IO ()
main = do
  putStrLn "### Play foobar:"
  (t, a) <- interpTraced cmdToIO foobar
  putStrLn "### Serialized trace:"
  for_ t $ \e -> putStrLn (serializeEvent e)
  putStrLn "### Replay foobar:"
  case retrace t foobar of
    Just a' | a == a' -> putStrLn "Replay OK!"
            | otherwise -> fail $ "Replay gave unexpected result: " ++ show (a, a')
    Nothing -> fail "Oops, invalid trace"