Idris 函数出现类型不匹配错误

Question

我是 Idris 的新手。我正在研究以下功能

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

我知道我已将平均值声明为 return 双精度，但我为平均值编写的声明并未 return 双精度。这就是我难过的地方。我希望 cast 能够完成这项工作。

Answer 1

你的缩进不对。在docs，他们说

When writing Idris programs both the order in which definitions are given and indentation are significant ... New declarations must begin at the same level of indentation as the preceding declaration. Alternatively, a semicolon ; can be used to terminate declarations.

试试这个...

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

我想在你那里它正在解析 wordCount str 之后 average 中的所有内容作为 wordCount str 的参数，这会导致类型错误，因为 Nat 不接受参数

Idris 函数出现类型不匹配错误

Idris function getting a type mismatch error

functional-programming

idris