[Agda] Agda IO with session types

[Peter Hancock]

On 18/10/2010 23:44, Alan Jeffrey wrote:
> Hi everyone,
> 
> I commited an experimental fragment of an IO library to:
> 
>   http://github.com/agda/agda-system-io

I found this very interesting.  It is in some respects very similar to 
some work I published with Neil Ghani and Dirk Pattinson that people
call "eating", particularly "container eating", which means 
defining continuous functions between final coalgebras for containers. 
   http://www.sciencedirect.com/science/journal/15710661
There is indeed a "simple input-output process language", in which the 
programs are built up both inductively and coinductively.  Continuity
corresponds to productivity. 

If I understand it right, your session types correspond to elements
of the final coalgebra for a container (these objects constrain what
can happen, and in what order; there is something corresponding to
&, which is a kind of append operation).  A container is a functor
of the form (Sigma x : A) B x -> X. 

The tricky part of our construction was to define composition so it 
stood a chance of being associative.  This required thinking of 
the processes as reading a whole indexed family of input streams,
as it were in lock-step.  On the output side too, things are emitted
in "horizontal slices". 

I have some elderly Agda (some of it Agda version 1) where I type-checked
this stuff.  It turned out to be a particular (unindexed) case of something I did
earlier with Pierre Hyvernat, on formal topology.  It took me some time
to notice this.
   http://authors.elsevier.com/sd/article/S0168007205000710
This too can be seen as "eating" final coalgebras, not for containers,
but for *indexed* containers.  The definition of composition is 
pretty intricate, but essentially the same as in container
eating.  I have some bit-rotted Agda where I type-checked it. 

By the way, the category one gets is fairly interesting, as there
are adjoint functors (A \otimes) and (A \lollipop) corresponding
to lock-step synchronisation with A, and simulation of A. 
To be precise, the objects in the category are what I call 
interfaces (they can also be seen as games).  
An interface is a pointed coalgebra for an indexed container over a 
set S of indices (and so represents an element of the final
coalgebra for the container).  A morphism is a simulation
of a certain kind. 

> We can construct interesting categorical structure in this setting: _&_ forms a product (though once you get outside the monoidal fragment, buffering is required, which can be expensive!), there is also a coproduct, option, Kleene star, etc.

All of our work (somewhat unrealistically) assumed unbounded buffering between processes, so it
really was applicable only to "pipelines", without loops.  

> 
> There are some limitations to this model, notably it only supports left-to-right communication, and as a result only has monoidal structure, not monoidal closed structure.  I'm thinking about extending it from transducers to a games semantics model, which would make _⇒_ an operation on sessions (or arenas if you prefer), with its usual definition in terms of perp and tensor.
> 

This sounds very familiar; except we found there *is* some closed monoidal structure around the notion 
of lockstep synchronisation. 

> The games model is quite a bit more complex, but the power of bidirectional and higher-order communication might be worth it.
> 

I had some fun trying to imagine what these things are, but failed. 

Peter Hancock