伊德里斯类型导出用于算术运算

在下面的代码伊德里斯类型导出用于算术运算

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

伊德里斯导出一个整数类型的X变量，其中我认为它应该得到像在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

Can有人向我解释这一点？

来源

2017-08-13 Ivan Kleshnin

“Idris”的类型推理并没有Haskell那么成熟。对于依赖类型，类型推断不会那么好。这里可能会出现类似于单态限制的情况。为了更好地解释这种行为，你应该在'idris-dev'仓库中打开bug：https://github.com/idris-lang/Idris-dev/issues – Shersh

@Shersh依赖类型不需要对类型推断进行任何限制为非依赖程序。另外，这个案例涉及泛化而不是推论，而且伊德里斯没有通过设计进行概括，也不是因为任何根本原因。 –

@AndrásKovács您能指引我谈谈关于这个“Idris没有设计概括性”主题的内容吗？ –

我认为在一般情况下，可以说在idris的REPL中检查类型推断是一个坏主意。存在于Idris文件中的REPL代码和代码行为有所不同。

你想要的功能将被写成：

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

和将有一个类型类同您从Haskell的期望之一。 Idris中的类型推断通常非常弱（因为它不能用于依赖型类型系统）。

来源

2017-08-14 09:24:46 Markus

伊德里斯类型导出用于算术运算

回答

相关问题