[Agda] Status of copatterns
f at mazzo.li
Mon Jan 28 02:06:21 CET 2013
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