在Idris中，IO可以發生在任何宇宙中嗎？

Question

這是我的問題。 Idris有一個累積的宇宙層次，宇宙由編譯器推斷。使用dosomethingreal : IO是否意味着層次結構中最低的宇宙？是IO : Type，從來沒有IO : Type 1？或者我可以在任何宇宙中進行IO操作？

Answer 1

您可以。例如，類型Type -> Type位於比參數類型更高的Universe中。所以Type -> Type絕對不是最低的宇宙，也不是IO (Type -> Type)，但

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

運行正常。