如何在Agda中定义含依赖模块参数的数据类型的参数化模块？

问题根源 #

你编写的Sig数据类型直接引用了模块参数ℓ和Sort，但这些参数要到SortedABT模块声明时才会被绑定，Agda无法识别未提前定义的标识符，导致代码无法运行。

解决方法 #

方法一：将Sig移至模块内部

把Sig的定义放到SortedABT模块内部，使其可以直接访问模块参数：

module SortedABT {ℓ} (Sort : Set ℓ) (Op : Sort → Set ℓ) where
  data Sig : Set ℓ where
    ■ : Sort → Sig
    ν : Sig → Sig

  -- 若需要依赖sig参数，可嵌套子模块
  module WithSig (sig : (s : Sort) → Op s → List Sig) where
    -- 此处编写ABT相关的后续定义

方法二：让Sig成为带参数的独立数据类型

将Sig定义为依赖ℓ和Sort的参数化数据类型，模块中通过传入实例来使用：

data Sig {ℓ} (Sort : Set ℓ) : Set ℓ where
  ■ : Sort → Sig Sort
  ν : Sig Sort → Sig Sort

module SortedABT {ℓ} (Sort : Set ℓ) (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List (Sig Sort)) where
  -- 此处编写ABT相关的后续定义

方法选择建议 #

• 若Sig仅在SortedABT模块内部使用，优先选方法一，避免全局命名空间污染。
• 若需要在多个模块间复用Sig类型，选择方法二，通过参数化实现类型复用。

内容的提问来源于stack exchange，提问作者Philip Wadler