如何解决为什么 Agda 拒绝 Set₁ → Set₁?
代码如下:
Continuation : Set → Set₁ → Set₁
Continuation R X = (X → R) → R
Selection : Set → Set₁ → Set₁
Selection R X = (X → R) → X
dagger : {R : Set} → Selection R → Continuation R
dagger S X k = k (S k)
出于其他原因,我需要继续和选择以使用更高的宇宙。但随后匕首的定义引发了一个错误:
(Set₁ → Set₁) 应该是一种排序,但在检查应用程序的推断类型时不是 集合₁ → 集合₁ 匹配预期类型_16
解决方法
在 Agda 中,_→_
是不属于任何范畴的函数空间,而是属于类型和
功能。我的猜测是您想要以下内容:
dagger : {R : Set} → ∀ X → Selection R X → Continuation R X
dagger X S k = k (S k)
即索引类型和索引保留函数的函数空间。
或者,您可以通过使用 stdlib 的
Relation.Unary
态射和写的概念:
open import Relation.Unary
dagger : {R : Set} → Selection R ⊆ Continuation R
dagger S k = k (S k)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。