为什么 Monad 是 Set1？

Question

我一直在尝试在 Agda 中对 Monad 类型类进行编码。我已经走到这一步了：

module Monad where
  record Monad (M : Set → Set) : Set1 where
    field
      return : {A : Set} → A → M A
      _⟫=_ : {A B : Set} → M A → (A → M B) → M B

所以 Monad 'instance' 实际上只是传递的函数的记录。问题：为什么 Monad 排序为 Set1？ 用 Set 注释会出现以下错误：

The type of the constructor does not fit in the sort of the
datatype, since Set₁ is not less or equal than Set
when checking the definition of Monad

我应该经过什么样的思考过程才能确定 Monad 是 Set1 而不是 Set？

Answer 1

Agda 有一个无限层次的宇宙 Set : Set1 : Set2 : ... 来防止悖论 (Russell's paradox, Hurkens' paradox)。 _->_ 保留此层次结构：(Set -> Set) : Set1、(Set1 -> Set) : Set2、(Set -> Set2) : Set3，即 A -> B 所在的宇宙取决于 A 和 B谎言：如果A的大于B的，则A -> B与A位于同一个宇宙，否则A -> B位于与 B.

相同的宇宙

您正在量化 Set（在 {A : Set} 和 {A B : Set} 中），因此 return 和 _⟫=_ 的类型在 Set1，因此整个事情都在于 Set1。对于显式宇宙，代码如下所示：

TReturn : (Set → Set) → Set1
TReturn M = {A : Set} → A → M A

TBind : (Set → Set) → Set1
TBind M = {A B : Set} → M A → (A → M B) → M B

module Monad where
  record Monad (M : Set → Set) : Set1 where
    field
      return : TReturn M
      _⟫=_ : TBind M

Agda wiki 中有关 Universe 多态性的更多信息。

为什么 Monad 是 Set1？

Why is Monad of sort Set1?

functional-programming

monads

agda

dependent-type