[Agda] Agda IO with session types

[Alan Jeffrey]

Hi everyone,

I commited an experimental fragment of an IO library to:

   http://github.com/agda/agda-system-io

The idea is to explore how to get the benefit of iteratee IO in Agda, 
but be as typesafe as possible.

The model is based on a simple input-output process language, for 
example a process which adds two numbers is:

add : ⟨ ℕ ⟩ & ⟨ ℕ ⟩ ⇒ ⟨ ℕ ⟩
add = inp (♯ λ x → inp (♯ λ y → out (x + y) done))

The interesting part of this is the type...

* S ⇒ T is the type of processes with input session S and output session T.

* ⟨ ℕ ⟩ is the session with only one action, which is a natural number.

* S & T is session concatenation.

Running this on a completed trace:

runAdd = C⟦ add ⟧ ( 3 ∷ 5 ∷ [] )

gives the expected answer 8 ∷ [].  I've not done the gluing into the IO 
model yet, but it should be pretty easy to give safe IO bindings, e.g. 
executing at top level a process of type Bytes ⇒ Bytes.

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.

The composition in the category is given by parallel composition with 
quite a simple definition, based on the expansion laws for CCS:

_⟫_ : ∀ {S T U} → (S ⇒ T) → (T ⇒ U) → (S ⇒ U)
P       ⟫ out c Q = out c (P ⟫ Q)
inp F   ⟫ Q       = inp (♯ λ a → ♭ F a ⟫ Q)
out b P ⟫ inp G   = P ⟫ ♭ G b
P       ⟫ done    = P
done    ⟫ Q       = Q

Note that since output is inductive, parallel composition terminates 
even though input is coinductive.

The equivalent of iteratees comes from performing the usual premonoidal 
state transformer construction: stateful morphisms from T to U with 
state S are stateless morphisms from T & S to U & S.  In particular, 
when T is [] we get the usual type for parsers S ⇒ U & S.

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.

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

A.