I/O Monads

Recursive and Corecursive Free Monads.

IO

Finite I/O

data IO (A: Type): Type :=
     (getLine: (String → IO) → IO)
     (putLine: String → IO → IO)
     (pure: A → IO)

Example:

record Main: Type :=
(main: IO.replicateM 100
       (IO.>>= IO.data () IO.getLine IO.putLine))