# Why does higher-order abstract syntax need an inverse to define catamorphisms?

In the introduction to the colorfully-named Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, Washburn and Weirich describe a problem in traditional formulations of higher-order abstract syntax (HOAS):

One obstacle preventing the widespread use of this technique is the difficulty in using elimination forms, such as catamorphisms, for datatypes containing functions. The general form of catamorphism for these datatypes requires that an inverse be simultaneously defined for every iteration. Unfortunately, many operations that we would like to define with catamorphisms require inverses that do not exist or are expensive to compute.

They go on to demonstrate this problem with a small example, in Haskell. They define the following datatypes to represent simple lambda terms with HOAS:

data Exp = Lam (Exp -> Exp) | App Exp Exp
data Value = Fn (Value -> Value)

Lam represents lambda terms, App represents function application, and Fn represents evaluated functions. They next attempt to define eval :: Exp -> Value, but this causes trouble, as it requires converting a function of type Exp -> Exp to one of type Value -> Value. Since Exp appears in both positive and negative positions, this requires functions from both Exp -> Value and Value -> Exp to define.

The remainder of the paper proposes a solution to that problem, but I am stuck on something else: I don’t understand why it’s a problem at all. Usually, in programming language papers, we define languages with grammars like the following one:

\begin{align*} v &::= \lambda x. e \\ e &::= v \thinspace | \thinspace e \thinspace e \end{align*}

If we define a big-step evaluation relation $$e \Downarrow v$$, we have no need to define some other “unevaluation” relation $$v \Uparrow e$$, as lambdas are already values, so $$\lambda x.e \Downarrow \lambda x.e$$, which is quite straightforward.

It seems to me that a natural translation of the above grammar to HOAS is different from the one Washburn and Weirich present. Specifically, I think it would look more like this:

data Exp = Lit Value | App Exp Exp
data Value = Fn (Value -> Exp)

Defining eval on this grammar is as simple as defining the usual big-step relation:

eval :: Exp -> Value
eval (Lit v) = v
eval (App e1 e2) = case eval e1 of
Fn v -> eval (v (eval e2))

But this solution seems much too simple to be right. Boxes Go Bananas is a well-cited paper from reputable authors published at a reputable PL conference, so its solution surely must have some advantage over the one I presented above. My question, therefore, is simply this: what is that advantage? What am I missing?