FullIOSpecMonad.idr

implementation Functor IOSpec where
  map f = assert_total recur where
    recur (Pure a) = Pure (f a)
    recur (ReadLine cont) = ReadLine (recur . cont)
    recur (WriteLine s next) = WriteLine s (recur next)

implementation Applicative IOSpec where
  pure = Pure
  (<*>) pf a = assert_total (recur pf) where
    recur (Pure f) = map f a
    recur (ReadLine cont) = ReadLine (recur . cont)
    recur (WriteLine s next) = WriteLine s (recur next)

implementation Monad IOSpec where
  (>>=) ma f = assert_total (recur ma) where
    recur (Pure a) = f a
    recur (ReadLine cont) = ReadLine (recur . cont)
    recur (WriteLine s next) = WriteLine s (recur next)