functional-programming - 为什么 OCaml 不允许函数匹配？

Question

如果我做

match (fun i -> i + 1) with
   (fun i -> i + 1) -> true;;

它被拒绝了。

为什么 OCaml 不允许函数匹配？

Answer 1

Ocaml（如 Haskell）基于 Lambda 演算。比较两个函数通常是不确定的：如果你可以比较两个函数，那么你可以说一个函数是否终止。但是，如果你的语言是图灵完备的，你就不能。

我们使用的所有通用语言都是图灵完备的：它们能够计算任何东西。

所以，也许在某些情况下是可能的，在一般语言中是不可能的。

Answer 2

有很多困难的问题。

• 函数应该匹配到什么程度？例如应该fun x -> x + 1与您的版本匹配？fun i -> 1 + i或者怎么样fun i -> ((fun x -> i+1) 42)？AFAIK 没有办法证明两个任意函数在行为上是等价的（在纯 lambda-calculus-like 函数的情况下可能存在）。

• 函数被编译并且它们的句法结构在运行时不再存在。不过，当然可以通过身份匹配功能。

• 模式匹配是关于解构值，但 OCaml 中没有符号来区分函数中使用的变量和模式一部分的变量。

在我的硕士期间，我们学习了 Lambda Prolog，它能够统一 lambda 表达式；这看起来很漂亮（虽然对我的记忆来说有点远）但是该语言是一种研究原型，甚至比普通 Prolog 更不受欢迎......我很高兴有关于它的消息 :)

Answer 3

比较函数是否相等是困难的。如果您根据函数的文本表示定义相等，则fun x -> x + 1比较不同于fun x -> 1 + x. 这不是很有用。如果您根据函数的值定义相等，则结果是不可计算的。结果是没有合理的定义。