为什么没有明确类型的Idris片段类型检查？

Question

我刚刚开始学习Idris,我正在阅读" 使用Idris进行类型驱动开发 "一书.第二章的示例练习之一是编写一个函数,给定一个字符串,该函数确定该字符串中单词的平均长度.我的解决方案如下:

average : String -> Double
average phrase =
  let werds = words phrase
      numWords = length werds
      numChars = the Nat (sum (map length werds)) in
  cast numChars / cast numWords

但是,由于这numChars条线,我在解决这个问题时遇到了很多麻烦.出于某种原因,除非我明确使用类型,否则不会进行类型检查the Nat.错误说明:

Can't disambiguate since no name has a suitable type:
        Prelude.List.length, Prelude.Strings.length

这对我来说并没有多大意义,因为无论使用哪个定义length,返回类型都是Nat.这一点得到了以下事实的支持:在REPL中可以无错误地完成相同的操作序列.这是什么原因？

Answer 1

这确实很奇怪，因为如果你命名中间计算map length werds，那么 Idris 就能够推断出类型：

average : String -> Double
average phrase =
  let werds    = words phrase
      numWords = length werds
      swerds   = map length werds
      numChars = sum swerds in
  cast numChars / cast numWords

并且 REPL 还能够推断出sum . map length . words类型为String -> Nat。如果您在这里没有得到任何满意的答案，我建议您提交错误报告。