Control.IOI

v11.3.15 • Free IOI Comonad

Church-encoded Free IOI Comonad is a comonadic state machine defined by an anamorphism. It represents a process that can interact with its environment.

Types

IOI :: * -> *

The Church-encoded Free IO Comonad. It represents a potentially infinite state-based process (a machine) defined by an anamorphism.

Implementation

forall (x: *) .
  (forall (s: *) . s -> (s -> f r s) -> x) ->
  x

F :: * -> * -> *

The interaction functor for the IO stream. Describes the possible next steps of a process: output, input, or return.

Implementation

forall (x: *) .
  (data -> s -> x) ->
  ((data -> s) -> x) ->
  (r -> x) ->
  x

Foreigns

get_line :: Data

Leaf FFI shared with IO. Reads input from console.

Implementation

foreign get_line :: Data = henk_io get_line

put_line :: Data -> ()

Leaf FFI shared with IO. Writes output to console.

Implementation

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

Functions

iof_put_line_f :: String -> S -> F r S

Helper to construct a "write" step in the interaction functor.

Implementation

iof_put_line_f str ns x put_line_ get_line_ return_ =
  put_line_ str ns

iof_get_line_f :: (String -> S) -> F r S

Helper to construct a "read" step in the interaction functor.

Implementation

iof_get_line_f k x put_line_ get_line_ return_ =
  get_line_ k

iof_return_f :: r -> F r S

Helper to construct a terminal step in the interaction functor.

Implementation

iof_return_f vr x put_line_ get_line_ return_ =
  return_ vr

mk_io :: S -> (S -> F r S) -> IOI r

Creates an IOI process from an initial state and a step function (existential constructor).

Implementation

mk_io r s seed step x k = k s seed step

run_ioi :: IOI r -> r

Unpacks the existential machine and drives the loop.

Implementation

run_ioi ioi =
  ioi Any (\_s -> \seed -> \step -> run_ioi_step seed step)