# #StackBounty: #functional-programming #category-theory What is the category theory interpretation of higher order abstract syntax?

### Bounty: 50

Suppose you have a simple sort of lambda calculus abstract syntax tree. The fine details don’t really matter.

``````data T = Unit | Void | T :*: T | T :+: T | T :-> T | I

data Term x a where
Var :: x -> Term x x
Int :: Int -> Term x I
Add :: Term x I -> Term x I -> Term x I
Apply :: Term x (a :-> b) -> Term x a -> Term x b
Lambda :: (x -> Term x b) -> Term x (a :-> b)

lam :: (Term x a -> Term x b) -> Term x (a :-> b)
lam f = Lambda (x -> f (Var x))

newtype Program a = Program (forall x. Term x a)
``````

How is this sort of structure to be interpreted according to category theory?

I understand that closed cartesian categories are supposed to capture the notion of the lambda calculus and have written more than one compiler from such a higher order abstract syntax abstract syntax tree to closed cartesian categories myself but still don’t really "get" what higher order abstract syntax is supposed to mean in terms of category theory.

`lam` doesn’t really seem to be a sort of functor to me. If `lam` was some functor operation wouldn’t we want a type sort of like `lam :: (a -> b) -> Term x (F a :-> F b)` or`lam :: (Term x a -> Term x b) -> Term x (F a :-> F b)` for some sort of `F`.

I thought this sort of thing might be related to the Yoneda embedding and tried explicitly thinking of the free variable parameter as an environment argument and Lam as a category not just a AST.

``````data T = Unit | Void | T :*: T | T :+: T | T :-> T | I

data Lam env result where
Id :: Lam a a
(:.:) :: Lam b c -> Lam a b -> Lam a c

Coin :: Lam env Unit
Left :: Lam a (a :+: b)
Right :: Lam b (a :+: b)
Fanout :: Lam env a -> Lam env b -> Lam env (a :*: b)
Curry :: Lam (b :*: a) c -> Lam a (b :-> c)
Absurd :: Lam Void r
First :: Lam (a :*: b) a
Second :: Lam (a :*: b) b
Fanin :: Lam a r -> Lam b r -> Lam (a :+: b) r
Uncurry :: Lam a (b :-> c) -> Lam (b :*: a) c

-- Some extra stuff
Int :: Int -> Lam env I
Add :: Lam env I -> Lam env I -> Lam env I

newtype Program a = Program (forall env. Term env a)
``````

But I didn’t really find the Yoneda embedding to simplify things much.

``````yo :: (forall env. Lam env a -> Lam env b) -> Lam a b
yo f = f Id
``````

I don’t have a problem figuring out how to compile one representation to another but I just don’t understand what higher order abstract syntax is supposed to mean.

And to be clearer I’m not just looking for what higher order abstract means for Cartesian closed categories but what it means for any sort of language whether it be about some sort of affine language or is some sort of relational Prolog sort of thing.

Get this bounty!!!

This site uses Akismet to reduce spam. Learn how your comment data is processed.