Corecursive I/O

I/O Library

Infinity I/O Monads

IOI

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