在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] 

编辑作为一种事后，如果要实现替换风格代替其中的公式而言，可以遮蔽（通常的范围规则），你最终可能会做这样的事情：

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 

顺便说一句，谨防​​：Substitution is the process of replacing all free occurences of a variable in an expression with an expression.