[stack] concatenative lexically-scoped polymorphic mutable variables

Recently, I had been working on a problem in 5th. Because 5th is a  
linear language, it is impossible for any object to be referenced more  
than once (by definition). One problem this creates, amongst many, is  
that global variables cannot be efficiently implemented. The reason is  
that accessing a global variable either requires that it be copied,  
which may be expensive, or requires temporarily removing it, which is  
unsafe as an attempt to fetch it again before it is restored will  
cause an error. Neither is acceptable.

One way of solving this problem is to allow global variables to be  
removed, but to also keep track of this on the type level. This is  
implemented by passing an extensible record on top of the stack (or on  
the side of the stack -- whichever sounds nicer to you). A "push"  
function can be used to push an object into a particular "slot" in the  
record provided that the slot is currently empty. A "pull" function  
can be used to remove an object from a slot provided that the slot is  
currently full. These slots are polymorphic in the sense that objects  
of different types can inhabit the same slot at different times  
throughout the program.

If this is taken to its logical conclusion by allowing slots to hold  
multiple values, and by adding a bit of type system magic to ensure  
that only the most recently bound object in a slot can be manipulated  
until the point of the introduction of that pseudo-binding returns  
(which is doable), you end up with a type-safe form of dynamic  
scoping. This is not particularly interesting as I believe it is  
already well-known that dynamic scoping is compatible with  
concatenativity. (It may, however, be interesting that this is  
relatively easy to handle in terms of type inference.)

What is perhaps a new realization is that this approach gets you  
lexical scoping as well. This is doable by generating unique names for  
the lexical pseudo-variables in a particular definition. Because the  
names are unique, other functions will be unable to access the slots.  
5th's disallowing of recursive definitions is critical here as well as  
it prevents the slots from getting clobbered before the they are  
removed and discarded. Since the types of the slots are carried  
individually in the type system, mutating these slots can be done in a  
manner that is type-safe, even if the type associated with a  
particular slot changes within a definition.

In a non-linear variant of 5th, we could employ the same system but  
disallow updating or removing values from slots. This would give us  
variables that work as if they were implemented via substitution.  
However, substitution is not actually necessary as the fetching of a  
"variable" can be delayed until the function that fetches an object  
from a particular slot is called. Because substitution is avoided, the  
language remains a concatenative (albeit with rather fancy namespace  
control). The big bonus here is that you get a dual view of the  
semantics; you can look at it either from the perspective of term  
rewriting and substitution or via the perspective of function  
composition. This has led me to consider dropping linearity as this is  
just too pretty.

There are a few restrictions on all this. As already indicated, the  
language must not allow recursion. (Actually, tail recursion is  
allowable.) Additionally, the language must not have first class  
functions as the pseudo-variables cannot be closed over. Finally,  
special care must be taken for things like callback functions. In  
particular, the type system must ensure that the function given does  
not reference any slots meant to be used to emulate lexical scoping.  
This is straightforward to enforce.

This email is really about 10 pages shorter than it should be. If  
anyone managed to follow along, or would like clarification, I'd be  
happy to respond.

- John