I/O Monads

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

Infinity I/O Monads

Corecursive CoFree CoMonad

IOI

Infinite I/O

data IOI.F (A,State: Type): Type := (getLine: (String → State) → IO) (putLine: String → State → IO) (pure: A → IO) data IOI (A,State: Type) := (intro: State -> (State -> IOI.F A State) -> IOI)

Example:

record Main: Type := (main: λ (r: Type) -> IOI.MkIO r (Maybe IOI.data) (Maybe.Nothing IOI.data) ( λ (m: Maybe IOI.data) -> Maybe.maybe IOI.data m (IOI.F r (Maybe IOI.data)) ( λ (str: IOI.data) -> IOI.putLine r (Maybe IOI.data) str (Maybe.Nothing IOI.data)) (IOI.getLine r (Maybe IOI.data) (Maybe.Just IOI.data))))