Why OCaml does not allow function matching? [close

问题:

if I do

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

It got rejected.

Why OCaml does not allow function matching?

回答1:

There are many difficult problems with that.

• How precisely should functions match? E.g. should fun x -> x + 1 be a match with your version? How about fun i -> 1 + i or fun i -> ((fun x -> i+1) 42)? AFAIK there is no way to prove that two arbitrary functions are behaviorally equivalent (well there might be, in the case of pure lambda-calculus-like functions).

• Functions are compiled and their syntactic structure does not exist anymore at runtime. It would certainly be possible to match functions by identity, though.

• Pattern matching is about deconstructing values, but there is no notation in OCaml to differentiate variables used in the function from variables that are part of the pattern.

During my master we studied Lambda Prolog, which was able to unify on lambda-expressions; that seemed quite beautiful (it's a bit far for my memory though) but the language was a research prototype even less popular than normal Prolog… I would be happy to have news about it :)

回答2:

Ocaml (like Haskell), is based on Lambda Calculus. Comparing two functions is undecidable in general : If you can compare two function, then you can say if a function terminates or not. But, if you language is Turing-Complete, you can't.

All general languages we use are Turing-Complete : they are able to compute anything.

So, maybe it would be possible in some case, it's impossible in general languages.

回答3:

Comparing functions for equality is difficult. If you define equality based on the textual representation of the functions, then fun x -> x + 1 compares different from fun x -> 1 + x. This isn't so useful. If you define equality based on the values of the functions, the result isn't computable. The upshot is that there's no sensible definition.