I think I solved the problem of type inference for "call" in concatenative languages. In a private mail, Slava Pestov (the creator of Factor) challenged me with the problem of inferring types for the bi and bi@ combinator. In essence, the problem boils down to "call". The solution, Christopher Diggins proposes in his papers on Cat is not without complications.
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:
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 are type annotations.
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:
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.
The question to answer is:
Rule (1) applies:
Rules (2) applies:
We can conclude that
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 on top. But there is a constraint which demands that the continuation ( @D1 | @Q ) returns a data stack with two integers on top and @D2 underneath.
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
which does not capture the effect the created continuation has on the data stack.
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
@D $X$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| @P2
with @D = @D1 [ @Q ]
and @D2 $X$Y = ( @D1 | @Q )
and @P = @P2
We can conclude that
@D1 [ @Q ] | call + @P ==> @D2 $Z| @P
with
( @D1 | @Q ) ==> @D2 $X$Y |
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.