Donnerstag, September 17, 2009

Concatenative Programming via Rewriting in Scheme

The kernel of a concatenative programming language can be easily implemented using a rewriting system. As a proof-of-concept the presented implementation fully relies on Scheme's rewriting system at macro expand time! All one needs is define-syntax and -- in order to provide access to Scheme's built-in procedures -- a single defmacro.

(Apologies, if the formatting makes the code below hard to read. If you like to get the Scheme code, just drop me an email.)

Rewriting rules concerning the data stack (ds) are written as follows:

(rule swap : (@d ... snd fst) ==> (@d ... fst snd))
^^^^ ^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^
word datastack before datastack after

Note that the topmost element of the data stack is the rightmost element in the notation above.

Rewriting rules concerning the data _and_ the program stack (ps) are written as

(rule call : (@d ... (@q ...)) (@p ...) ==> (@d ...) (@q ... @p ...))
^^^^ ^^^^^^^^^^^^^^^^^ ^^^^^^^^ ^^^^^^^^ ^^^^^^^^^^^^^^^
word ds before ps before ds after ps after

Note that the topmost element of the program stack is the leftmost(!) element. Letting the data stack and the program stack "touch" their heads, makes it easier to describe the process when a word or quotation moves from the top of the program stack to the top of the data stack. The item just appears to move over to the other side.

Quotations are written as lists. The notation for patterns is according to the conventions for syntax-rules in Scheme. The use of a "@" in patterns has no special syntactic meaning, it's just a personal preference.

To run a concatenative program type

> (run () (2 3 plus))
^^ ^^^^^^^^^^
ds ps

If you type this in at the console, the result just shows the resulting data stack since the program stack is empty.

Here are some examples and their results (indicated by "-->"):

> (run (1 2) (3 4)) --> (1 2 3 4)
> (run () (2 1 swap dup 1 plus)) --> (1 2 3)
> (run (1 2) ((plus dup) call)) --> (3 3)
> (run () (4 5 1 2 eq (plus) (minus) ifte)) --> (-1)
> (run () (4 5 1 2 eq neg (plus) (minus) ifte)) --> (9)

This is the way, I implemented the rewriting system with Scheme macros only. I use PLT Scheme, choose language "Pretty Big".

First, we need to import "defmacro". In addition, we need a nice macro hack from Oleg Kiselyov, see "How to write symbol? with syntax-rules". We use it in the definition of 'run'.

(require mzlib/defmacro)

(define-syntax symbol??
(syntax-rules ()
((symbol?? (x . y) kt kf) kf) ; It's a pair, not a symbol
((symbol?? #(x ...) kt kf) kf) ; It's a vector, not a symbol
((symbol?? maybe-symbol kt kf)
(let-syntax
((test
(syntax-rules ()
((test maybe-symbol t f) t)
((test x t f) f))))
(test abracadabra kt kf)))))

The rule macro transforms rewrite rules into new macros. For example, the rule for 'swap'

(rule swap : (@d ... snd fst) ==> (@d ... fst snd))

creates the following new macro

((swap (@d ... snd fst) ps) (run (@d ... fst snd) ps))

That means, whenever an s-expression with 'swap' being leftmost is encountered, such like '(swap (1 2 3) (4 5))', the macro is applied. In the example, the result is '(run (1 3 2) (4 5))'.

(define-syntax rule
(syntax-rules (: ==>)
((_ word : (@d1 ...) ==> (@d2 ...))
(define-syntax word
(syntax-rules ()
((_ (@d1 ...) ps) (run (@d2 ...) ps)))))
((_ word : (@d1 ...) ==> (@d2 ...)
(@d3 ...) ==> (@d4 ...))
(define-syntax word
(syntax-rules ()
((_ (@d1 ...) ps) (run (@d2 ...) ps))
((_ (@d3 ...) ps) (run (@d4 ...) ps)))))
((_ word : (@d1 ...) (@p1 ...) ==> (@d2 ...) (@p2 ...))
(define-syntax word
(syntax-rules ()
((_ (@d1 ...) (@p1 ...)) (run (@d2 ...) (@p2 ...))))))
((_ word : (@d1 ...) (@p1 ...) ==> (@d2 ...) (@p2 ...)
(@d3 ...) (@p3 ...) ==> (@d4 ...) (@p4 ...))
(define-syntax word
(syntax-rules ()
((_ (@d1 ...) (@p1 ...)) (run (@d2 ...) (@p2 ...)))
((_ (@d3 ...) (@p3 ...)) (run (@d4 ...) (@p4 ...))))))
))

The run macro keeps the rewriting process running until the program stack is empty. The assumption is that there is a rewriting rule defined for symbols used on the program stack.

(define-syntax run
(syntax-rules ()
((run (@d ...) ()) ; we are done
'(@d ...))
((run (@d ...) (wrd @p ...)) ; inspect next wrd on program stack
(symbol?? wrd
(wrd (@d ...) (@p ...)) ; activate macro associated with wrd
(run (@d ... wrd) (@p ...)))))) ; move wrd on top of data stack

In order to have access to Scheme's built in procedures, we introduce a rewriting rule for a word called 'alien'. In Scheme, a procedure such as '+' can also be called using apply:

> (+ 2 3)
5
> (apply + '(2 3))
5

Thus, 'alien' expects the arguments and a symbol on top of the data stack, each wrapped in a quotation/list. To interact with Scheme, we need to use defmacro _alien.

(defmacro _alien (op q ds ps)
`(run (,@ds ,(apply (eval op) q)) ,ps))

(define-syntax alien
(syntax-rules ()
((_ (@d ... (@q ...) (op)) (@p ...))
(_alien op (@q ...) (@d ...) (@p ...)))))

Now let us define some rewriting rules:

(rule swap : (@d ... snd fst) ==> (@d ... fst snd))
(rule dup : (@d ... fst) ==> (@d ... fst fst))
(rule quote1 : (@d ... fst) ==> (@d ... (fst)))
(rule quote2 : (@d ... snd fst) ==> (@d ...(snd fst)))
(rule quote3 : (@d ... trd snd fst) ==> (@d ... (trd snd fst)))
(rule call : (@d ... (@q ...)) (@p ...) ==> (@d ...) (@q ... @p ...))
(rule ifte : (@d ... #f (@t ...) (@e ...)) (@p ...) ==> (@d ...) (@e ... @p ...)
(@d ... obj (@t ...) (@e ...)) (@p ...) ==> (@d ...) (@t ... @p ...))
(rule plus : (@d ...) (@p ...) ==> (@d ...) (quote2 (+) alien @p ...))
(rule minus : (@d ...) (@p ...) ==> (@d ...) (quote2 (-) alien @p ...))
(rule mult : (@d ...) (@p ...) ==> (@d ...) (quote2 (*) alien @p ...))
(rule div : (@d ...) (@p ...) ==> (@d ...) (quote2 (/) alien @p ...))
(rule eq : (@d ...) (@p ...) ==> (@d ...) (quote2 (eq?) alien @p ...))
(rule neg : (@d ... #f) ==> (@d ... #t)
(@d ... obj) ==> (@d ... #f))

And we are done ;-)

For information about concatenative languages, see concatenative.org.

Montag, September 14, 2009

Type Inference for "call" in Concatenative Languages

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:

@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 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:

@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 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.