haskell - 关于在类 Haskell 语言中通过部分应用定义 "multivariable"函数

Question

所以。实际上，我正在修改 Idris 语言，在某种程度上遵循 Brady 的 Idris 类型驱动开发。我不认为我在这里写的内容与特定的编程语言相关(而且我不知道任何 Haskell，就此而言)。但是我不知道我还能在哪里发布这个，因为从数学家的角度来看，我不知道部分应用程序/柯里化(Currying)、类型、lambdas 和所有这些东西。

一些上下文

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

Given the self-explaining snippet

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

rotate : Shape -> Shape

where Shape : Type and rotate are holes for the type of a shape and for a function that rotates a Shape by 90 degrees respectively, there is an obvious pattern behind a quadruple and a turn-around function

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

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

which lead us to write a twice (high-order) function capable of applying two times the same operator.

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

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

他实际定义图像的位置 twice f : ty -> ty的 twice在任意 f 上的函数1.

第二个，在我看来更优雅一点，是定义 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 术语，而是让事情变得具体。

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

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

有人可以澄清我上面报道的两种方法(布雷迪和我的)之间的区别吗？

1是的，我是数学系的学生...

Answer 1

没有硬性的“规则”告诉一个人何时应该使用一种风格而不是另一种风格。

一个函数定义为

f x = \y => ...

完全等于定义为的函数

f x y = ...

当我们想强调我们喜欢看到 f 时，我们可能更喜欢第一个符号。作为一元函数，其共域由函数组成。当我们希望看到 f 时，我们会使用第二种表示法。作为二元函数。

对于您编写的函数组合

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

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

composite g f x = g (f x)

但这虽然较短，但不是很清楚，因为它建议人类读者考虑 composite作为一个三元函数。作为人类，我也更喜欢第一种形式，但不会偏爱计算机。

如果我不能像你那样使用组合，我会把 Brady 的代码写成

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 = ... 形式的每个定义与 n>0可以看作是语法糖:一种我们可以用来编程的符号，但是在学习与编程语言相关的理论时我们可以忽略它。具体来说，如果我需要在数学上证明所有程序的属性 P , 我不必考虑 P 的情况使用语法糖，但仅限于每个方程的形式为 f = ... 的情况，可能涉及 lambda。这简化了证明，因为我们需要处理更少的案例。

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