为什么这个 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型 。如果您在这里没有得到任何满意的答案，我建议您提交错误报告。

Answer 2

这是一个实现错误。伊德里斯是用哈斯克尔写的，而不是用伊德里斯本身写的。由于Haskell没有依赖类型，因此更有可能出现错误。也许，有一天，伊德里斯会被改写。