[Agda] Re: Agda IO with session types

[Alan Jeffrey]

I added the low-level IO bindings for the transducer library, and did 
some simple benchmarking.  A word-counting example is:

 
http://github.com/agda/agda-system-io/blob/master/src/System/IO/Examples/WC.agda

This is the same benchmark as over in iterateeland:

   http://okmij.org/ftp/Haskell/Iteratee/Lazy-vs-correct.txt

Comparing the Agda version with Linux wc gives:

   $ cat /usr/share/dict/words | time ./WC
   931709 98568
   1.27user 0.02system 0:01.32elapsed 97%CPU

   $ cat /usr/share/dict/words | time wc
     98569   98568  931708
   0.12user 0.01system 0:00.13elapsed 98%CPU

That is a 10x slowdown compared to the native wc, which sits between the 
Haskell iteratee peformance (6x slowdown) and Haskell lazy IO
performance (12x slowdown).

Memory-wise it fits into a 75K heap, and gives the garbage collector a 
good workout:

      594,329,832 bytes allocated in the heap
       24,730,488 bytes copied during GC
           20,968 bytes maximum residency (1 sample(s))
           26,064 bytes maximum slop
                1 MB total memory in use (0 MB lost due to fragmentation)

Not bad, considering there's almost no optimization in it (apart from a 
fair bit of hackery to ensure strictness / laziness in just the right 
places).

A.

On 10/18/2010 05:44 PM, Jeffrey, Alan S A (Alan) 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.