Control.IO

IO :: * -> *

The Church-encoded Free IO Monad. It represents a calculation that can perform effects via handles (get_line, put_line) and eventually returns a pure value.

Implementation

forall (r: *) .
  ((data -> r) -> r) ->
  (data -> (() -> r) -> r) ->
  (a -> r) ->
  r

get_line :: Data

Leaf FFI: the primitive console operation to read input from standard input.

Implementation

foreign get_line :: Data = henk_io get_line

put_line :: Data -> ()

Leaf FFI: the primitive console operation to write output to standard output.

Implementation

foreign put_line :: Data -> () = henk_io put_line

io_pure :: A -> IO A

Lifts a pure value into the IO monad.

Implementation

io_pure x io_r get_line_ put_line_ pure_ = pure_ x

Usage

io_pure 5

io_get_line :: IO String

Abstract action that requests a line of text via handles.

Implementation

io_get_line io_r get_line_ put_line_ pure_
  = get_line_ pure_

io_put_line :: String -> IO ()

Abstract action that requests to display a string via handles.

Implementation

io_put_line str io_r get_line_ put_line_ pure_ =
  put_line_ str (\_ -> pure_ tt)

io_bind :: IO A -> (A -> IO B) -> IO B

Monadic bind for sequencing IO actions.

Implementation

io_bind m f io_r get_line_ put_line_ pure_ =
  m io_r get_line_ put_line_
    (\a -> f a io_r get_line_ put_line_ pure_)

run_io :: IO A -> A

Interpreter for the IO action. Written in Henk as a Church fold.

Implementation

run_io action = action Any io_get_handler io_put_handler io_pure_handler

replicate_io :: Nat -> IO () -> IO ()

Repeats an IO action N times sequentially.

Implementation

replicate_io n action = case n of
    Zero   -> io_pure tt
    Succ p -> io_bind action (\_ -> replicate_io p action)

Usage

greet_thrice = replicate_io (Succ (Succ (Succ Zero))) 
                            (io_put_line "Hi!")