[Agda] generative thunk?

[Nils Anders Danielsson]

On 2010-12-31 12:27, Conor McBride wrote:
> 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?

No, but map′ was (and still is).

> When you wrote [...] you rather suggested that it was your *new* way
> of doing things which introduced a *new* generativity problem. Is this
> the case?

I made the problem worse, because after my change there was an implicit
tilde, with an accompanying fresh name, in front of every coinductive
constructor.

> 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?

That ought to work. I usually try to structure my code so that it only
refers to forced computations, but I have also encountered problems
caused by generativity.

> 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.

> 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? At the moment, when you write

   thunk e[x1...xn]

you get the function

   thunk-237 x1...xn ~ e[x1...xn]

(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. With your construct you need to be careful not to substitute
under thunk (to avoid problems with subject reduction), but as I
mentioned above I found Agda's current representation of substitutions
to be suboptimal for this task.

-- 
/NAD