Geek Answers Handbook

In Idris, can IO happen in any universe?

This is my question. Idris has an aggregate hierarchy of universes where the junior is output by the compiler. Does use use the dosomethingreal : IOsmallest universe in the hierarchy? Is IO : Typeand never IO : Type 1? Or can I have IO actions in any universe?

+4
source share
1 answer

You can. For example, the type Type -> Typeis in a higher universe than the type of the argument. Thus, it is Type -> Typedefinitely not part of the lower universe, and is not IO (Type -> Type), but

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

works fine.

+4
source

More articles:


All Articles