[Agda] Agda goes coinductive

[Conor McBride]

Hi

On 5 Jun 2008, at 21:54, Dan Doel wrote:

> On Thursday 05 June 2008, Ulf Norell wrote:
>> One of the code sprints in the recent Agda meeting was to add  
>> coinductive
>> datatypes to Agda.
>
> Excellent! In celebration, here's everyone's favorite monad:  
> partiality (a mix
> of stuff from Abstract Nonsense for Functional Programmers and General
> Recursion via Coinductive Types).

Yes, this is splendid news! Well done! Wish I'd
been there, but I had drycleaning, ironing,
shaving, and punctuality obligations to
discharge...

And I was very pleased to see a Hancock classic
(with which, by the way, Coq has been known to
struggle) working out of the box. Of course, I'm
now hoping to understand the criteria for
accepting mutual definitions. There's plenty more
where that came from, so I'm confident the new
equipment will get lots thrown at it.

So now our troubles really begin...

[..]

> codata D (a : Set) : Set where
>   now   : a -> D a
>   later : D a -> D a
>
> never : {a : Set} -> D a
> never ~ later never

[..]

> codata _↑ {a : Set} : D a -> Set where
>   diverge : {dx : D a} -> dx ↑ -> later dx ↑
>
> -- problems here
> -- diverge-never : never ↑
> -- diverge-never ~ diverge diverge-never
> -- complaint: never != later never

Ulf's just remarked:

Ulf> This is the expected behaviour. When checking equality
Ulf> it's not safe to unfold corecursive functions.

[Later addition: what follows is an idea
which has tempted me for a while, but which
may, it turns out, have difficulties. Rather
than editing the text with hindsight, I thought
I'd just let you watch the crash...]

That's certainly the case for /evaluation/. As
some of you know, I suspect that one might try
a little bit harder in a type-directed equality
on normal forms. The intuition behind the
suggestion is that one should be able to tell
if two normal forms constitute "intensionally
the same computation in different stages of
evolution" by running the /initially/ less
involved one for finite time.

That's to say, when faced with deciding whether

   ne == cocon (cocon ... (ut)) : CoDataType

where neither ne nor ut is coconstructor-headed
(substitute whatever coalgebraic notion is
actually in place); note, there may be multiple
ut's.

repeatedly unfold ne until one of 4 things
inevitably happens

(1) ne fails to evolve a coconstructor
because of some inner neutral thing gumming
up the works, so say NO
(2) the coconstructors emerging from ne
conspicuously differ from those around ut,
in which case say NO
(3) ne evolves to the same pattern of
coconstructors, wrapped around some neutral
ne', in which case compare ne' with ut
as neutral values
(4) in some step, the coconstructors from
ne pass leapfrog those around ut, so that
the left-hand side is strictly more evolved
than the right, hence they cannot come
from the same mechanism, so say NO

Crucially, we decide up front which side to
evolve: we don't race the two. Moreover,
we're not trying to find a /simulation/,
just a more liberal /intensional/ match.
So if you define new constants

   fred ~ C fred
   jim ~ C jim

you get

   fred == C fred
   fred /= jim

(Of course, if you were to elaborate fred
and jim in terms of some universal unfold,
then they would become equal, but that's
under at least a few laters.)

Key questions:

(1) Does this loop?
   I don't think so. Productivity of ne
   guarantees that the tree of
   coconstructors evolved increases strictly,
   towards a bound given by the tree of
   coconstructors around the ut's. We
   continue either by saying no, or by
   comparing neutral terms.
(2) Is it a congruence? I'm not sure. It
   seems stable with respect to further
   evolution. I guess we also need to check
   that if ne and ne' evolve to the same
   coconstructory agglomeration, then ne
   and ne' coincide. That's a worry:
   what about

     fred ~ C fred
     jim  ~ C fred

   ? Maybe there's too much generativity
   around to get away with this approach.
   Maybe something more fundamental is
   wrong. Maybe we can recognize the
   distinction between evolving recursive
   fred and non-recursive jim.
(3) Is this too intensionally brittle to
   be helpful? My hope is that making ~
   imply == might save a lot of basic
   misery. But if generativity introduces
   too many unexpected distinctions, we
   might consider ourselves worse off.

Of course, if it's too brittle to be a
congruence, then it's no good, so we need
to record it as a mistake from which to
learn.

Perhaps it's hubristic to try to squeeze
a bit more out of the definitional equality
here. These are infinite objects, so
equational reasoning is inevitably going to
be evidence-based. A decent implementation
of coinduction is just what we need to bang
the last few nails into the coffin of
intensional propositional equality...

All the best

Conor
>