IO

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))