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

我一样知道，我声明平均数是要返回一个Double，但是我写的平均数的声明却没有返回一个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 不吃亏