'Default Behavior' for Haskell recursive data types

Question

I'm trying to write a propositional logic solver in Haskell. I'm representing logical expressions with a recursive data type called 'Sentence' that has several subtypes for different operations - 'AndSentence', 'OrSentence', etc. So I guess it's a tree with several types of node each having 0, 1, or 2 children.

It seems to be working but some of the code is kind of repetitive and I think there ought to be a better way to express it. Basically I have several functions where the 'default behavior' is to just have the function act recursively on the children of a node, bottoming out on certain node types (typically the 'AtomicSentences', which are leaves). So I write a function like:

imply_remove :: Sentence Symbol -> Sentence Symbol
imply_remove (ImplySentence s1 s2) = OrSentence (NotSentence (imply_remove s1)) (imply_remove s2)
imply_remove (AndSentence s1 s2) = AndSentence (imply_remove s1) (imply_remove s2)
imply_remove (OrSentence s1 s2) = OrSentence (imply_remove s1) (imply_remove s2)
imply_remove (NotSentence s1) = NotSentence (imply_remove s1)
imply_remove (AtomicSentence s1) = AtomicSentence s1

and I want a more concise way to write the lines for 'AndSentence', 'OrSentence', and 'NotSentence'.

It seems like functors are similar to what I want, but that didn't work out... I want to act on the subtrees, not on some values contained in each node of the subtrees.

Is there a right way to do this? Or a more natural way to structure my data?

Answer 1

This looks as a nice case for recursion-schemes.

First, we describe your Sentence sym type as a type-level fixed point of a suitable functor.

{-# LANGUAGE DeriveFunctor, LambdaCase #-}

import Data.Functor.Foldable  -- from the recursion-schemes package

-- The functor describing the recursive data type
data SentenceF sym r
   = AtomicSentence sym
   | ImplySentence r r
   | AndSentence r r
   | OrSentence r r
   | NotSentence r
   deriving (Functor, Show)

-- The original type recovered via a fixed point
type Sentence sym = Fix (SentenceF sym)

The above Sentence sym type is almost identical to your original one, except everything must be wrapped inside a Fix. Adapting the original code to use this type is completely mechanical: where we used (Constructor ...), we now use Fix (Constructor ...). For instance

type Symbol = String

-- A simple formula: not (p -> (p || q))
testSentence :: Sentence Symbol
testSentence = 
   Fix $ NotSentence $
      Fix $ ImplySentence
         (Fix $ AtomicSentence "p")
         (Fix $ OrSentence
            (Fix $ AtomicSentence "p")
            (Fix $ AtomicSentence "q"))

Here's your original code, with its redundancies (made worse by the extra Fixes).

-- The original code, adapted
imply_remove :: Sentence Symbol -> Sentence Symbol
imply_remove (Fix (ImplySentence s1 s2)) =
  Fix $ OrSentence (Fix $ NotSentence (imply_remove s1)) (imply_remove s2)
imply_remove (Fix (AndSentence s1 s2)) =
  Fix $ AndSentence (imply_remove s1) (imply_remove s2)
imply_remove (Fix (OrSentence s1 s2)) =
  Fix $ OrSentence (imply_remove s1) (imply_remove s2)
imply_remove (Fix (NotSentence s1)) =
  Fix $ NotSentence (imply_remove s1)
imply_remove (Fix (AtomicSentence s1)) =
  Fix $ AtomicSentence s1

Let's perform a test by evaluating imply_remove testSentence: the result is what we expect:

 -- Output: not ((not p) || (p || q))
 Fix (NotSentence
   (Fix (OrSentence
      (Fix (NotSentence (Fix (AtomicSentence "p"))))
      (Fix (OrSentence
         (Fix (AtomicSentence "p"))
         (Fix (AtomicSentence "q")))))))

And now, let's use the nuclear weapons borrowed from recursion-schemes:

imply_remove2 :: Sentence Symbol -> Sentence Symbol
imply_remove2 = cata $ \case
   -- Rewrite ImplySentence as follows
   ImplySentence s1 s2 -> Fix $ OrSentence (Fix $ NotSentence s1) s2
   -- Keep everything else as it is (after it had been recursively processed)
   s -> Fix s

If we run the test imply_remove2 testSentence, we get the same output as the original code.

What does cata do? Very roughly, when applied to a function like in cata f, it builds a catamorphism, i.e. a function which

1. takes a formula apart into its subcomponents
2. recursively apply cata f to the found subcomponents
3. reassembles the transformed components into a formula
4. passes this last formula (with processed subformulae) to f so that the topmost connective can be affected

The last step is the one doing the actual work. The \case above performs just the wanted transformation. Everything else is handled by cata (and the Functor instance which has been automagically generated).

All the above being said, I wouldn't recommend anyone to lightly move to recursion-schemes. Using cata can lead to very elegant code, yet it requires one to understand the involved machinery, which may not be immediate to grasp (it surely wasn't for me).