First let me introduce a notation for describing the effect of a word via substitutions. I use pattern matching. $X matches a single word, #X matches a single word _or_ quotation, and @X matches any number of words/quotations. To refer to a quotation, I use squared brackets. For example, "[ $X ]" matches a quotation with a single word inside like "[ 7 ]". Furthermore, I explicitly distinguish the data stack and the program stack and separate them with a bar "|". Here are some example substitutions:
@D #X | dup @P ==> @D #X #X | @P
@D #X #Y | swap @P ==> @D #Y #X | @P
$Y | + @P ==> @D $Z | @P
@D [ @X ] [ @Y ] | append @P ==> @D [ @X @Y ] | @P
As you can see, @D and @P explicitly catch the "rest" of the data stack and the program stack, respectively. The rules are precise specifications on the effects a word has on the data _and_ the program stack. Attachments like
The combination of a data and program stack represents a "continuation". A substitution rule substitutes a matching continuation by another continuation.
Since concatenative programs are written in continuation passing style, so to speak, we can decompose the substitution of a continuation @DS | @PS into ( @DS | @P ) | @S with @PS = @P @S, meaning that @P and @S stand for any decomposition of @PS. For example, the program "dup *" can be decomposed into "dup" and "*". Instead of evaluating ( @DS | dup * @R ) with some instance of a data stack @DS, we can also first evaluate ( @DS | dup ), which must result in an empty program stack and a data stack @DS', and then evaluate ( @DS' | * @R ). For this process, we also write ( @DS | dup ) | * @R.
Now we have everything in place to define the substitution rule for call:
@D [ @Q ] | call @P ==> ( @D | @Q ) | @P
The right hand side of the rule uses a continuation so that that further substitution rules for whatever is on @P can be applied and don't hinder stack effect inference.
Let's take the program "call +" as an example. To avoid naming conflicts in the following, we repeat the rules for "call" and "+" and rename some pattern variables.
(1) @D1 [ @Q ] | call @P1 ==> ( @D1 | @Q ) | @P1
(2) @D2 $X
$Y | + @P2 ==> @D2 $Z | @P2
The question to answer is:
(?) @D | call + @P ==> @D' | @P
Rule (1) applies:
@D | call + @P ==> ( @D1 | @Q ) | @P1
with @D = @D1 [ @Q ] and @P1 = + @P
==> ( @D1 | @Q ) | + @P
with @D = @D1 [ @Q ]
Rules (2) applies:
==> @D2 $Z
with @D = @D1 [ @Q ]
and @D2 $X
$Y = ( @D1 | @Q )
and @P = @P2
We can conclude that
@D1 [ @Q ] | call + @P ==> @D2 $Z
( @D1 | @Q ) ==> @D2 $X
We are done! The result says that "quote +" expects a quotation [ @Q ] at the very top of the data stack with @D1 underneath. The result will be a data stack with elements @D2 and an integer $Z
I don't find a way to express this any shorter. This is just the way it is. The example shows that type inference of "call +" is possible. Problems just occur if stack effect declarations (at least for the purpose of type inference) are limited to the data stack only. Consider Factor's stack effect declaration for call
call ( callable -- )
which does not capture the effect the created continuation has on the data stack.