That's my question. Idris has a cumulative universe hierarchy where the universe is inferred by the compiler. Does the use of dosomethingreal : IO imply the lowest universe in the hierarchy? Is IO : Type and never IO : Type 1? Or can I have IO actions in any universe?
Asked
Active
Viewed 98 times
4
ruben.moor
- 1,876
- 15
- 27
1 Answers
4
You can. For example, the type Type -> Type is in a higher universe than the argument type. So Type -> Type is definitely not in the lowest universe and neither is IO (Type -> Type), but
test : IO (Type -> Type)
test = return List
runs fine.
xash
- 3,702
- 10
- 22