[Agda] Re: Agda IO with session types

[Alan Jeffrey]

On 10/26/2010 07:13 AM, Nils Anders Danielsson wrote:
> On 2010-10-25 21:35, Alan Jeffrey wrote:
> 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.

The hack I adopted was using a datatype:

   data Strict (A : Set) : Set where
     ! : A -> Strict A

with a COMPILED_DATA binding to bind ! to a strict constructor.  Usable, 
for example:

   sum' : (Strict Natural) -> (List Natural) -> Natural
   sum' (! m) [] = m
   sum' (! m) (n :: ns) = sum' (! (m + n)) ns

   sum : (List Natural) -> Natural
   sum = sum' (! (# 0))

Yay, control over evaluation order!

The problem with using ∞ as the laziness tag is that it conflates 
call-by-need evaluation order with being coinductive: there are times 
I'd like cbn over inductive structures.

> --
> /NAD

A.