所以，我其实是在修饰伊德里斯的语言，有点效仿布雷迪的做法。类型驱动开发与Idris. 我不认为我在这里写的是什么。该 与特定的编程语言联系在一起（我也不懂什么Haskell，就这点而言）。但我不知道还能在哪里发这个帖子，因为我对部分应用currying、类型、lambdas和所有这些从数学家角度看的东西一无所知。
在本书的第二章中，作者提请大家注意以下情况。
给出了一个自明的片段
double : Num a => a -> a double x = x + x rotate : Shape -> Shape哪儿
Shape : Type和rotate是形状的类型和旋转函数的孔。Shape分别为90度，背后有一个明显的规律。quadruple和aturn-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 在任意 f1.
第二种，在我看来更优雅一点，就是定义为 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
谁能给我澄清一下上面报道的两种方法（布雷迪的和我的）的区别？
没有硬性的 "规则 "告诉我们什么时候应该使用一种风格而不是另一种风格。
一个函数定义为
f x = \y => ...
完全等于定义为
f x y = ...
当我们想强调我们喜欢看的时候，我们可能更喜欢第一种记法。f 作为一个1-ary函数，其密码域是由函数组成的。当我们希望看到的时候，我们会使用第二种符号来代替 f 作为一个二元函数。
对于函数组成，你写道
composite g f = \x => g (f x)
因为组成通常被认为是一个2-ary函数。我们也可以写成
composite g f x = g (f x)
但这虽然较短，却不那么清晰，因为它建议人类读者考虑的是 composite 作为一个3-ary函数。作为人类，我也更喜欢第一种形式，但对于计算机来说，不会有任何偏好。
如果我不能像你一样使用组成，我会把布雷迪的代码写成
twice f = \x => f (f x)
强调我们真的希望看到 twice 作为函数到函数的映射（说得挑剔一点，是endo到endo）。这两种形式是完全等同的。
最后，再来一个更成熟的说明：从基础的角度来看，没有必要用符号来表示
f x1 ... xn = stuff
我们常用来定义函数。极为迂腐的说，上面其实并没有定义出 f但只定义了如何 f 当应用到 n 参数。既然我们知道那是唯一的标识。f我们不关心这个 但是，如果我们这样做，我们会定义 f 就像我们定义其他任何东西一样，即用一个定义方程，其形式是
f = something
特别是
f = \x1 .. x2 => stuff
所以，每一种形式的定义 f x1 .. xn = ... 与 n>0 可谓 句法糖符号：一个我们可以用来编程的符号，但在研究编程语言相关理论时，我们可以忽略这个符号。具体来说，如果我需要在所有程序上用数学方法证明一个属性 P我不需要考虑以下情况，即 P 使用了语法糖，但只有在每个方程都有以下形式的情况下才会使用。f = ...，可能涉及到lambdas。这简化了证明，因为我们需要处理的情况比较少。
现在，我对Idris了解不多，所以我不知道在Idris中，这种转换为lambdas的方法是否在所有情况下都能实现。在Agda中，这是不可能的，因为例如，依赖性消除是如何进行的。在Coq中，这反而是可能的。在你需要依赖类型之前，你应该没有问题。