[Agda] generative thunk?

[Nils Anders Danielsson]

On 2010-12-31 17:04, Conor McBride wrote:
> On 31 Dec 2010, at 14:23, Nils Anders Danielsson wrote:
>> What is delayed here?
>
> Only the formation (and hence possible computation) of the application.
> The subexpressions of thunk(f|a1,..an) are the arguments a1,..an.

OK. Currently an expression like

   x = c (thunk (c' x))

is well-formed, but with your suggested construction it wouldn't be.
With this construction you need to be careful to delay the "leaves" in a
corecursive expression. I'm interested in mixed induction/coinduction,
so this doesn't sound very appealing to me.

>> With your construct you need to be careful not to substitute
>> under thunk (to avoid problems with subject reduction),
>
> I'm not sure I see how these problems arise. Can you give an example?

Given that the subexpressions are not delayed I don't think there would
be a problem.

-- 
/NAD