What level of static typing can be added to a stack-based language? I know it's impossible to fully statically type some stack languages:
"string" 399 1 io.inputAsInt range loop swap end-loop # can't determine what'll be on the top of the stack until runtime
But is there some level of static typing that stack languages can have?
I said in the comments that I had some disagreement with the premise of the question, but let's dive into why that is. Fundamentally, I think a fully statically typed stack language is eminently possible, and all the trade-offs in doing that are relevant to other paradigms as well.
We can easily define a (non-trivial) sound static type system for the language in your example. One of the rules will be that the body of a loop must complete with the same stack type as it began. It will reject your program as badly-typed, and you'll need to change it. For other functions, it will simulate their stack effects in the obvious way, pushing and popping representations of types to a stack, and reject the program when the stack doesn't meet the function's requirement.
This is a sound static type system and checker. It will reject some programs that perhaps could have run, but that's what all sound static type checkers do. It will allow plenty of programs through, and maybe enough to be useful.
Perhaps we do want this program to run. We could extend the type system: the loop construct is deemed to produce a union type of all possible results¹, and now this program is accepted!
The next question, though, is what we can do after that if we continue the program. We know that what's on top is either an integer or a string, but not which; we should be able to call a function that accepts both of those (perhaps a print, or a rotation), we should be able to drop or duplicate it, and we should be able to push new values onto the stack on top of it.
We can't do anything that requires specifically an integer or specifically a string as an argument, but that's correct — the program would crash some of the time, and that's exactly what a static type system is there to save us from. The language could provide a construct for inspecting the dynamic type — an is-int returning a boolean perhaps, or a pattern-matching system branching on different types. That would be fine to do, and the type system can accommodate these extensions as well.
Perhaps this isn't the language you want to have, which is fine and reasonable, but it's still a stack-based language and it's fully typed. There's nothing particular to a stack language about the complications we're facing here — the sample program is no different to
x = 399
y = "string"
for i from 1 to io.inputAsInt:
x, y = y, x
We can't determine what type y is here either! A type system for this language would likely also reject the program, or leave us with a union type, and many of the same solutions apply. Just like the example program, this has clear semantics and could run safely to the end in an untyped model.
Now, there are some cases where stack-based languages really are a little different: where the stack is actually the material element. The obvious case is something like 1 io.inputAsInt range loop drop end-loop: we don't know which items are left afterwards, or whether it went off the stack. This program would also be rejected by the type system sketched above, probably even after the extension. Arguably, that's what you want a type system to do for you.
This though is exactly the same problem as running off the end of an array in a procedural language, and it also admits of similar fixes: stack types that incorporate the stack size, rejecting programs that don't validate the change they're going to make, bounded stacks, and so on. All of these tools are available to the language designer, and it's up to them which programs they want to eliminate and where they want to spend their complexity budget to ameliorate it. They also have plenty of options for filling in that lost expression space, like adding more compound types or reified stacks.
Most statically-typed concatenative languages do reject programs like that, at least by default, in favour of having explicit bounds on the stack transformation that a function can do. We can include in that category things like Java bytecode, which is typed and verified before it runs, as well as human-directed programming languages like Kitten. It's fine for a language to decide it wants an unsound type system instead that lets some of these cases through, and there are plenty of deliberately unsound languages in other paradigms too. The unsound system can still perform useful validations and be worthwhile.
For a short formal treatment of typing concatenative languages you can look at Robert Kleffner's thesis, which also points at earlier work on stack effects in Forth in particular.
¹ This is actually somewhat complicated to do precisely, since there is a dependency between the two types at the top (if one is a string, the other isn't), but it is resolvable, or we can just say the top two entries are typed int|string. It doesn't matter for the moment and so I'm going to ignore that.
I'll complement Michael's excellent answer with some examples from an existing stack-based compiled language Factor.
Factor has one primary type system: stack effects. A stack effect of a function describes how many items it consumes and/or produces on the stack. Every defined function in Factor is annotated with its stack effect, which is checked during compilation.
A typical function looks like this:
: add ( x y -- z )
<function-body> ;
This add function takes two items on the stack, and produces one.
As a more involved example, the following function loop takes a "quotation" (a statically checked lambda) and repeatedly runs the quotation until it produces an f (false value) on the top. Here, ... means that the function can consume any number of stack items in addition to the parameter pred, but the stack height of ... part must be preserved. In addition, the quotation parameter pred is also checked for its own stack effect at the call site.
: loop ( ... pred: ( ... -- ... ? ) -- ... )
<function-body> ;
One could add static typing on the stack items themselves on top of stack effect checking. Factor already has a rudimentary tool for basic typing of this kind, but it can be extended much further.
For example, the swap function (a primitive that swaps two top items) could be typed with two generic type parameters, like ( 't1 't2 -- 't2 't1 ).
For the loop above, one could impose an extra constraint on the ... part: if it consumes n items of type t1, t2, ..., tn respectively, it must output n items of the same types as well. This is analogous to "variadic generics" where the number of generic parameters itself can be generic over integers.
Without automatic union types (as Michael suggested), OP's program won't typecheck because 't1 't2 will be inferred to be int string and [int string] != [string int], which violates the expected ( ... -- ... ) type of loop body.
Other than stack effects and stack element type matching, there is nothing much different from non-stack languages in terms of typing, so you can employ pretty much any type system that works for you. This is also mentioned in Michael's answer, but to reiterate, ultimately there's no difference between trying to type
123 "abc" [ swap ] read-int times
in Factor and
a = 123
b = "abc"
n = int(input())
for _ in range(n):
a, b = b, a
in Python.
