[Agda] generative thunk?

[Conor McBride]

Hi Andreas

On 30 Dec 2010, at 09:22, Andreas Abel wrote:

> Hi Conor,
>
> you are hitting the repercussions of the 2008 Nottingham coup d'etat  
> on Agda coinduction.  What exactly is going on here I do not know  
> and do not approve, but, roughly:
>
> Every use of a SHARP is translated into a new definition (in your  
> case, thunk-6, thunk-7, and thunk-8), and they are considered  
> different. This is why zut fails.  fut succeeds because only on  
> instance of thunk is created, while the two others are meta- 
> variables which are instantiated with the correct instance of thunk.

That's what I suspected. The obvious expedient of defining one copy of  
thunk
and using it instead falls foul of the termination checker: if I'm  
lucky, it
just moans in the usual miserable way, forcing me to expand  
definitions I'd
rather keep tidy. I have an unlucky example which I'm trying to cut to  
the
minimum, but it locks my emacs every time.

> Nisse had plans to fix this by a structural equality test which  
> identifies more terms.  In my view, however, there is neither  
> sufficient theory nor consensus for the current approach to  
> coinduction in Agda and we need to go back to the drawing board.

Agreed. We need to think it through again. It's not enough to paper  
over the
cracks. I should, of course, point out that Anton has been thinking it  
through
for some time. I'm not at all sure about his notational proposal  
(though I'm
hardly in a position to criticise), but something sitting closer to  
the concept
of weakly final coalgebra would make a lot of sense to me.

I'm also looking at managing productivity with the "tomorrow  
idiom" (in fact,
my experimental models are the source of the troubling examples), but  
I'm some
way off a clear proposal.

> Could you file this as an issue on the bug tracker?

I have done so.

Cheers

Conor