4
$\begingroup$

Category theory often captures the hearts of computer scientists because of its uncanny capacity to cleanly describe CS concepts. A common example is the way Algebraic Data Types can be represented as product and coproduct.

Homoiconicity is a label for programming languages where "the primary representation of programs is also a data structure in a primitive type of the language itself". I might describe it as a recursive relationship between a program's syntax and its semantics. The main benefit of using a homoiconic language is that it unlocks some very powerful metaprogramming capabilities. Lisp and Prolog are common examples of such languages that deliver on this promise of powerful metaprogramming. A Couple of Meta-interpreters in Prolog is a nice introduction to this kind of metaprogramming for Prolog.

I have a CS-background and I found the isomorphism between ADTs and the CT concepts product and coproduct quite clarifying for understanding ADTs. Similarly, I could say I have a practical understanding of homoiconicity, but not in the illuminating way that a categorical description of it may provide.

Thus this question (stated a few ways):

Is there a way to describe the relationship between the higher-level representation of a program and its representation in a primitive datatype in category theory terms?

or

Is there is a categorical description of homoiconicity that captures its essence?

or

What is the category of homoiconicity?

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ I'm not sure category theory is the place to look for this. If by "primary representation of programs" you mean something like an abstract syntax tree of its source code, then you have to deal with the problem that there are many ways that two programs can be "the same", on the intensional–extensional spectrum. There is a similar issue about functions in mathematics, but by and large mathematicians have chosen to think about functions extensionally. In particular, to think of programs as morphisms in some nice category usually requires adopting extensionality to some minimal degree. $\endgroup$
    – Zhen Lin
    Apr 17, 2021 at 0:54
  • 1
    $\begingroup$ @ZhenLin Is not it somehow reminiscent of features that should be present in Joyal's arithmetic universes? I mean some structure on a category $C$ enabling to interpret comparison of certain properties of internal categories in $C$ with same properties of $C$ itself? $\endgroup$
    – მამუკა ჯიბლაძე
    Apr 17, 2021 at 5:43
  • $\begingroup$ @ZhenLin Thanks for the pointer to intensional logic, very interesting philosophical topic I was not familiar with. I found plato.stanford.edu/entries/logic-intensional which seems to be a decent introduction which I'm still reading. I agree that this seems to be related to my question, especially when held up to my description of homoiconicity as "a recursive relationship between a program's syntax and its semantics". But be careful pointing me to such fascinating topics, my next question is dangerously close to being "What is the category of intensional logic?" :D $\endgroup$
    – infogulch
    Apr 17, 2021 at 16:20
  • $\begingroup$ @მამუკაჯიბლაძე ah the connection to Gödel incompleteness seems clear now that you mention it. IIRC, Gödel's strategy was to take a logical construction of numbers and use numbers to construct a syntax for logic and interpret it. While his purpose with such a tool was to disprove simultaneous completeness and consistency, homoiconic languages perhaps consider what else one might do with it. Thus a categorical proof of Gödel incompleteness results seems like it might be a good place to try to extract the shape of this kind of self-representational structure for this question. Thanks! $\endgroup$
    – infogulch
    Apr 17, 2021 at 16:36

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.