1

类型之间有什么区别

(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;

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

4

1 回答 1

0

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

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

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

于 2017-06-24T10:38:09.720 回答