Idris中(\x=>2.0*x) `map` [1..10]报错Enum Double未实现的原因咨询

首先咱们先明确错误本身，你输入的代码触发的错误是：

Idris> (\x=>2.0*x) map [1..10]
检查函数Prelude.Functor.map的应用时：找不到Enum Double的实现。

错误原因拆解 #

你预期的是map把List Int转成List Double，这个思路本身没问题——map确实支持输入输出列表的类型不同。但问题出在Idris的类型推断顺序和枚举语法[a..b]的依赖规则上：

1. 你的lambda表达式(\x=>2.0*x)里，2.0是Double类型，所以Idris会自动推断参数x的类型也是Double。
2. 既然map的函数参数接受Double，Idris就会推断map的输入列表应该是List Double，而不是默认的List Int。
3. 但[1..10]这种枚举语法需要依赖Enum类型类的实现才能生成列表，Idris默认给Int提供了Enum实例，但没有给Double内置Enum实例——毕竟浮点数的“枚举”行为（比如从1.0到10.0每次加1.0）不是通用且无歧义的，所以Idris不会默认支持。

简单说：Idris不是先把[1..10]当成List Int再转成Double，而是先根据lambda的类型要求，试图把[1..10]解析成List Double，但这需要Enum Double，而它不存在，所以报错。

解决办法 #

有几种简单的方式可以修复这个问题：

• 显式指定输入列表的类型：告诉Idris[1..10]是List Int，这样map就会把每个Int传给lambda，而lambda会自动把Int转成Double运算：

  (\x=>2.0*x) `map` ([1..10] : List Int)
  

• 显式转换lambda的参数类型：让lambda接受Int，手动把它转成Double：

  (\x=>2.0 * cast x) `map` [1..10]
  

• 显式指定结果列表的类型：引导Idris调整推断方向，先把[1..10]当成List Int，再生成List Double：

  (\x=>2.0*x) `map` [1..10] : List Double
  

内容的提问来源于stack exchange，提问作者corazza