为什么Monad是Set1？
为什么Monad是Set1？
提问于 2016-06-01 00:15:27
我一直在努力对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**?**的 of sort 用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
Stack Overflow用户
回答已采纳
发布于 2016-06-01 01:59:57
Agda有一个无限层次的宇宙Set : Set1 : Set2 : ...来防止悖论(罗素悖论，赫肯斯悖论)。_->_保留了这样的层次结构：(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维基中宇宙多态性的信息。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/37557568
复制相关文章
相似问题
腾讯云开发者
