[Agda] Choice sequences and effects

[Peter Hancock]

There may be some people on the list interested in how to write
input-output programs that actually do things, where the programs are
terms in an Agda-like type theory.

With all due diffidence, and apologies for being unclear,
I think writing such programs is
essentially programming with choice sequences of a generalised form.

A generalised choice sequence lives in a type of the form (nu F s),
ie. an instance of a coinductive family (nu F) of type Set^S = S -> Set
where F is an functor on indexed sets : Set^S, and s is an index.
The functor F must be container-like: a S-sorted signature in the
form of an S-indexed container

	S -> Fam^2 S

with outermost index  C and innermost R, so the container
has the form

         s |-> (C s, c |-> (R s c, r |-> n s c r))

In the most interesting case, F has the form G', which has
the same type as G, but has a state space (1 + (Sigma : g.S)g.C s),
with a special initial state inL () and a subsequent reversal of the roles C and R.  Essentially,
the first player chooses the initial state, and then play proceeds with roles reversed.

Temporarily at least, this seems to me a very reasonable model of external-world resources, like
access to measurements of the external world's state, or a means to change it.

I don't really kown what the practical implications of this view are. Maybe the IO-interface
should be structured in terms of the I/O-resources (file storage, network, physical world, peripherals)
a program may access.

Hank