agda
What should our explicit import policy be?
As discussed in https://github.com/agda/agda-stdlib/pull/2334 we don't currently have a policy about when imports should use an explicit using statement and when it's fine to open the whole module. We should add something to the style guide.
I have no particularly strong feelings on the matter.....
We certainly should allow explicit imports, even if they are long, and not remove them once they've been put into place.
To me, there should be some 'core' of the library where explicit imports are required, and an 'upper layer' where they are merely encouraged.
I would argue in favour of mandatory explicit import lists if they mention, say, max half a dozen identifiers. Throwing these in as we touch modules should hopefully help us detect spurious dependencies (until we get better tooling to do it automatically).
I'd be happy with mandatory for <= 6. I'd be unhappy to have explicit imports deleted just because they're long.
I'd be happy with mandatory for <= 6. I'd be unhappy to have explicit imports deleted just because they're long.
NB some recent refactorings do indeed delete 'long' using directives, but usually only to localise them further by removing more names, or to distribute the names they do import over lower-level modules they import from... so I don't think there's unnecessary 'widening' of import interfaces going on here.
