Есть ли расширяемый и эффективный способ написания экзистенциальных операторов в Haskell без реализации встроенного языка программирования логики? Часто, когда я реализую алгоритмы, я хочу выразить экзистенциально количественные утверждения первого порядка, такие как
∃x.∃y.x,y ∈ xs ∧ x ≠ y ∧ p x y
, где ∈
перегружено в списках. Если я тороплюсь, я могу написать понятный код, похожий на
find p [] = False
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs
или
find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs]
. Но этот подход плохо обобщается на запросы, возвращающие значения, предикаты или функции с несколькими арностями. Например, даже такой простой оператор, как
∃x.∃y.x,y,z ∈ xs ∧ x ≠ y ≠ z ∧ f x y z = g x y z
, требует написания другой процедуры поиска. А это означает значительный объем шаблонного кода. Конечно, такие языки, как Curry
или Prolog
, которые реализуют сужение или механизм разрешения, позволяют программисту писать такие операторы, как:
find(p,xs,z) = x ∈ xs & y ∈ xs & x =/= y & f x y =:= g x y =:= z
, значительно злоупотребляя нотацией, которая выполняет как поиск, так и возвращает значение. Эта проблема часто возникает при реализации формально заданных алгоритмов и часто решается с помощью комбинаций таких функций, как fmap
, foldr
и mapAccum
, но в основном явная рекурсия.Есть ли более общий и эффективный или просто общий и выразительный способ написания такого кода на Haskell?