这是我的问题。 Idris 有一个累积的 Universe 层次结构，其中 Universe 由编译器推断。是否使用dosomethingreal : IO暗示层次结构中最低的宇宙？是 IO : Type从不IO : Type 1 ?或者我可以在任何 Universe 中进行 IO 操作吗？
最佳答案
你可以。例如，类型 Type -> Type位于比参数类型更高的宇宙中。所以Type -> Type绝对不在最低宇宙中，也不是IO (Type -> Type) ， 但
test : IO (Type -> Type)
test = return List
运行良好。
关于io - 在 Idris 中，IO 可以在任何宇宙中发生吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/37341154/