参数化数据类型作为模块参数？

Question

在 Agda 中，如何定义与以下内容等效的参数化模块？

data Sig : Set ℓ where
  ■ : Sort → Sig
  ν : Sig → Sig

module SortedABT {ℓ} (Sort : Set ℓ) (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List Sig) where

当然上面不起作用，因为

ℓ

和

Sort

出现在

Sig

的定义中，但是是模块的参数，所以还没有定义它们出现的位置。我查看了 Agda 手册并尝试了各种网络搜索，但没有找到解决方法。请帮忙！

Answer 1

不确定您正在寻找哪种用户体验，但您可以尝试

module _ {ℓ} (Sort : Set ℓ) where

  data Sig : Set ℓ where
    ■ : Sort → Sig
    ν : Sig → Sig

  module SortedABT (Op : Sort → Set ℓ) (sig : (s : Sort) → Op s → List Sig) where

这增加了

Sig : ∀ {ℓ} (Sort : Set ℓ) → Set ℓ

当前范围以及预期

SortedABT

。

或者，您可能想给外部

module

起一个这样的名称：

module SigAndStuff {ℓ} (Sort : Set ℓ) where

因此始终需要在特定的

open

处显式地进行

Sort

编辑，例如

open SigAndStuff ⊤

添加了

Sig : Set

当前范围以及原始

SortedABT

实例化如下：

SortedABT {zero} {⊤}