[Agda] Agda IO with session types

[Alan Jeffrey]

Ah, this is very interesting.  Starting from your "Representations of 
stream processors..." paper, we have a lot in common, in particular your 
definition of P A B is exactly that of my ω⟨A⟩ ⇒ ω⟨B⟩, where ω : Session 
-> Session is the "infinite stream" construction, and ⟨_⟩ : Set -> 
Session is the "singleton stream" construction.

Now we move onto "Continuous functions on final coalgebras" and things 
are still very similar, but some differences pop up.  I generalized from 
sessions of the form ω⟨A⟩ to arbitrary sessions:

   data Session : Set₁ where
     [] : Session
     _∷_ : (A : Set) → (Ss : ∞ (A → Session)) → Session

which is indeed the terminal coalgebra:

   Session = nu X . (1 + Fam X)

using your definition:

   Fam X = Sigma (S : Set) S -> X

I think this is essentially the same as your construction.

The thing I didn't do is generalize the data from streams to arbitrary 
trees.  In the finite case (finite trees and finite index sets), this is 
cosmetic (well, apart from efficiency issues) in that any tree can be 
serialized (think XML).  In the infinite case, the serialization is a 
bit painful, as you have to interleave the child serializations, and 
moreover you have to interleave fairly.  I think this is connected to 
your comment (p. 8) "Of course, unless the position sets are restricted 
to be finite..."

If we had bidirectional transforms, then we could encode infinite trees 
quite easily, using a tensor which allows the recipient of a tree to 
decide how to explore it.  This is essentially the way that games 
semantics codes lollipop, and is the main motivating reason for allowing 
bidirectional processes!

I'll have to think about the generalization from data streams to trees. 
  The additional categorical structure would be nice (yay monoidal 
closed categories) but the construction may be quite fearsome.

A.

On 10/19/2010 02:21 AM, Peter Hancock wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda