隐式函数：currying 和 totality答案

【问题标题】：Implicit functions: currying and totality隐式函数：currying 和 totality
【发布时间】：2016-02-07 07:15:48
【问题描述】：

在 VDM-SL 中指定隐式函数时，是否可以指定柯里化函数？下面的 test1 和 test2 是显式的 uncurried 和 curried 函数，而 test3 是一个隐式的 uncurried 函数。 Overture 都接受了所有内容。 test4 是对隐式柯里化函数的尝试，但被 Overture 拒绝。

另外，有没有办法用隐式函数定义来指定它应该是全部的？

module moduleName
  exports all
  definitions
  functions

  test1 : nat * nat +> nat
  test1 (arg1,arg2) == arg1+arg2;

  test2 : nat -> nat +> nat
  test2 (arg1) (arg2) == arg1+arg2;

  test3 (arg1:nat,arg2:nat) res:nat
  post res = arg1+arg2;

  test4 (arg1:nat) (arg2:nat) res:nat
  post res = arg1+arg2;

end moduleName

【问题讨论】：

标签： vdm-sl

【解决方案1】：

不，我担心柯里化函数只是为显式函数定义提供的。并且没有隐式定义的部分/全部指标。

（我只是问为什么我们会有这种差异。似乎与语言的历史有关：英国学校产生了隐式函数但没有柯里化，而丹麦学校有显式函数有柯里化。他们真的应该被协调——你猜到的语法可能就是结果。）

【讨论】：