2
$\begingroup$

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.

Improve this question
$\endgroup$
8
  • $\begingroup$ $\mathsf{lam}_{A, B, C} : \mathscr C(A \times B, C) \to \mathscr C(A, C^B)$ is a bijective function between hom-sets in a cartesian-closed category $\mathscr C$; it's not a functor. I'm not sure what you mean by "not just looking for what higher order abstract means for Cartesian closed categories", because the interpretation of these constructions categorically is given by structure in a cartesian-closed category, and to understand the relationship is to understand higher-order abstract syntax categorically. $\endgroup$
    – varkor
    Sep 1, 2020 at 18:18
  • $\begingroup$ @Varkor Higher order syntax isn't only about Cartesian closed categories. You don't even need exponential objects for hoas. For example, I have found useful something like letBe : (Lam () a -> Lam env b) -> Lam (env, a) b, also letLabel : (Lam a Void -> Lam b env) -> Lam b (a + env) $\endgroup$
    – Molly Stewart-Gallus
    Sep 1, 2020 at 19:53
  • 1
    $\begingroup$ I'm unclear exactly what structure you are describing, but if you have any binding structure in the syntax (even if not explicitly $\lambda$-abstraction and application), the corresponding categorical analogue will be residual objects (in particular, exponential objects if the binding structure permits exchange, weakening and contraction). The category does not have to be closed, though this is generally the case in practice. $\endgroup$
    – varkor
    Sep 1, 2020 at 20:56
  • $\begingroup$ @Varkor not sure how products correspond to residual objects. In any case I think what I really want is how to work in the internal language of the category and about the Lang and Syn (Syntactic Category) functors. $\endgroup$
    – Molly Stewart-Gallus
    Sep 2, 2020 at 18:06
  • $\begingroup$ Exponential objects correspond to residual objects, just as cartesian products correspond to tensor products. $\endgroup$
    – varkor
    Sep 2, 2020 at 18:12

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.