IO

IO

FINITE

Finite I/O is recursive free monad represented as inductive type IO.

foldNat : Nat -> (a -> a) -> a -> a foldNat Zero f x = x foldNat (Succ m) f x = f (foldNat m f x) data IO r = PutStrLn String (IO r) | GetLine (String -> IO r) | Return r putStrLn : String -> IO U putStrLn str = PutStrLn str (Return Unit) getLine : IO String getLine = GetLine Return return : a -> IO a return = Return (>>=) : IO a -> (a -> IO b) -> IO b PutStrLn str io >>= f = PutStrLn str (io >>= f) GetLine k >>= f = GetLine (\str -> k str >>= f) Return r >>= f = f r replicateM : Nat -> IO U -> IO U replicateM n io = foldNat n (io >>) (return Unit) recursion : IO U -- over Nat = replicateM 5 (getLine >>= putStrLn)