是否存在纯函数的术语，只有一个可能的实现？

Question

我正在考虑像身份函数这样的函数：

val f : 'a -> 'a
let f x = x

组成功能：

val compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
let compose f g x = f (g x)

或者，如果定义了monadic map和return函数，则应用bind函数：

val return : 'a -> 'a t
val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t

val ( >>| ) : 'a t -> ('a -> 'b) -> 'b t
let ( >>| ) t f = t >>= fun x -> f x |> return

在每种情况下，只有一个纯函数（忽略相同逻辑的等效表示）可以编写以满足函数的类型签名。

这样的函数有一个术语吗？为什么只能有一个实现呢？

Answer 1

你可以定义自己的函数理论，其中上述函数将具有一些特殊的语义，

type _ fn =
  | Ident : ('a -> 'a) fn
  | Compose : (('b -> 'c) fn -> ('a -> 'b) fn -> ('a -> 'c)) fn
  | Map : (('b -> 'c) fn -> ('a -> ('a -> 'c) -> 'c) fn -> ('a -> ('a -> 'b) -> 'c)) fn
  | Gen : 'a -> 'a fn

最小的语义是将这些抽象的具体化为OCaml函数，即应用函数，

let rec app : type s. s fn -> s = function
  | Ident -> fun x -> x
  | Compose -> fun f g x -> app f (app g x)
  | Map -> fun ret bind x f -> app bind x (fun x -> app ret (f x))
  | Gen f -> f

请注意，提供的app函数是愚蠢的，因为它没有使用Compose和Map应用程序中的函数语义知识，即，Map Ident Ident是Ident，Compose Ident x是x，还有许多其他身份，即使这样简单也可以推断出来。理论。这一切都留给了读者的练习:)

当然，这个额外的间接层将是显而易见的，因为你不能直接编写Ident x，但必须编写app Ident x。除了将所有常规函数提升到理论中，例如，

let 7 = app (Gen (+)) 3 4.