#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) orlam :: (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!!!

Leave a Reply

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