Fixing a very old bug

Two and a half years ago, Mackenzie Straight reported a bug: stack effect inference would hang when given the following input:

[ [ dup call ] dup call ]

Of course this code hangs when evaluated anyway, but one does not expect a type checker to hang when given a non-terminating program!

For a long time, I had no idea how to fix this issue, and such patterns never came up in real code anyway, so I put it aside. Until today, this was probably the oldest bug which is still open.

Well, now it is fixed!

Some background information first...

Factor's stack effect inference is the basis of the compiler, and a key optimization performed at the inference level is lifting quotations up to their call site. Most of the time this works great, however in the example is rewritten as [ dup call ] [ dup call ] call, then [ dup call ] dup call, and it loops from there. The rewrite system used by the compiler was potentially non-terminating! Calls to curry are rewritten in a similar way, and similar non-termination can occur.

Using the results proven in The Theory of Concatenative Combinators, we can write a turing-complete basis for Factor:

drop
over
curry
>r
r>
call

Using these six words, together with all quotations (recursively) built up from them, we can express any computable function.

This presents a major problem. Because all of these operations -- stack shuffling, calling of quotations, and partial application -- are partially evaluated during stack effect inference, this means that determination of the stack effect of an arbitrary Factor expression becomes equivalent to the halting problem.

In the end, the fix was simple. Stack effect inference just gives up if a quotation calls itself directly or indirectly. Since the set of child quotations nested in a given input quotation is finite, the process either terminates, or eventually gives up with an error:

( scratchpad ) [ [ dup call ] dup call ] infer.
Word: [ dup call ]
The quotation [ dup call ] calls itself.
Stack effect inference is undecidable when quotation-level recursion is permitted.
Nesting: { [ dup call ] }

In real code, we don't do combinatory-logic-style quotation-level recursion; we just define named recursive words. In any case, somebody who wants to write odd stuff like M and Y combinators in Factor will simply have to put up with slower performance because such code will run in the interpreter instead of compiling.

Christopher Diggins's Cat language doesn't suffer from this problem, because his stack effect inferencer is more sophisticated than mine; it supports parametric polymorphism and row types, so quotations don't have to lifted up to their call site in order to determine the stack effect of a combinator. However, when Chris goes on to implement compiler optimizations, he'll find that quotation lifting can bring a huge performance benefit, just like lambda lifting in functional languages. In this case, the non-termination of quotation lifting still has to be considered.