在类 Haskell 语言中通过部分应用定义“多变量”函数

Question

所以。我实际上是在修改 Idris 语言，在某种程度上遵循 Brady 的Idris 类型驱动开发。我不认为我在这里写的是依赖于特定的编程语言（我不知道任何哈斯克尔，对于这个问题）。但我不知道我还能在哪里发布这个，因为我不了解部分应用/柯里化、类型、lambdas 以及从数学家的角度来看的所有东西。

一些上下文

在本书的第二章中，作者提请注意以下场景。

鉴于不言自明的片段

double : Num a => a -> a
double x = x + x

rotate : Shape -> Shape

其中Shape : Type和rotate分别是形状类型和将 a 旋转Shape90 度的函数的孔，aquadruple和turn-around函数后面有明显的模式

quadruple : Num a => a -> a
quadruple x = double (double x)

turn_around : Shape -> Shape
turn around x = rotate (rotate x)

这导致我们编写一个twice能够应用两次相同运算符的（高阶）函数。

在我看来，解决问题的方法主要有两种。第一个只是遵循 Brady 的代码

twice : (ty -> ty) -> ty -> ty
twice f x = f (f x)

在那里，他实际上定义图像twice f : ty -> ty中的twice在任意函数f¹。

第二个，在我看来更优雅一点，是twice通过一个composite函数和/或一个匿名函数来定义，通过稍微改变它的签名

twice : (ty -> ty) -> ty
twice f = composite f f

composite : (ty_2 -> ty_3) -> (ty_1 -> ty_2) -> (ty_1 -> ty_3)
composite g f = \x => g (f x)

两种方法都会导致最终结果

turn_around : Shape -> Shape
turn_around = twice rotate

问题

我会尽量让我的问题保持清晰，所以我不会滥用基本的 compsci 术语，而是让事情变得具体。

1. 假设我们有一个“多变量”函数

   f : ty_1 -> ty_2 -> ... -> ty_n
   

   然后f是一个函数带x_1 : ty_1另一个函数f x_1 : ty_1 -> ... -> ty_n。我们什么时候应该选择f通过写来定义

   f x_1 = stuff
   

   代替

   f x_1 ... x_{n-2} = stuff2
   

2. 有人可以向我澄清上面报告的两种方法（布雷迪和我的）之间的区别吗？

---

¹是的，我是一名数学学生...

Answer 1

没有硬性规定告诉人们何时应该使用一种风格而不是另一种风格。

定义为的函数

f x = \y => ...

完全等于定义为的函数

f x y = ...

当我们想强调我们喜欢将其f视为一个由函数组成的 codomain 的一元函数时，我们可能更喜欢第一种表示法。当我们希望将其f视为二元函数时，我们将改为使用第二种表示法。

对于您编写的函数组合

composite g f = \x => g (f x)

因为组合通常被认为是一个二元函数。我们也可以写

composite g f x = g (f x)

但这虽然较短，但并不那么清楚，因为它建议人类读者将其视为composite三元函数。作为人类，我也更喜欢第一种形式，但不会偏爱计算机。

如果我不能像你一样使用组合，我会把布雷迪的代码写成

twice f = \x => f (f x)

强调我们真的希望将其twice视为功能到功能的映射（endo-to-endo，要挑剔）。这两种形式是完全等价的。

最后，一个更数学的说明：从基础的角度来看，不需要符号

f x1 ... xn = stuff

我们通常用它来定义函数。非常迂腐，上面实际上并没有定义f，而只是定义了f应用于n参数时的行为方式。由于我们知道唯一标识f，因此我们不关心它。但是，如果我们这样做了，我们会f像定义其他任何东西一样定义，即使用以下形式的定义方程

f = something

尤其是

f = \x1 .. x2 => stuff

所以，形式f x1 .. xn = ...with 的每一个定义n>0都可以看作是语法糖：一种我们可以用来编程的符号，但是在学习与编程语言相关的理论时我们可以忽略它。具体来说，如果我需要用数学方法证明所有程序的属性P，我不必考虑P使用语法糖的情况，而只考虑每个方程都有形式的情况f = ...，可能涉及 lambdas。这简化了证明，因为我们需要处理的情况更少。

现在，我不太了解 Idris，所以我不知道在 Idris 中是否在所有情况下都可以转换为 lambdas。例如，在 Agda 中这是不可能的，因为依赖消除是如何执行的。在 Coq 中，这将是可能的。在您需要依赖类型之前，您应该没问题。