calculus/Calculus/Lambda/Omega/Explicit/lib/IO.cloe

   1 :load Pair.cloe
   2
   3 :assume World : *
   4 IO_Polytype (X:*) : *p
   5  = (Data:*) -> (data:(p:World -> Pair World X) -> Data) -> Data
   6 IO (X:*) = Monotype (IO_Polytype X)
   7
   8 :load Monad.cloe
   9 Monad_return_IO (X:*)
  10  : Monad_Return IO X
  11  = λ(x:X) ->
  12      monotype (IO_Polytype X)
  13      (λ(Data:*) (data:(World -> Pair World X) -> Data) ->
  14        data (λ(w:World) -> pair World X w x))
  15 Monad_bind_IO (X:*) (Y:*)
  16  : Monad_Bind IO X Y
  17  = λ(mx:IO X) (my:X -> IO Y) ->
  18    monotype (IO_Polytype Y)
  19      (λ(Data:*) (oy:(World -> Pair World Y) -> Data) ->
  20        polytype (IO_Polytype X) mx Data (λ(px:World -> Pair World X) ->
  21          oy (λ(w:World) ->
  22            uncurry World X (Pair World Y)
  23             (λ(w:World) (x:X) ->
  24               polytype (IO_Polytype Y) (my x) (Pair World Y) (λ(py:World -> Pair World Y) ->
  25                 py w
  26               )
  27             )
  28             (px w)
  29          )
  30        )
  31      )
  32 Monad_List
  33  : Monad IO
  34  = monad IO
  35  Monad_return_IO
  36  Monad_bind_IO