如何在 Agda 的记录/数据类型中存储函数？答案

【问题标题】：How can I store a function inside record/data type in Agda?如何在 Agda 的记录/数据类型中存储函数？
【发布时间】：2017-11-16 08:15:02
【问题描述】：

我已阅读文档。它说：

严格的积极性条件排除了诸如
之类的声明
data Bad : Set where
    bad : (Bad → Bad) → Bad
    --     A     B      C
    -- A is in a negative position, B and C are OK
因为在构造函数的参数类型中有一个负面的 Bad 出现。（请注意，在 Haskell 和 ML 等标准函数式语言中，允许使用 Bad 的相应数据类型声明。）。

但它没有说明是否有另一种方法可以将函数存储在其他东西（如数据类型或记录类型）中。

我也试过这个，它也不能编译：

bin-op : ∀ {ℓ} (A : Set ℓ) → Set ℓ
bin-op A = A → A → A

record Storer {ℓ} (A : Set ℓ) : Set where
  field
    operator : bin-op A

那么如何将函数存储在数据类型/记录类型/我不知道的其他内容中？

【问题讨论】：

每当您收到错误消息时，请发布。如果您尝试record Storer {ℓ} (A : Set ℓ) : Set ℓ where 会怎样？严格的积极性条件仅适用于归纳事件，Storer 甚至不是归纳的。
Wtf，这行得通。您能否解释更多或提供我可以从中阅读答案的链接？我对如何在 Agda 中使用关键字 inductive 和 coinductive 知之甚少。谢谢！
Here 是一些关于宇宙多态性的文档。我想说的是，这里的问题不在于严格的积极性，而是Storer 被定义在比它实际所属的宇宙（Set ℓ）更低的宇宙（Set）中。
好的，明白了。谢谢！
为什么不回答这个问题并获得一些代表？

标签： function agda

【解决方案1】：

问题出在

record Storer {ℓ} (A : Set ℓ) : Set where

部分。在这里您声明Storer 属于Set Universe，但是Storer 包含bin-op A，它在Set ℓ Universe 中，并且记录不能小于其字段。因此，解决方法是将Storer 定义为Set ℓ：

record Storer {ℓ} (A : Set ℓ) : Set ℓ where

严格的积极性与问题完全无关。

Agda 中的Universe 多态性在旧的wiki 中有所描述。

【讨论】：