CODEWITHSUNDEEP
haskellpattern-matching
Jonathan Prieto-Cubides
Jonathan Prieto-Cubides

Reputation: 2847

Pattern Matching in a Haskell Function

I have many methods that have boilerplate code in their definition, look at the example above. 

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)

As you can see, the definitions for replace function follows a pattern. I want to have the same behavior of the function, simplifying his definition, probably using some pattern matching, maybe with a wildcard _ or X over the arguments, something like: 

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

For avoiding the following definitions:

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)

Is there some way? Forget about the purpose of the function, it could be whatever.

Upvotes: 1

Views: 432

Answers (3)

Daniel Wagner
Daniel Wagner

Reputation: 153182

If you have many constructors that should be treated in a uniform way, you should make your data type reflect that.

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]

Now the pattern match for all binary operators is much easier:

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

To preserve existing code, you can turn on PatternSynonyms and define the old versions of And, Or, and so on back into existence:

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

Upvotes: 5

Gurkenglas
Gurkenglas

Reputation: 2317

Data.Functor.Foldable abstracts the pattern of recursive data structures:

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, beware of 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.

Upvotes: 2

Alec
Alec

Reputation: 32319

I'm not entirely sure this is what you are looking for but you could do the following. The idea is that you can consider a formula to be abstracted over another type (usually a Term in your case). Then, you can define what it means to map over a formula. I tried to replicate your data definitions, although I have some problems with Formula - namely that all the constructors seem to require another 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)

The interesting thing to note is that now the replace function can be applied to anything that is a functor - it even serves as replace for a list!

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

EDIT As an afterthought, if you are implementing a substitution style replace where terms in formulas can be shadowed (the usual scoping rules), you will probably end up doing something like this:

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

Which isn't as cute, but also isn't as straightforward pf a problem.

Upvotes: 2

Related Questions