为什么 OCaml 不允许函数匹配？ [关闭]答案

【问题标题】：Why OCaml does not allow function matching? [closed]为什么 OCaml 不允许函数匹配？ [关闭]
【发布时间】：2012-12-07 10:05:44
【问题描述】：

如果我这样做了

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

它被拒绝了。

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

【问题讨论】：

【解决方案1】：

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

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

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

【讨论】：

【解决方案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 更不受欢迎......我很高兴有关于它的消息:)

【讨论】：

戴尔·米勒、戈帕兰·纳达图尔等人。已经开发并继续维护Teyjus，这是 lambda-prolog 的一个很好的实现。他们还通过Abella 进入证明助手领域，该领域使用相关的编码来reason 关于语法术语。

【解决方案3】：

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

【讨论】：