时间戳

首页 > 解决方案 > Agda 中匿名模块的用途

module - Agda 中匿名模块的用途

问题描述

进入 Agda 标准库的根目录，并发出以下命令：

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

产生以下结果：

843

每当我遇到这样的匿名模块（我假设这就是它们的名称）时，我完全不知道它们的目的是什么，尽管它们明显无处不在，也不知道如何使用它们，因为根据定义，我无法使用它们访问它们的内容他们的名字，虽然我认为这应该是可能的，否则他们将没有意义，甚至允许他们被定义。

维基页面：

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

有一个名为“匿名模块”的部分实际上是空的。

有人可以解释匿名模块的目的是什么吗？

如果可能的话，任何强调这些模块定义的相关性以及如何使用它们的内容的例子都将非常感激。

以下是我想出的可能的想法，但似乎没有一个是完全令人满意的：

  1. 它们是一种在 Agda 文件中重新组合主题相同的定义的方法。
  2. Agda 在使用它们提供的功能时以某种方式推断出它们的名称。
  3. 它们的内容仅在其 englobing 模块中可见/使用（有点像private块）。

标签： moduleagda

解决方案

匿名模块可用于简化共享某些参数的一组定义。例子：

open import Data.Empty
open import Data.Nat

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

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

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

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

  <⇒&gt;′ : m > n
  <⇒&gt;′ = {!!}

Afaik 这是匿名模块的唯一用途。当module _范围关闭时，您不能再引用该模块，但您可以引用它的定义，就好像它们根本没有在模块中定义一样（而是使用额外的参数）。

推荐阅读