Musterabgleich in einer Haskell-Funktion

Question

Ich habe viele Methoden, die in ihrer Definition einen Standardcode haben, siehe obiges Beispiel.

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) 

Wie Sie sehen können, folgt die Definitionen für replace Funktion ein Muster. Ich möchte das gleiche Verhalten der Funktion haben, seine Definition zu vereinfachen, wahrscheinlich einige Musteranpassung verwendet wird, vielleicht mit einem Platzhalter _ oder X über die Argumente, so etwas wie:

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

Zur Vermeidung folgende Definitionen:

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) 

Gibt es einen Weg? Vergiss den Zweck der Funktion, es könnte was auch immer sein.

Answer 1

Wenn Sie viele Konstruktoren haben, die einheitlich behandelt werden sollten, sollten Sie Ihren Datentyp darauf reflektieren lassen.

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] 

Nun ist die Mustererkennung für alle binären Operatoren ist viel einfacher:

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

vorhandenen Code zu sparen, sollten Sie auf PatternSynonyms und definieren Sie die alten Versionen von And drehen kann, Or, und so weiter zurück ins Leben:

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

Answer 2

Ich bin nicht ganz sicher, dass dies das ist, was Sie suchen, aber Sie könnten Folgendes tun. Die Idee ist, dass Sie eine Formel als abstrahiert über einen anderen Typ (in der Regel eine Term in Ihrem Fall) betrachten können. Dann können Sie definieren, was es bedeutet, über eine Formel zu mappen. Ich habe versucht, Ihre Datendefinitionen zu replizieren, obwohl ich einige Probleme mit Formula haben - nämlich, dass alle Konstrukteure eine andere Formula zu verlangen scheinen ...

{-# 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) 

Die interessante Sache zu beachten, dass jetzt die replace Funktion angewendet werden kann zu allem, was ein Funktor ist - es dient sogar als replace für eine Liste!

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

EDIT Als nachträglicher Einfall, wenn Sie einen Ersatz-Stil ersetzen implementieren, wo Begriffe in Formeln beschattet werden können (die üblichen Scoping-Regeln), werden Sie wahrscheinlich etwas am Ende wie folgt vorgehen:

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 

Das ist nicht so süß, aber auch nicht so einfach ein Problem.

Answer 3

Data.Functor.Foldable abstrahiert das Muster der rekursive Datenstrukturen:

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 

By the way, passen sie von 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.