IO.lol

:load Pair.lol

:assume World : *
IO_Polytype (X:*) : *p
 = (Data:*) -> (data:(p:World -> Pair World X) -> Data) -> Data
IO (X:*) = Monotype (IO_Polytype X)

:load Monad.lol
Monad_return_IO (X:*)
 : Monad_Return IO X
 = λ(x:X) ->
     monotype (IO_Polytype X)
     (λ(Data:*) (data:(World -> Pair World X) -> Data) ->
       data (λ(w:World) -> pair World X w x))
Monad_bind_IO (X:*) (Y:*)
 : Monad_Bind IO X Y
 = λ(mx:IO X) (my:X -> IO Y) ->
   monotype (IO_Polytype Y)
     (λ(Data:*) (oy:(World -> Pair World Y) -> Data) ->
       polytype (IO_Polytype X) mx Data (λ(px:World -> Pair World X) ->
         oy (λ(w:World) ->
           uncurry World X (Pair World Y)
            (λ(w:World) (x:X) ->
              polytype (IO_Polytype Y) (my x) (Pair World Y) (λ(py:World -> Pair World Y) ->
                py w
              )
            )
            (px w)
         )
       )
     )
Monad_IO
 : Monad IO
 = monad IO
 Monad_return_IO
 Monad_bind_IO