功能及产品类型特点答案

【问题标题】：Function and Product Types Peculiarity功能及产品类型特点
【发布时间】：2017-06-23 06:53:42
【问题描述】：

类型有什么区别

(seq of nat * seq of nat) -> nat

和

seq of nat * seq of nat -> nat

根据语言参考手册* 的优先级高于->，因此括号无效；它们在语义上是相同的。但是考虑函数定义

length: (seq of nat * seq of nat) -> nat
length (mk_(l,m)) == len l + len m;

length0: seq of nat * seq of nat -> nat
length0 (l,m) == len l + len m;

每个都使用一种类型，并且定义中使用的模式必须不同才能通过类型检查。这两种类型之间似乎存在差异。这里发生了什么？通过括号，它将参数解释为产品，但没有括号有两个参数，但不知何故，函数的参数类型仍然是产品。这是相当混乱的。有人可以澄清一下吗？

【问题讨论】：

标签： vdm-sl

【解决方案1】：

是的，这令人困惑。实际上，括号在这里用于两个目的，并且在语法中没有明确说明。单独地，括号可以在类型声明中用于指示分组并克服默认优先级。正如您所期望的那样。但在函数定义中，顶层括号和星号也是用来标识不同的参数类型。

所以“nat * nat -> nat”试图表明这是一个有两个参数的函数，而不是这个函数接受一个产品类型的单个参数。那么，你如何表明你真的想要一个单一的产品参数呢？答案：带括号:-)

所以函数定义中最外层的括号和乘积运算符用于对参数类型进行分组，但更深的括号和星号具有通常的含义。当它说参数/返回类型是“函数类型”时，语法具有误导性 - 从语法上讲这是正确的，但是随后解释类型的方式是特殊的，以便提取函数的参数编号和类型。

【讨论】：

* 并且可能值得在语言参考手册中添加一些关于此的内容。
在我看来，发生这种情况的原因是因为 VDM 选择为产品值创建特殊语法，即“mk_(x,y)”。如果你考虑 Haskell，产品值就像“(x,y)”，所以当涉及到函数应用时，你只有“f(x,y)”，而 VDM 可以有“f(x,y)”或“f( mk_(x,y))"。因此，在 Haskell 中您不会遇到这种类型的混淆。
并在 Haskell 中传递一个元组作为一个参数？那会是 f((x,y)) 吗？在这种情况下，差异并不是那么大。
不，Haskell 不需要像 VDM 那样将函数参数包裹在括号中。 'f(x,y)' 可以，但 'f((x,y))' 也可以，并且相同。 '((x,y))' 只是用括号括起来的 '(x,y)'。也意味着在 Haskell 中你可以只做 'f p' is p is a pair such as '(1,2)'，而 VDM 需要 'f(p)'。