[Agda] generative thunk?

[Conor McBride]

Hi Nisse, hi Thorsten, hi all,

On 30 Dec 2010, at 23:21, Nils Anders Danielsson wrote:

> On 2010-12-30 17:24, Thorsten Altenkirch wrote:
>> Not true. The new mechanism using \infty, \sharp and \fat was
>> initially implemented on top of the old one and hence these issues  
>> are
>> not related to the alleged coup.
>
> Thorsten is right, see the following message:
>
>  Changes to coinduction
>  http://article.gmane.org/gmane.comp.lang.agda/763/

Thanks for the pointer to that message, which I should probably have  
known
about. Perhaps the points it makes should be in the documentation for
coinduction.

But let me just check a point of history. You wrote

   The reason for the second change is that I got tired of writing  
things
   like

     map : ∀ {A B} → (A → B) → Stream A → Stream B
     map f (x ∷ xs) = f x ∷ map′
       where map′ ~ ♯ map f (♭ xs).

Was that sharp handled generatively? When you wrote

   Now you can write

     map : ∀ {A B} → (A → B) → Stream A → Stream B
     map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

   instead.

   There are some problems with this approach:

   * Two delayed applications of a coinductive constructor are not
     definitionally equal unless they come from the same location in
     the source code. This problem is a bit worse than when ~ was used,
     because now /every/ application is delayed.

you rather suggested that it was your *new* way of doing things which
introduced a *new* generativity problem. Is this the case? Thorsten,
I suspect you may be right, except in the bit where you say Andreas
is wrong, but perhaps comparing old with new sheds light on the
situation.

I suppose the semantics of map' ~ ... may have had a similar impact,
as the name map' is generative, and this lazy definition won't unfold
unless forced. I suppose also that top-level lazy definitions" with ~
were more sharable. But perhaps the old misery suggests a workaround.
If I want to point out a coincidence, should I be writing

mutual
   map : forall {S T} -> (S -> T) -> Stream S -> Stream T
   map f (s :: ss) = f s :: mapThunk f (force ss)
   mapThunk : forall {S T} -> (S -> T) -> Stream S -> Lazy (Stream T)
   mapThunk f ss = thunk (map f ss)

if I want to refer to thunked map calls in other places?

One problem, clearly, is that thunk comes in the guise of a term, when
it is rather a construct for delivering the seed of a coalgebra,
meaningless on its own. The type of my P thunk -> P thunk examples
should be rejected out of hand! But we should still want the identity
function to inhabit P (thunk x) -> P (thunk x).

Might one eliminate the generativity of thunk? 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.

Of course, what I'd really like to see is an elaboration scheme from the
programming language to some kind of coiterator. Identifying which
things are not really recursive calls but rather coinduction seeds:
that's got to play a part in any such elaboration.

But then, using types to characterise justifiable forms of recursive
definition is just so last century.

All the best

Conor