copatterns or records? about agda-categories HOT 4 CLOSED

I don't have a preference. I think there are two reasons to use records:

1. the stdlib mainly uses records;
2. Emacs C-c C-r works quite well for record directly.

but neither is that important. we can try both if copatterns have advantages. but due to agda/agda@ace8e0d, will performance still be a part of consideration?

from agda-categories.

Maybe I alerted you to this question without need, since I was not aware of agda/agda@ace8e0d . If the rhs of a function clause is a record expression (using actual record syntax), then this clause is internally translated to copattern matching.
I think this heuristics was introduced to bring out the benefits of copatterns without forcing users to rewrite large code bases. Thus, you should be fine if you use record syntax.

Orthogonal to this is of course the stylistic policy of the library.

from agda-categories.

This subtlety is good to know -- especially the part where this doesn't happen when using a record constructor. I tend to like record constructors... but I guess going through a function-as-constructor works.

from agda-categories.

Right, part of this issue is indeed moot.

Stylistically, I strongly prefer records as the principal way of defining things (i.e. the explicit 'field' keyword and the way things look for record definitions).

For instantiating records, I have not settled on a style. I would not be against using a mixed style in agda-categories.

I consider this to be a sufficient policy 'decision' for now, and so this issue can be closed.

from agda-categories.