爲什麼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的「實例」實際上只是一個函數的記錄傳遞。問題：爲什麼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。使用明確的Universe代碼如下所示：

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。