Consider a basic language containing integer and boolean literals along with addition. The first approach to modeling this language could be a type like the following:

data Exp
    = I Int
    | B Bool
    | A Exp Exp

with terms such as I 10, B True, A (I 5) (I 6), and so on. Since this is a language, we will want to end up writing some interpreters for it, such as the following function to pretty-print a term:

pprint :: Exp -> String
pprint (I i)   = show i
pprint (B b)   = show b
pprint (A l r) = "(" ++ pprint l ++ " + " ++ pprint r ++ ")"

The kind of recursion being performed here can be expressed easily as a catamorphism, so let’s go ahead and generalize it out. We’ll use the language of F-algebras, introducing a new type parameter a and replacing all of the recursive references with it.

newtype Fix f = Fix { unFix :: f (Fix f) }

cata :: Functor f => (f a -> a) -> Fix f -> a
cata h = h . fmap (cata h) . unFix

data ExpF a
    = I Int
    | B Bool
    | A a a
    deriving (Functor)

type Exp = Fix ExpF

Then, we can restate our pretty-printer without doing explicit recursion:

pprint :: Exp -> String
pprint = cata go
    where go (I i)   = show i
          go (B b)   = show b
          go (A l r) = "(" ++ l ++ " + " ++ r ++ ")"

But what happens when we want to write an evaluator for our language? The existence of the B constructor “messes everything up” - we can’t just implement eval :: Exp -> Int because not all of our terms will evaluate to an integer. Enter GADTs:

data Exp a where
    I :: Int                -> Exp Int
    B :: Bool               -> Exp Bool
    A :: Exp Int -> Exp Int -> Exp Int

Now, the Exp type is indexed by the type of the expression it represents, so now we can implement a well-typed evaluator:

eval :: Exp a -> a
eval (I i)   = i
eval (B b)   = b
eval (A l r) = eval l + eval r

But now we’re back to where we’ve started in terms of expressing recursive functions. Must we really implement our recursion manually for every GADT we define?

As you might have guessed from the title, the answer is no! We can find fixed points of GADTs in a way that is very similar to the recursive ADTs we are used to.

Constructing HFix

We can’t simply replace every recursive reference with a new type parameter a of kind ★ — since Exp is indexed by a type, we would lose the fact that the argument to the constructor should also be indexed by a type. Instead, let’s introduce a new type parameter f :: * -> *, which will allow us to retain the indexed type:

data ExpF a f where
    I :: Int   ->          ExpF Int  f
    B :: Bool  ->          ExpF Bool f
    A :: f Int -> f Int -> ExpF Int  f

Now we need an analogue to Fix that works for this kind of type. The kind of ExpF is * -> (* -> *) -> *, and our output should be the same kind as our original Exp, so we want a type of kind (* -> (* -> *) -> *) -> (* -> *).

newtype HFix h a = HFix { unHFix :: h a (HFix h) }

type Exp a = HFix ExpF a

Just like in Fix, we instantiate the last type parameter of our input to the fixed-point type, recursively tying the knot. To build up an Exp a, we just apply HFix after applying each constructor from ExpF. Some examples of such terms include HFix $ I 1 and HFix $ A (HFix $ I 2) (HFix $ I 2).

It’s getting rather unwieldy to construct terms of our language, so let’s go ahead and define some smart constructors which use HFix for us:

i :: Int -> Exp Int
i x = HFix $ I x

b :: Bool -> Exp Bool
b x = HFix $ B x

a :: Exp Int -> Exp Int -> Exp Int
a l r = HFix $ A l r

These aren’t necessary to perform our evaluation, but would come in handy in a real-life implementation scenario.

Catamorphisms

Now that we have a fixed-point representation of our data type, we need an analogue of cata for types of this kind. Recall the type of cata:

cata :: Functor f => (f a -> a) -> Fix f -> a

Since Exp can’t be a Functor, we will need a higher-order analogue that fills the same role. Instead of changing our a, however, we will want to change f:

class HFunctor h where
    hmap :: (f a -> g a) -> h a f -> h a g

With a HFunctor, we can lift a natural transformation f a -> g a into a map over h. We can implement HFunctor for ExpF easily:

instance HFunctor ExpF where
    hmap m (I x)   = I x
    hmap m (B x)   = B x
    hmap m (A l r) = A (m l) (m r)

Now, we should be able to express our analogue cataH. With cata, the caller is able to choose what the folding function is, along with the carrier type a. Continuing the analogy, in cataH we will be able to choose the carrier functor f:

cataH :: HFunctor => (h a f -> f a) -> HFix h a -> f a
cataH m = m . hmap (cataH m) . unHFix

The definition of cataH is identical to our previous definition of cata, modulo the choices of typeclass and fixed-point operator. This should give us some confidence that the definition is correct.

Finally, let’s define evaluation for our new fixed type:

eval :: Exp a -> a
eval = cataH go
    where go (I i)   = i
          go (B b)   = b
          go (A l r) = l + r

And we’re done! If your type can be a HFunctor, you can use cataH to perform catamorphisms over it. This same approach can be generalized to types of other kinds in a very similar fashion.