search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

What should our explicit import policy be? #2339

Open MatthewDaggitt opened 6 months ago

MatthewDaggitt commented 6 months ago

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.....

JacquesCarette commented 6 months ago

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.

gallais commented 6 months ago

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).

JacquesCarette commented 6 months ago

I'd be happy with mandatory for <= 6. I'd be unhappy to have explicit imports deleted just because they're long.

jamesmckinna commented 5 months ago

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.