Чтение из файла в Идрисе

Question

каков предпочтительный идиоматический c способ чтения файлов в Idris? Например, я пытаюсь прочитать числа из файловой карты в значения Int и суммировать все. Входной файл

5 3 4 6 12

import Data.String

myCast: Maybe Integer -> Integer
myCast Nothing = 0
myCast (Just val) = val


sumNums: String -> Integer
sumNums s = sum (map myCast (map parseInteger (words s)))

, и меня больше всего интересует читающая часть

main : IO ()
main = do
  (Right content) <- readFile "input.txt" | (Left err) => printLn err
  printLn (sumNums content)

Как правильно обращаться с Either / Maybe здесь?

Answer 1

С книга и документы

main : IO ()
main = do file <- readFile "input.txt"
          case file of
               Right content => printLn (sumNums content)
               Left err => printLn err

<- позволяет нам действовать непосредственно на Either IO (Either FileError String). Затем мы делим регистр на возможные значения, печатая их в каждом случае