Назначение анонимных модулей в Agda

Question

Переход к root стандартной библиотеки Agda и выполнение следующей команды:

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

Дает следующий результат:

843

Когда я сталкиваюсь с такими анонимными модулями ( Я предполагаю, что они так называются), я совершенно не могу понять, какова их цель, несмотря на их очевидную повсеместность, ни как их использовать, потому что по определению я не могу получить доступ к их контенту, используя их имя, хотя я предполагаю должно быть возможно, иначе не было бы смысла даже разрешать их определение.

Страница вики:

https://agda.readthedocs.io/en/v2.6.1/language/module-system.html#anonymous -модули

есть раздел под названием «анонимные модули», который на самом деле пуст.

Может ли кто-нибудь объяснить, какова цель анонимных модулей?

Если возможно, любой пример Подчеркнуть актуальность определения таких модулей, а также то, как использовать их содержимое, будет очень признательно.

Вот возможные идеи, которые я придумал, но ни одна из них не кажется полностью удовлетворительной:

1. Это способ перегруппировать тематически идентичные определения внутри файла Agda.
2. Их имя каким-то образом передается Agda при использовании функций, которые они предоставляют.
3. Их содержимое предназначено только для того, чтобы быть видимым / использоваться внутри их модуля расширения (немного похоже на блок private).

Answer 1

Анонимные модули могут использоваться для упрощения группы определений, которые разделяют некоторые аргументы. Пример:

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, это единственное использование анонимных модулей. Когда область module _ закрыта, вы больше не можете ссылаться на модуль, но вы можете ссылаться на его определения, как если бы они вообще не были определены в модуле (но вместо этого с дополнительными аргументами).