算术运算的 Idris 类型推导答案

【问题标题】：Idris type deriving for an arithmetic operation算术运算的 Idris 类型推导
【发布时间】：2018-01-21 08:13:11
【问题描述】：

在下面的代码中

Idris> :t \x => x + x
\x => x + x : Integer -> Integer

Idris 为 x 变量派生一个 Integer 类型，我认为它应该派生一个接口限制，就像在 Haskell 中一样：

Haskell> :t (\x y -> x + y)
(\x y -> x + y) :: Num a => a -> a -> a

那么它甚至不像 Integer 那样接受 Double 类型：

Idris> (\x => x + x) 2.0 
4.0 : Double

谁能给我解释一下？

【问题讨论】：

Idris 的类型推断不如 Haskell 成熟。对于依赖类型，您的类型推断不会那么好。这里可能会发生类似于单态限制的事情。要找到对此行为的更好解释，您可能应该在 idris-dev 存储库中打开错误：github.com/idris-lang/Idris-dev/issues
@Shersh 依赖类型对非依赖程序的类型推断没有任何限制。此外，这种情况涉及的是泛化而不是推理，并且 Idris 没有通过设计进行泛化，不是因为任何根本原因。
@András Kovács 你能指导我看一些关于这个“Idris 没有设计概括”主题的内容吗？

【解决方案1】：

我认为总的来说，可以说在 idris 的 REPL 中检查类型推断是一个坏主意。 REPL 代码和 Idris 文件中存在的代码行为不同。

你想要的函数可以写成：

addy: Num a => a -> a -> a
addy x y = x + y

并且会有一种与您期望从 Haskell 获得的类型相似的类型。 Idris 中的类型推断通常非常弱（因为它无法确定依赖类型的类型系统）。

【讨论】：