Concatenative programming languages
John Purdy has a good overview of concatenative programming languages. He points out that they are built around function *concatenation*, rather than function *application*, but also points out that this definition does really help explain *why* they're useful or interesting.
A different view that he describes is that *everything* in a concatenative language is a function that operates on a stack — and in particular, on a *prefix* of the stack. If you were to type one of these functions, you could explicitly include the “stack variable” that shows how the function's input and output relates to the prefix:
2 :: (σ) → (σ, int) + :: (σ, int, int) → (σ, int)
This is exactly like the symbol stack pre- and post-conditions in stack graphs!
And the prefix variables are just like the globs in a Swanson environment type!
Mihelic2021 is a good rendering of the operational semantics of a stack-based language.
Pestov2010 describes Factor, which introduces checked stack effect annotations as a means of adding types to stack-based programs.
Diggins has two unpublished papers that describe the type system of Cat, which inspired how Factor _checks_ the stack effect annotations in a program, instead of treating them as unchecked documentation like in Forth.