This page is a work in progress. Here be dragons.

A concatenative program is a composition of functions over a stack: the meaning of a program is the composition of the meaning of its words, left to right. Because the stack is the only interface between words, typing it fully captures each word’s behavior. A word’s type is an arrow S -> S', and an expression f . g is well-typed only when f’s type is A -> B and g’s type is B -> C.

But what is a stack’s type? A stack type is either empty, or a type pushed onto a stack type. To type words generically, we extend this with row variables: type variables that range over entire stack types rather than individual values. A row variable names the portion of the stack a word doesn’t touch, the part it neither consumes nor produces.

Consider dup, which copies the top of the stack. A monomorphic type like Int -> Int Int only works when the stack has exactly one integer, since we can’t express that the rest of the stack passes unchanged without using row variables in this system.

The generic version needs to abstract over both the top element and the rest of the stack, with a type of forall r a. ..r a -> ..r a a, where r is a row variable. This can be read as “for any stack r and any type a, dup consumes a stack with a on top and produces one with a on top twice, leaving the rest of the stack r untouched.”

For brevity sake I will be omitting the forall part of the types I mention unless truly needed.

Now consider dip, which hides the top of the stack for a quotation. Its type is ..r a (..r -> ..s) -> ..s a which tells us the following things:

• dip is a higher-order combinator, since it takes an arrow type as a parameter.
• The quotation has a type of ..r -> ..s, which tells us that it changes the shape of the stack, but not how.
• The value a disappears from the stack while the quotation runs, then reappears on top afterwards. The type enforces this: a is absent from both sides of the arrow in the quotation’s type.