所以。我实际上是在修补Idris语言，在某种程度上遵循Brady的Idris类型驱动开发。我不认为我在这里写的内容与特定的编程语言有关(就此而言，我不认识任何 Haskell)。但我不知道我还能在哪里发布这个，因为我对部分应用/咖喱、类型、lambda 和数学家的角度来看的所有东西一无所知。
一些背景
在本书的第二章中，作者提请注意以下情况。
给定自我解释的片段
double : Num a => a -> a double x = x + x rotate : Shape -> Shape其中
Shape : Type和rotate是形状类型和分别将Shape旋转 90 度的函数的孔，quadruple和turn-around函数背后有一个明显的图案quadruple : Num a => a -> a quadruple x = double (double x) turn_around : Shape -> Shape turn around x = rotate (rotate x)这导致我们编写了一个能够应用两次相同运算符的
twice(高阶)函数。
在我看来，解决问题的方法主要有两种。首先是遵循布雷迪的代码
twice : (ty -> ty) -> ty -> ty
twice f x = f (f x)
他实际上定义了twice函数在任意f1上的图像twice f : ty -> ty。
第二个，在我看来更优雅一点，是通过composite函数和/或匿名函数来定义twice，通过稍微改变一下它的签名来定义
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。我们什么时候应该选择通过写作来定义ff x_1 = stuff而不是
f x_1 ... x_{n-2} = stuff2有人可以澄清上面报告的两种方法(布雷迪和我的)之间的区别吗？
1是的，我是一名数学学生...
没有硬性"规则"告诉人们何时应该使用一种风格而不是另一种风格。
定义为
f x = y => ...
正好等于定义为
f x y = ...
当我们想要强调我们希望将f视为一个 1 元函数时，我们可能更喜欢第一种表示法，其协域由函数组成。当我们希望f视为 2 元函数时，我们将使用第二种表示法。
对于您编写的函数组合
composite g f = x => g (f x)
因为组合通常被认为是 2 元函数。我们也可以写
composite g f x = g (f x)
但这虽然更短，但并不那么清楚，因为它建议人类读者将composite视为 3 元函数。作为一个人，我也更喜欢第一种形式，但不会偏爱计算机。
如果我不能像你那样使用组合，我会把布雷迪的代码写成
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
因此，与n>0f x1 .. xn = ...形式的每个定义都可以被视为语法糖：我们可以用来编程的符号，但在研究与编程语言相关的理论时我们可以忽略它。具体来说，如果我需要在数学上证明所有程序P的属性，我不必考虑P使用句法糖的情况，而只需要考虑每个方程都有形式f = ...的情况，可能涉及lambda。这简化了证明，因为我们需要处理更少的情况。
现在，我不太了解伊德里斯，所以我不知道在伊德里斯的所有情况下是否都可以转换为 lambdas。例如，在阿格达，由于依赖消除的方式，这是不可能的。在Coq中，这是可能的。在你需要依赖类型之前，你应该没问题。