Vilem, I suggest to use free monads. They reduce boilerplate a little. First, separate the variable form the rest of the syntax: data Prop v = Not v | And v v | Or v v | If v v | Iff v v -- maybe GHC can derive this instance for you, given the appropriate language extension flag. instance Functor Prop where fmap f (Not p) = Not (f p) fmap f (And p q) = And (f p) (f q) fmap f (Or p q) = Or (f p) (f q) fmap f (If p q) = If (f p) (f q) fmap f (Iff p q) = Iff (f p) (f q) Then use Control.Monad.Free from the package 'free'. It also has a template Haskell part. The function you want is called 'iter' there, and applying a context of type var -> Bool is simply fmap. Note that a Map from var to Bool does not always yield a total reduction, since your formula might contain variables that are not in the Map. data Free f var = Pure var | Free (f (Free f var)) instance Functor f => Monad (Free f) where return = Pure Pure a >>= f = f a Free m >>= f = Free (fmap ((=<<) f) m) type Proposition var = Free Prop var type Predicate = Free Prop Bool -- F-algebras for functor f class Functor f => FAlg f a where alg :: f a -> a instance FAlg Prop Bool where alg (Not b) = not b alg (And p q) = p && q alg (Or p q) = p || q alg (If p q) = not p || q alg (Iff p q) = p == q eval = iter alg :: Predicate -> Bool map_and_eval ctx = iter alg . fmap ctx If feasible, remove If and Iff from the Prop type and make them binary functions on type Proposition var instead. That reduces the boilerplate further. -- Olaf