[Agda] Re: Status of copatterns

[Andreas Abel]

Hi Francesco,

the current implementation just tries to reduce copatterns to record 
expressions /before/ type-checking, since Agda's core does not know 
about copatterns.  This, of course, causes all kinds of problems.

The plan is to add them to Agda's core, I have started on this but did 
not have time to complete it yet.  In particular, I have to change the 
reduction engine and such sort of stuff...

Cheers,
Andreas

On 28.01.13 2:06 AM, Francesco Mazzoli wrote:
> Hi list,
>
> After attending a talk by Andreas Abel on copatterns I have been trying them out
> today and in my opinion they improve considerably the usability of coinduction.
> I always felt the ‘manual’ coinduction that Agda currently provides is pretty
> clunky while copatterns feel much more ‘right’.
>
> However, there are a couple of problems in the current implementation which make
> copatterns not that usable:
>
> * Holes don’t work properly, see
>    <https://code.google.com/p/agda/issues/detail?id=742>
> * ‘where’ is unimplemented
>
> Now, some problems are to be expected in such an early stage, however a comment
> by Andreas on the mentioned bug caught my eye:
>
>     Probably can be fixed, but how much should I invest into this throw-away
>     code?
>
> Does this mean that the current implementation is going to be replaced by a
> better one, or does it mean that the future of copatterns is uncertain?  In the
> latter case, what are the roadblocks that make copatterns problematic?
>
> Thanks,
> Francesco
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/