Dear Factor-ians,
I think I solved the problem of type inference for "call" in concatenative
languages. In a private mail, Slava challenged me with the problem of
infering types for the bi and bi@ combinator. In essence, the problem boils
down to "call". The solution, Christopher Diggins proposes in his paper (see
http://www.cat-language.com/paper.html) 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:
@D #X | dup @P ==> @D #X #X | @P
@D #X #Y | swap @P ==> @D #Y #X | @P
@D $X<int> $Y<int> | + @P ==> @D $Z<int> | @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
<int> are type annotations.
The combincation 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<int> $Y<int> | + @P2 ==> @D2 $Z<int> | @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<int> | @P2
with @D = @D1 [ @Q ] and @D2 $X<int> $Y<int> = ( @D1 | @Q ) and @P = @P2
We can conclude that
@D1 [ @Q ] | call + @P ==> @D2 $Z<int> | @P
with
( @D1 | @Q ) ==> @D2 $X<int> $Y<int> | <empty>
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<int> 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
call ( callable -- )
which does not capture the effect the created continuation has on the data
stack.
Cheers,
Dominikus
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
Factor-talk mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/factor-talk
