В Идрисе, может ли IO случиться в любой вселенной?

Question

Это мой вопрос. Идрис имеет совокупную иерархию юниверсов, где юниор выводится компилятором. Использует ли dosomethingreal : IO наименьшую вселенную в иерархии? Есть IO : Type и никогда IO : Type 1? Или я могу иметь действия IO в любой вселенной?

Answer 1

Вы можете. Например, тип Type -> Type находится в более высокой вселенной, чем тип аргумента. Так Type -> Type, безусловно, не в самой нижней вселенной, и ни один не IO (Type -> Type), но

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

работает отлично.