Есть ли в idris специальный синтаксис c для чистого ключевого слова?

Question

Я работаю над функцией чтения списка для ввода пользователем, а затем создания из него дерева. Вот код

readList : IO (Maybe BSTree a)
readList = do x <- getLine
              if all isDigit (unpack input)
                  then do (_ ** xs) <- readList
                      pure ( listToTree (cast x)::xs )
                  else pure Nothing

Это определение типа listToTree

listToTree : Ord a => List a -> BSTree a

При проверке типов readList я получаю сообщение об ошибке «неожиданно чистый» в строке pure ( listToTree (cast x)::xs ). Это проблема с отступом? Почему здесь нет чистого ключевого слова?

Answer 1

Отступы очень важны при работе в Идрисе и подобных языках. Я бы порекомендовал прочитать код стандартной библиотеки, чтобы увидеть соглашения, используемые в отношении отступов.

Будет проанализировано следующее:

readList : IO (Maybe (BSTree a))
readList = do
  x <- getLine
  if all isDigit (unpack input)
  then do
    (_ ** xs) <- readList
    pure (listToTree (cast x) :: xs)
  else
    pure Nothing