[Agda] Codata oddity

[Conor McBride]

Hi

This is weird and wonderful. Well done, Nicolas!

Let's think backwards...

On 6 Jun 2008, at 14:16, Nils Anders Danielsson wrote:

> Hi,
>
> The current implementation of codata seems to be a bit problematic.
> The following program was suggested by Nicolas Oury:
>
>   data _≡_ {a : Set} (x : a) : a -> Set where
>     refl : x ≡ x

That's good old intensional equality, so...

>   codata Stream : Set where
>     cons : Stream -> Stream
>
>   ω : Stream
>   ω ~ cons ω
>
>   p : ω ≡ cons ω

...that had better not hold, right? The two
sides are closed terms and intensionally distinct,
so refl ain't a proof of their equality, so no
such proof exists. Now we gotta find where the
liberty gets taken...

>   out : Stream -> Stream
>   out (cons xs) = cons xs

Should the above hold definitionally? Why should
the left-hand side compute at all, unless some
case analysis demands it? Correspondingly...

>   out-≡ : (xs : Stream) -> xs ≡ out xs
>   out-≡ (cons xs) = refl

...should that typecheck?

There's clearly a craft to being consistently
lazy which demands devotion and anxiety.

Looks like it ain't as simple as "case causes
computation", if what's to be computed is not
in demand. A reduction-rule-computing-anywhere
presentation doesn't work.

I was just about to ask what happens in Coq,
when I got Nicolas's message on Coq club.

Cat, meet pigeons...

We live in interesting times.

All the best

Conor