[Agda] generative thunk?

[Conor McBride]

Hi Nisse

On 31 Dec 2010, at 14:23, Nils Anders Danielsson wrote:

> On 2010-12-31 12:27, Conor McBride wrote:
>
>> Might one eliminate the generativity of thunk?
>
> Using something like ΠΣ's structural equality (preferably backed up  
> by
> some kind of meta-theory) should work. I tried to implement something
> like this, but the representation of substitutions used internally in
> Agda came in the way.

I look forward to seeing what that boils down to.

Ultimately, though, it's not metatheory that I want. I'd much prefer a
translation to a closed evidence-kernel with a corecursor, in which
all well typed terms are total, and which is extended only by making
definitions. I know, I know -- I want the moon on a stick.

>
>> What if the construct were
>>
>> thunk(f|a1,..an) -- perhaps not written that way, but conceptually  
>> thus
>>
>> where f is the name of a defined function, and
>>
>> thunk(f|a1,..an) : Lazy T just when f a1..an : T
>>
>> with
>>
>> force (thunk(f|a1,..an)) = f a1 .. an
>>
>> The generativity of thunk is eliminated, leaving the generativity of
>> recursive function names, of course. But at least if I write the same
>> thunk twice, they're identifiably the same.
>
> 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.

So it's just like

> At the moment, when you write
>
>  thunk e[x1...xn]
>
> you get the function
>
>  thunk-237 x1...xn ~ e[x1...xn]

only identified by the e (which must be an identifier), rather than the
237, and providing a notation which the programmer can openly duplicate,
rather than a magic number. I'd hope that at least the cure for  
generative
thunk need not require a radical reinvention of the definitional  
equality.
But perhaps I underestimate the problem.

Admittedly, one might also need an injection

   old : T -> Lazy T   with   force (old t) = t

which does not act as a guard, and gives lazy wrapping to values already
computed. (cf Anton and Hank's coding of more liberal coalgebras, which
allow either a seed for new codata or the placement of old codata). It  
is
not clear to me whether this conceptual distinction necessitates a
notational distinction or whether the elaboration is clear from context.

> (for some value of 237). Here thunk-237 is delayed, but in the
> application thunk-237 a1..an the individual arguments a1...an can  
> still
> be reduced.

That's also the case with the construct I propose. All expressions
compute: the thunk construct prevents the formation of the expression
which must be delayed, but its subexpressions are fair game. That's
actually my point: the meaningless or dangerous things -- thunk on its
own, the unforced recursive application -- should not be expressions
if you don't want them to be treated like expressions (computed,  
compared
for equality, etc).

> 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?
It should be ok to substitute free variables in the a1,..an.

> but as I
> mentioned above I found Agda's current representation of substitutions
> to be suboptimal for this task.

Now that I will believe. What's a good representation so often varies
catastrophically in response to small changes in desired functionality.

All the best

Conor