Warum ist Monad der Sorte Set1?

Question

Ich habe versucht, die Monad-Klasse in Agda zu kodieren. Ich habe so weit gekommen:

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 

So eine Monade ‚instance‘ ist wirklich nur ein Datensatz von Funktionen, die herumgereicht wird. Frage: Warum ist Monad der Sorte Set1? es mit Set Einfügen von Anmerkungen gibt die folgenden Fehler:

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 

Was Prozess gedacht soll ich durch bestimmen gehen zu, dass MonadSet1 ist eher als Set?

Answer 1

Agda hat eine unendliche Hierarchie von Universen Set : Set1 : Set2 : ..., um Paradoxen zu verhindern (Russell's paradox, Hurkens' paradox). _->_ bewahrt diese Hierarchie: (Set -> Set) : Set1, (Set1 -> Set) : Set2, (Set -> Set2) : Set3, dh das Universum, in dem A -> B liegt auf den Universen abhängt, in dem A und B liegen: Wenn A ‚s ist größer als B‘ s, dann A -> B als A im gleichen Universum liegt, sonst A -> B liegt im selben Universum wie B.

Sie Quantifizierung über Set (in {A : Set} und {A B : Set}), damit die Arten von return und _⟫=_ liegen in Set1, damit das Ganze liegt in Set1. Mit expliziten Universen sieht der Code wie folgt aus:

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 

Mehr über Universum Polymorphismus in Agda wiki.