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)