Pourquoi la monade de tri Set1?

Question

J'ai essayé d'encoder la classe de caractères Monad dans Agda. Je suis arrivé jusqu'ici:

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 

Ainsi, une « instance » Monad est vraiment juste un enregistrement de fonctions qui est passé autour. Question: Pourquoi Monad du tri Set1? annotant avec Set donne l'erreur suivante:

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 

Quel processus de pensée dois-je traversais pour déterminer que Monad est Set1 plutôt que Set?

Answer 1

Agda a une hiérarchie infinie d'univers Set : Set1 : Set2 : ... pour empêcher les paradoxes (Russell's paradox, Hurkens' paradox). _->_ conserve cette hiérarchie: (Set -> Set) : Set1, (Set1 -> Set) : Set2, (Set -> Set2) : Set3, à savoir l'univers où A -> B mensonges dépend des univers où A et B mensonge: si A « s est plus grand que B » s, alors A -> B se trouve dans le même univers que A, sinon A -> B se trouve dans le même univers que B.

Vous quantifier plus Set (en {A : Set} et {A B : Set}), d'où les types de return et _⟫=_ se trouvent dans Set1, d'où la chose se trouve dans Set1. Avec des univers explicites le code ressemble à ceci:

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 

Plus sur le polymorphisme de l'univers dans Agda wiki.