[Agda] Re: Agda IO with session types

[Nils Anders Danielsson]

On 2010-10-25 21:35, Alan Jeffrey wrote:
> 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).

In case you want to experiment further: It is very easy to tweak the
compiler to make all inductive datatypes strict. One can then use ∞ as a
laziness annotation.

--
/NAD