1. 9
  1.  

  2. 5

    There’s some deep mathematics to reinforce this statement and make it more precise. Precisely, composition is how the ambient compiler interprets computational effects.

    Recall that a Turing category is a Cartesian closed category (indeed, a topos) whose objects are the types of some programming language and whose arrows are the computable programs on those types. A Turing category has at least one Turing object, a type which can represent any arrow in the category, including all of the computable elements. What I mean by that, specifically, is that there is a family of embedding arrows which send any type to the Turing object, and another family of retracting arrows which send the Turing object to any desired type, such that embedding and then retracting is like doing nothing. Turing objects are the types of code literals. There can be multiple Turing objects, but I’ll assume that there’s just one, traditionally called A.

    To do some abstract nonsense to orient ourselves, let’s imagine that we have a value x of some type X, written x : X. Categorically, this is an element of X, by which we mean an arrow x : 1 → X from the terminal object which merely picks x. In programming, a terminal object is going to be something like null or void; think of starting from a blank slate or empty environment or fresh prompt. So our embedding will send x to a code literal [x] which we could then evaluate via retraction to give x again. Note that the code literal [x] : 1 → A is an element of the Turing object.

    A Turing category is entirely characterized by one operation per Turing object, called “Kleene composition” after Kleene’s Recursion Theorem, which is built on the same concept. (The literature also calls this the “Turing morphism”, but that is confusing.) The composition operation takes two elements [f] : 1 → A and [x] : 1 → A, and returns their composition as if they had been evaluated and then re-embedded, [f(x)] : 1 → A. However, since Kleene composition is itself computable, there are many different ways to compose, each corresponding to a different arrow of type (A, A) → A. If Turing objects are the types of code literals, then Kleene compositions are the different programs which can optimize those code literals without changing their behavior.

    Now we can demystify my first line. Kleene composition gives us the behavior for the values which we are composing. Our runtime behind the REPL will take what we write, turn it into code literals, and use its Kleene composition to append what we’ve written into what has been run so far. Then, any effects which need to be run in order to account for the appended code are interpreted by the interpreter.

    1. 3

      I really appreciate your comments.

      1. 2

        I almost posted the same thing, but I decided against it. Glad to see that I’m not the only one thinking it!

        1. 3

          I’m humbled and flattered by y’all’s praise. I just hope that I’m not making things harder to understand.

    2. 3

      Agree that semiotics is under studied and under applied in software, while maths and math-like ideas are super heavily over applied. I don’t think we have quite enough useful lenses to usefully analyze and understand software.

      On the topic of “glue code” and interpretation, I think there’s a distinction to be made between translating the same information to a new shape vs generating new information. A lot of software doesn’t generate new information (doesn’t “compute” anything). E.g. when you parse or serialize something, or when you invert a 1:1 dictionary - you just reorganize the data but the “information content” (what we can interpret in terms of domain knowledge when looking at that data) remains the same, or even goes down. (I’m not 100% sure we can nail down this distinction, though.) Then a lot of software has to do with just transmitting information between different locations (including persistence, in a way) and not “computing” anything. Yes our models of looking at software are starkly limited - so much work is done just looking at functions and types. We haven’t even figured out how to model clean separation of subject domain concepts from implementation yet.

      Side note, here’s an interesting paper on a “semiotic programming language” called Semprola: https://www.shift-society.org/salon/papers/#semprola-a-semiotic-programming-language