[Agda] Status of copatterns

Francesco Mazzoli f at mazzo.li
Mon Jan 28 02:06:21 CET 2013

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
* ‘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

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?


More information about the Agda mailing list