IOI

INFINITE

Infinite I/O is corecursive cofree comonad represented as coinductive type IOI.

data IOF r s
   = PutStrLn String s
   | GetLine (String -> s)
   | Return r

maybe : (a -> b) -> b -> Maybe a -> b
Just : a -> Maybe a

data IOI r
   = forall s . MkIO s (s -> IOF r s)

corecursion : IOI ()
   = MkIO
     Nothing
     (maybe (\ s -> PutStrLn s Nothing)
            (GetLine Just))

In pure functions:

   \ (r : *1)
-> #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)
       )
  )