为什么这个 Idris 片段在没有显式类型的情况下不进行类型检查？答案

【问题标题】：Why doesn't this Idris snippet typecheck without an explicit type?为什么这个 Idris 片段在没有显式类型的情况下不进行类型检查？
【发布时间】：2017-07-14 02:59:15
【问题描述】：

我刚刚开始学习 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 中可以无错误地完成相同的操作序列。这是什么原因？

【问题讨论】：

标签： functional-programming type-conversion type-inference idris

【解决方案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。如果您在这里没有得到满意的答复，我建议您提交a bug report。

【讨论】：

【解决方案2】：

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

【讨论】：