### March 2008

You may recall the definition for an exponential functor from my previous entry, which can also be viewed, I suppose, as functors in the
category of right-invertible functions in Haskell.

```
class ExpFunctor f where
xmap :: (a -> b) -> (b -> a) -> f a -> f b
```

Clarifying the above, an instance of ExpFunctor should satisfy the slightly generalized version of the Functor laws from Control.Monad:

```
xmap id id = id
xmap f g . xmap f' g' = xmap (f . f') (g' . g)
```

Since we like to apply xmap to a pair of functions such that f . g = id, as in the Fegaras/Sheard case, we get:

```
xmap f g . xmap g f
= xmap (f . g) (f . g) -- by second xmap law
= xmap id id 	       -- by f . g = id
= id		       -- by first xmap law
```

In any event, what I thought what I'd do today is note that Wouter Swierstra's Data Types a la Carte approach works over exponential functors.

I have been trying out various representations for higher-order abstract syntax (HOAS) in Haskell, with an eye towards seeing what I can actually use to get real work done and I have run into a few unexpected headaches, and a couple of neat observations. That said, I should probably start by explaining some terminology.

Encoding a language that binds variables in higher order abstract syntax generally involves constructing an abstract data type that contains functions. A functor for representing expressions from Berendregdt's lambda cube in HOAS goes something like (ignoring any consolidation of binders and sorts)

```
data F a
= Lam a (a -> a)
| Pi a (a -> a)
| App a a
| Star
| Box
```

There are a number of mathematical functors that are not instances has Haskell's Functor class, such as the above.