Purpose of anonymous modules in Agda

Question

Going at the root of Agda standard library, and issuing the following command:

grep -r "module _" . | wc -l

Yields the following result:

Whenever I encounter such anonymous modules (I assume that's what they are called), I quite cannot figure out what their purpose is, despite of their apparent ubiquity, nor how to use them because, by definition, I can't access their content using their name, although I assume this should be possible, otherwise their would be no point in even allowing them to be defined.

The wiki page:

https://agda.readthedocs.io/en/v2.6.1/language/module-system.html#anonymous-modules

has a section called "anonymous modules" which is in fact empty.

Could somebody explain what the purpose of anonymous modules is ?

If possible, any example to emphasize the relevance of the definition of such modules, as well as how to use their content would be very much appreciated.

Here are the possible ideas I've come up with, but none of them seems completely satisfying:

They are a way to regroup thematically identical definitions inside an Agda file.
Their name is somehow infered by Agda when using the functions they provide.
Their content is only meant to be visible / used inside their englobing module (a bit like a private block).

user_2948250 · Answer

Anonymous modules can be used to simplify a group of definitions which share some arguments. Example:

open import Data.Empty
open import Data.Nat

<⇒¬≥ : ∀ {n m} → n < m → n ≥ m → ⊥
<⇒¬≥ = {!!}

<⇒> : ∀ {n m} → n < m → m > n
<⇒> = {!!}

module _ {n m} (p : n < m) where

  <⇒¬≥′ : n ≥ m → ⊥
  <⇒¬≥′ = {!!}

  <⇒>′ : m > n
  <⇒>′ = {!!}

Afaik this is the only use of anonymous modules. When the module _ scope is closed, you can't refer to the module anymore, but you can refer to its definitions as if they hadn't been defined in a module at all (but with extra arguments instead).

Purpose of anonymous modules in Agda

1 Answers