[Agda] Agda IO with session types

[Alan Jeffrey]

On 10/18/2010 05:49 PM, Gregory Crosswhite wrote:
>    To shoot a question in the dark:  could your model be turned into an
> arrow?

Hmm, I don't think so, at least not without hoop-jumping.  IIRC, arrows 
form a Freyd category where the center is Set (that is, there's an 
identity-on-objects functor F : Set -> C which maps the product 
structure in Set to the premonoidal structure in C).  Processes form a 
monoidal category, and there is a perfectly good functor F : Set -> C, 
but it's not identity-on-objects, as the object structure of processes 
is much richer than the object structure of Set.

A.

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