functional-programming - OCamlが関数マッチングを許可しないのはなぜですか？

Question

私が行った場合

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

却下されました。

OCamlが関数マッチングを許可しないのはなぜですか？

Answer 1

Ocaml（Haskellのような）は、ラムダ計算に基づいています。2つの関数を比較することは、一般的に決定不可能です。2つの関数を比較できる場合は、関数が終了するかどうかを判断できます。しかし、あなたの言語がチューリング完全である場合、それはできません。

私たちが使用するすべての一般的な言語はチューリング完全です：それらは何でも計算することができます。

ですから、場合によっては可能かもしれませんが、一般的な言語では不可能です。

Answer 2

それには多くの難しい問題があります。

• 機能はどの程度正確に一致する必要がありますか？たとえばfun x -> x + 1、あなたのバージョンと一致する必要がありますか？どうfun i -> 1 + iですかfun i -> ((fun x -> i+1) 42)？AFAIKには、2つの任意の関数が動作的に同等であることを証明する方法はありません（純粋なラムダ計算のような関数の場合は、そうなる可能性があります）。

• 関数はコンパイルされ、その構文構造は実行時に存在しなくなります。ただし、IDによって関数を照合することは確かに可能です。

• パターンマッチングは値を分解することですが、OCamlには、関数で使用される変数をパターンの一部である変数と区別するための表記法はありません。

私のマスターの間に、ラムダ式を統合することができたLambdaPrologを研究しました。それは非常に美しいように見えましたが（私の記憶には少し遠いですが）、言語は通常のPrologよりもさらに人気のない研究プロトタイプでした…それについてのニュースがあれば嬉しいです:)

Answer 3

平等のために関数を比較することは困難です。関数のテキスト表現に基づいて等式を定義する場合は、とはfun x -> x + 1異なるものを比較しfun x -> 1 + xます。これはあまり役に立ちません。関数の値に基づいて等式を定義すると、結果は計算できません。結論は、賢明な定義がないということです。