Соответствие шаблону в функции Haskell

Question

У меня есть много методов, которые имеют шаблонный код в их определении, посмотрите на пример выше.

replace:: Term -> Term -> Formula -> Formula 
replace x y (Not f)   = Not $ replace x y f 
replace x y (And f g)   = And (replace x y f) (replace x y g) 
replace x y (Or f g)   = Or (replace x y f) (replace x y g) 
replace x y (Biimp f g)  = Biimp (replace x y f) (replace x y g) 
replace x y (Imp f g)   = Imp (replace x y f) (replace x y g) 
replace x y (Forall z f)  = Forall z (replace x y f) 
replace x y (Exists z f)  = Exists z (replace x y f) 
replace x y (Pred idx ts)  = Pred idx (replace_ x y ts) 

Как вы можете видеть, определения для replace функции следует шаблон. Я хочу иметь такое же поведение функции, упрощая его определение, вероятно, используя некоторые сопоставления с образцом, может быть, с групповым символом _ или X над аргументами, что-то вроде:

replace x y (X f g)   = X (replace x y f) (replace x y g) 

Для избежания следующих определений:

replace x y (And f g)   = And (replace x y f) (replace x y g) 
replace x y (Or f g)   = Or (replace x y f) (replace x y g) 
replace x y (Biimp f g)  = Biimp (replace x y f) (replace x y g) 
replace x y (Imp f g)   = Imp (replace x y f) (replace x y g) 

Есть ли способ? Забудьте о цели функции, это может быть что угодно.

Answer 1

Если у вас есть много конструкторов, к которым следует обращаться единообразно, вы должны сделать так, чтобы ваш тип данных отражал это.

data BinOp  = BinAnd | BinOr | BinBiimp | BinImp 
data Quantifier = QForall | QExists 
data Formula = Not Formula 
       | Binary BinOp Formula Formula -- key change here 
       | Quantified Quantifier Formula 
       | Pred Index [Formula] 

Теперь матч шаблон для всех бинарных операторов намного проще:

replace x y (Binary op f g) = Binary op (replace x y f) (replace x y g) 

Чтобы сохранить существующий код, вы можете включить PatternSynonyms и определить старые версии And, Or, и так далее назад в существование:

pattern And x y = Binary BinAnd x y 
pattern Forall f = Quantified QForall f 

Answer 2

Я не совсем уверен, что это то, что вы ищете, но вы можете сделать следующее. Идея состоит в том, что вы можете рассмотреть формулу, которая будет абстрагироваться над другим типом (обычно в вашем случае Term). Затем вы можете определить, что означает отображение по формуле. Я попытался повторить ваши определения данных, хотя у меня есть некоторые проблемы с Formula - а именно, что все конструкторы, похоже, требуют еще Formula ...

{-# LANGUAGE DeriveFunctor #-} 

data Formula a 
    = Not (Formula a) 
    | And (Formula a) (Formula a) 
    | Or (Formula a) (Formula a) 
    | Biimp (Formula a) (Formula a) 
    | Imp (Formula a) (Formula a) 
    | Forall a (Formula a) 
    | Exists a (Formula a) 
    | Pred a (Formula a) 
    deriving (Functor) 

data Term = Term String {- However you define it, doesn't matter -} deriving (Eq) 

replace :: (Functor f, Eq a) => a -> a -> f a -> f a 
replace x y = fmap (\z -> if x == z then y else z) 

Интересно отметить, что в настоящее время функция replace может быть применен к чему-либо, что является функтором - он даже служит replace для списка!

replace 3 9 [1..6] = [1,2,9,4,5,6] 

EDIT Подумав, если вы реализуете стиль заместительной заменить, когда члены формулы могут быть затененный (обычные правила видимости), вам, вероятно, в конце концов сделать что-то вроде этого:

replace' :: (Eq a) => a -> a -> Formula a -> Formula a 
replace' x y f@(Forall z _) | x == z = f 
replace' x y f@(Exists z _) | x == z = f 
replace' x y f@(Pred z _) | x == z = f 
replace' x y formula = fmap (replace' x y) formula 

Это не так мило, но и не так просто, как проблема.

Answer 3

Data.Functor.Foldable абстрагирует структуру рекурсивных структур данных:

import Data.Functor.Foldable 

data FormulaF t 
    = Not t 
    | And t t 
    | Or t t 
    | Biimp t t 
    | Imp t t 
    | Forall A t 
    | Exists A t 
    | Pred B C 
    deriving (Functor, Foldable, Traversable) 

type Formula = Fix FormulaF 

replace :: Term -> Term -> Formula -> Formula 
replace x y = cata $ \case -> 
    Pred idx ts -> Pred idx (replace_ x y ts) 
    f -> f 

Кстати, остерегайтесь replace x y (Forall x (f x)) = Forall x (f y): Substitution is the process of replacing all free occurences of a variable in an expression with an expression.