问在伊德里斯，任何宇宙都会发生IO吗？
EN

Stack Overflow用户

提问于 2016-05-20 07:59:48

回答 1查看 94关注 0票数 4

这是我的问题。Idris有一个累积的宇宙层次结构，其中宇宙是由编译器推断的。dosomethingreal : IO的使用是否意味着层次结构中最低的宇宙？是IO : Type而不是IO : Type 1吗？或者我可以在任何宇宙中进行IO操作吗？

回答已采纳

发布于 2016-05-28 10:30:37

你可以的。例如，类型Type -> Type在比参数类型更高的范围内。所以Type -> Type绝对不是在最低的宇宙中，IO (Type -> Type)也不是，但是

test : IO (Type -> Type)
test = return List

跑得很好。

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/37341154

复制

相似问题

问在伊德里斯，任何宇宙都会发生IO吗？EN