1

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.

Improve this question
2
  • Maybe DeriveFunctor or make an explicit instance of it? Then the above might end up as replace x y = fmap (\z -> if x == z then y else x). Of course, that means that Formula will have kind * -> *, but that sounds reasonable. Formula Bool would be a boolean formula. Commented Apr 23, 2016 at 5:55
  • You could make Formula an instance of Compos, would that help? Commented Apr 23, 2016 at 12:05

3 Answers 3

Reset to default
5

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
Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

I like that but the bad news are with this I must rewrote every single method.
@jonaprieto I have added a sentence to address this concern.
2

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.

Improve this answer

1 Comment

I don't think that last one is going to work. fmap is going to expect something of type a -> a, but you're handing it something of type Formula a -> Formula a. (But the rest of the advice here is solid.)
2

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.

Improve this answer

1 Comment

I wonder why was this downvoted? Is there any issue with this approach? (Beyond variable capturing and substituting non free occurrences, which are common with other answers so far)

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.