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