我希望这个问题适合这个网站，与 Haskell 相比，这只是关于 Idris 中具体语法的选择，因为两者非常相似。我想这不是那么重要，但我很好奇。对于 Haskell 使用 -> 的某些情况，Idris 使用 =>。到目前为止，我已经看到 Idris 仅在函数类型中使用 ->，而在 lambdas 和 case _ of 等其他事物中使用 =>。这种选择是否来自意识到在这些用例之间有明确的句法区别在实践中是有用的？这只是一个随意的外观选择，我想多了？
【问题讨论】：
嗯，在 Haskell 中，类型签名和值位于不同的命名空间中，因此在一个中定义的内容不会与另一个中的内容发生冲突。在 Idris 中，类型和值占用相同的命名空间，这就是为什么您看不到例如data Foo = Foo 就像在 Haskell 中一样，而是 data Foo = MkFoo - 类型称为 Foo，构造函数称为 MkFoo，因为已经有一个值（类型 Foo），绑定到名称Foo，例如data Pair = MkPairhttp://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples
因此，最好的情况是它没有尝试使用用于构造函数类型的箭头，而使用用于 lambdas 的箭头 - 这些是完全不同的东西。您可以将它们与例如the (Int -> Int) (\x => x).
【讨论】：
我认为这是因为他们对 -> 符号的解释不同。
来自Wikipedia：
A => B表示如果A为真，那么B也为真；如果A为假，则不会提及B
这似乎适合 case 表达式，并且
->可能与=>含义相同，也可能与下面给出的函数含义相同
这是
f: X -> Y表示函数f将集合X映射到集合Y
所以我的猜测是，Idris 只是使用 -> 来表示狭义的第二种含义，即在类型签名中将一种类型映射到另一种类型，而 Haskell 使用更广泛的解释，它与 => 的含义相同。
【讨论】：