Почему OCaml не позволяет сопоставлять функции? [закрытый]

Если я это сделаю 

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

Оно было отвергнуто.

Почему OCaml не позволяет сопоставлять функции?

3 2
functional-programming ocaml

3 ответа:

С этим связано много сложных проблем.

  • Насколько точно должны совпадать функции? Например, должен ли fun x -> x + 1 совпадать с вашей версией? Как насчет fun i -> 1 + i или fun i -> ((fun x -> i+1) 42)? АФАИК нет никакого способа доказать, что две произвольные функции являются поведенчески эквивалентными (ну, может быть, в случае чистых функций, подобных лямбда-исчислению).

  • Функции компилируются, и их синтаксическая структура больше не существует во время выполнения. Конечно, можно было бы сопоставить однако функционирует по принципу идентичности.

  • Сопоставление по шаблону - это деконструкция значений, но в OCaml нет обозначения, позволяющего отличать переменные, используемые в функции, от переменных, входящих в шаблон.

Во время моего мастера мы изучали лямбда-пролог, который был способен объединяться на лямбда-выражениях; это казалось довольно красивым (это немного далеко для моей памяти, Хотя), но язык был исследовательским прототипом даже менее популярным, чем обычный Пролог... я был бы счастлив иметь Новости об этом:)

3

Ocaml (как и Haskell), основан на лямбда-исчислении. Сравнение двух функций вообще неразрешимо : если вы можете сравнить две функции, то вы можете сказать, завершается ли функция или нет. Но, если ваш язык является Тьюринг-полным, вы не можете.

Все общие языки, которые мы используем, являются полными Тьюринга : они способны вычислять что угодно.

Так что, возможно, это было бы возможно в каком-то случае, это невозможно в общих языках.

4

Сравнение функций для равенства затруднительно. Если вы определяете равенство на основе текстового представления функций, то fun x -> x + 1 сравнивает отличное от fun x -> 1 + x. Это не так уж и полезно. Если вы определяете равенство на основе значений функций, результат не поддается вычислению. В итоге получается, что нет никакого разумного определения.

2