Функция Идриса получает ошибку несоответствия типа

Question

Я новичок в Идрисе. Я работаю над следующей функцией

average :  String -> Double
average str 
    = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords

where
    wordCount : String -> Nat
    wordCount str = length (words str)

    allLengths : List String -> List Nat
    allLengths strs = map length strs

Я продолжаю получать следующую ошибку

Type checking ./average.idr
average.idr:5:47:
  |
5 |                   totalLength = sum (allLengths (words str)) in
  |                                   ^
When checking right hand side of average with expected type
        Double

When checking argument x to type constructor =:
        Type mismatch between
                Nat (Type of Main.average, wordCount str _)
        and
                _ -> _ (Is Main.average, wordCount str _ applied to too many arguments?)

Holes: Main.average

Я знаю столько, что я объявил среднее значение для возврата Double, но объявление у меня есть написано для среднего, не возвращает двойной. Вот где я в тупике. Я ожидал, что cast сделает эту работу.

Answer 1

Ваш отступ отключен. В документах говорится:

При написании программ Idris важны как порядок, в котором даются определения, так и отступы ... Новые объявления должны начинаться с того же уровня отступа. как предыдущее объявление. В качестве альтернативы можно использовать точку с запятой ; для завершения объявлений.

Попробуйте это ...

average :  String -> Double
average str 
    = let numWords = wordCount str
          totalLength = sum (allLengths (words str)) in
          cast totalLength / cast numWords

Я думаю, в вашем он разбирает все в average после wordCount str в качестве аргументов wordCount str, что приводит к ошибке типа cos Nat не принимает аргументы