[Agda] no quick cofix

[Conor McBride]

Hi

Just to conclude my investigation into extending
the definitional equality to make coinductive
defining "equations" hold. Sorry Andreas, but
the news seems bad to me.

I wrote a little typechecker (300ish lines of
Haskell; email me if you'd like to see it) with
Pi, Sigma, One, Nat, and Stream. Streams are only
introduced by cons or by unfold, where

  S : Set   e : S -> X * S   s : S
----------------------------------
  unfold S e s : Stream X

Dependent case analysis turns unfolds into conses
on demand, as you'd expect. And I was hoping to
have the usual type-directed equality, with the
extra rule

  h = fst (e s) : X   t = unfold S e (snd (e s)) : Stream X
-----------------------------------------------------------
  cons h t = unfold S e s : Stream X

and its symmetric image. There are no races, and
there aren't any crummy counterexamples to transitivity
made by corecursive definitions which don't do anything.
Nicolas's nice example goes through ok. But it's
still not transitive.

   unfold Nat (\s -> (0, 0)) 1

     /=

   unfold Nat (\s -> (0, 0)) 0

but both equal

   cons 0 (unfold Nat (\s -> (0, 0)) 0)

We're not going to get out of this one. Take
S to code configurations of Turing machines
and e = \s -> (0, next s), where next evolves
the machine one step, resulting in a specific
configuration HALT (discarding the description
of the halting state), if the machine halts.
The rules plus transitivity say that

   unfold S e start = unfold S e HALT

if the machine halts. Oops.

There's another system I'm looking at, where
paradoxically, computation on codata is even
lazier (and Nicolas's example doesn't
typecheck). I haven't tripped it up yet, but
I expect it's more intensional than anyone
could put up with in practice.

So observational propositional equality is
looking to me like the best candidate for
having dependent case analysis directly on
codata. But I'm biased.

All the best

Conor