haskell - Haskell 和类 Haskell 语言之间的类型声明语法差异

Question

在 Haskell 中，类型声明使用双冒号，即 (::)，如 not::Bool -> Bool。

但是在许多语法与 Haskell 类似的语言中，例如榆树、 Agda 、 他们使用单个冒号(:)来声明类型。就像不是:Bool -> Bool。

为什么这些语言放弃了 haskell 风格的类型声明语法。

• 声明类型时 (:) 比 (::) 更好吗？
• 或者 (::) 更适合其他用途？
• 或者只是因为 (:) 比 (::) 少一个字符？

Answer 1

IIRC Haskell 选择使用 ::是一个(不幸的)历史事故。 Haskell 很大程度上基于 Miranda，它也使用 ::对于类型¹。 Miranda 的作者确实希望 cons 运算符为 :因为他们认为它会使用得更普遍，所以打字操作符必须委托(delegate)给 :: .

这确实没有被证明是一个好主意，因为否则所有关于类型的文献(甚至是谈论 Haskell 的文献)都使用 : 。作为最近的paper at hand ，双冒号用于所有示例(Haskell)代码，但数学判断(如第 10 页)都遵循传统的单冒号。

<小时/>

¹ 我想我记得在某个地方听到过(编辑:是 here ，但我懒得听整件事以获得正确的时间)，当时，许多 FP 研究人员只是想非常清楚地定义 Miranda，以便讨论惰性函数纯语言的研究论文可以有一个共同的语言来讨论他们的想法。 Miranda 的设计者并不希望这样，而是说如果用另一种可能与 Miranda 非常相似的语言来完成就可以了(前提是，为了双方的利益，这两种语言仍然是可区分的) 。这是 Haskell 委员会的出发点。