functional-programming - 纯函数只有一种可能的实现吗？

Question

下图中有一个快速解释，为什么纯函数似乎只有一种可能的实现。
我不太明白这个想法，因为 (++) : ('a -> 'b) -> ('a -> 'b) -> 'a -> 'b 例如可以通过 let (++) (f: ('a -> 'b )) (g: ('a -> 'b)) x = f x 或
let (++) (f: ('a -> 'b)) (g: ( 'a -> 'b)) x = g x
这张图片是错误的还是我错过了什么？

Answer 1

你是对的。即使没有类型注释，所附图像也不正确。

首先，重要的是要考虑这里假设的实现的“平等”类型。让我们考虑以下示例。

1. (@@) 等于 (@@+) 吗？

   let ( @@ ) f x = f x
   let ( @@+ ) f x =
     let _ = 42 in
     f x
   

2. (|>) 等于 (|>+) 吗？

   let ( |> ) x f = f x
   let ( |>+ ) x f = f @@ x
   

3. (%) 等于 (%+) 吗？

   let ( % ) f g x = f (g x)
   let ( %+ ) p q r = p (q r)
   

如果(@@)不等于(@@+)，那么我们可以构造函数的第五个实现bool -> bool，例如(fun x -> let _ = 42 in true)。

因此，图像的作者希望不是通过其实现(或代码)来区分函数，而是通过一些其他元素(例如其行为)来区分(如 duck test 或数学函数的等式)。

尽管如此，图像还是不正确。该图像声称“对于签名中没有任何具体类型的纯函数，只有一种可能的实现”，但事实并非如此。例如，不存在纯函数'a -> 'b。这可以通过 the Curry–Howard correspondence 显示.