[Agda] Agda IO with session types

[Gregory Crosswhite]

  To shoot a question in the dark:  could your model be turned into an 
arrow?

Cheers,
Greg

On 10/18/2010 03:44 PM, Alan Jeffrey wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda