[Agda] Choice sequences and effects

[Alan Jeffrey]

On 10/08/2011 02:25 PM, Peter Hancock wrote:
> 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.

That would be me then :-)

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

Programming over choice sequences is certainly one of the ways of 
programming IO, and indeed that's the basic idea behind my work with 
Julian Rathke on streaming I/O (The Lax Braided Structure of Streaming 
I/O, CSL 2011, http://ect.bell-labs.com/who/ajeffrey/papers/csl11.pdf), 
which was heavily influenced by your work on stream processing.

There is a somewhat cosmetic difference about whether you choose to work 
with indexed sets (as you do, and which codes the type's automaton 
explicitly with state set S) or with coinductive sets (which is what we 
did, and makes the automaton implicit). There are nasty issues about 
cardinalities and codes-of-sets vs. sets, but "morally" they're the same 
thing.

More interestingly, you're allowing R to depend on C, which is a gap in 
our approach. We worked with functions S -> T (subject to some sanity 
conditions), that is the state of T can't depend on the state of S, and 
vice versa. The generalization to allow state dependencies between S and 
T is a natural one, the only reason why we didn't go down that route is 
that it doesn't have an obvious categorical presentation, since C and R 
are dependent on each other.

There's been a lot of interest recently in multi-party session types, 
which may be relevant here (essentially C and R are types in a two-party 
session).

I think my only quibble with your approach is whether this is the only 
way of formalizing I/O. For example, many I/O models make use of unique 
name generation, time, nondeterminism, state ecapsulation, or other 
features which don't have immediate representations as functions over 
choice sequences.

A.

>
> 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 -> Fam2 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda