Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

additions to style-guide #2270

Merged
merged 2 commits into from
Feb 5, 2024
Merged

additions to style-guide #2270

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4a4f72a
added stub content on programming idioms
jamesmckinna Jan 31, 2024
661aef0
added para on qualified import names
jamesmckinna Feb 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 37 additions & 2 deletions doc/style-guide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,15 +121,31 @@ automate most of this.

* If it is important that certain names only come into scope later in
the file then the module should still be imported at the top of the
file but it can be given a shorter name using the keyword `as` and then
opened later on in the file when needed, e.g.
file but it can be imported *qualified*, i.e. given a shorter name
using the keyword `as` and then opened later on in the file when needed,
e.g.
```agda
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
...
...
open SetoidEquality S
```

* Naming conventions for qualified `import`s: if importing a module under
a root of the form `Data.X` (e.g. the `Base` module for basic operations,
or `Properties` for lemmas about them etc.) then conventionally, the
qualified name(s) for the import(s) should (all) share as qualfied name
that of the name of the `X` datatype defined: i.e. `Data.Nat.Base`
should be imported as `ℕ`, `Data.List.Properties` as `List`, etc.
In this spirit, the convention applies also to (the datatype defined by)
`Relation.Binary.PropositionalEquality.*` which should be imported qualified
with the name `≡`.
Other modules should be given a 'suitable' qualified name based on its 'long'
path-derived name (such as `SetoidEquality` in the example above); commonly
occcurring examples such as `Algebra.Structures` should be imported qualified
as `Structures` etc.
NB. Historical legacy means that these conventions have not always been observed!

* When using only a few items (i.e. < 5) from a module, it is a good practice to
enumerate the items that will be used by declaring the import statement
with the directive `using`. This makes the dependencies clearer, e.g.
Expand Down Expand Up @@ -532,3 +548,22 @@ word within a compound word is capitalized except for the first word.

* The names of patterns for reflected syntax are also *appended* with an
additional backtick.

#### Specific pragmatics/idiomatic patterns

## Use of `with` notation

Thinking on this has changed since the early days of the library, with
a desire to avoid 'unnecessary' uses of `with`: see Issues
[#1937](https://github.com/agda/agda-stdlib/issues/1937) and
[#2123](https://github.com/agda/agda-stdlib/issues/2123).

## Proving instances of `Decidable` for sets, predicates, relations, ...

Issue [#803](https://github.com/agda/agda-stdlib/issues/803)
articulates a programming pattern for writing proofs of decidability,
used successfully in PR
[#799](https://github.com/agda/agda-stdlib/pull/799) and made
systematic for `Nary` relations in PR
[#811](https://github.com/agda/agda-stdlib/pull/811)

Loading