Direkt zum Hauptbereich

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.

Beliebte Posts aus diesem Blog

Lidl und der Kassen-Bug

Es gibt Fehler, im Informatiker-Jargon "Bugs", die etwas anrühriges haben. Ich bat den Menschen an der Kasse bei Lidl um einen Moment Geduld und meine Kinder um Ruhe, um nicht den wunderbaren Moment zu verpassen, bei dem es passierte. Der Lidl-Mensch fluchte kurz auf -- und ich war entzückt! "Einen Moment, davon muss ich ein Foto machen!" Und dann machte ich noch eines. Ich bin heute extra für diesen Fehler zu Lidl gepilgert -- ich wollte es mit eigenen Augen sehen. Gestern hat mir ein Student (vielen Dank Herr Breyer) von diesem Fehler in einer EMail berichtet. Ein richtig schöner Fehler, ein Klassiker geradezu. Ein Fehler, den man selten zu Gesicht bekommt, so einer mit Museumswert. Dafür wäre ich sogar noch weiter gereist als bis zum nächsten Lidl. Der Fehler tritt auf, wenn Sie an der Kasse Waren im Wert von 0 Euro (Null Euro) bezahlen. Dann streikt das System. Die kurze Einkaufsliste dazu: Geben Sie zwei Pfandflaschen zurück und Lidl steht mit 50 Cent bei Ihne

Syntax und Semantik

Was ist Syntax, was ist Semantik? Diese zwei Begriffe beschäftigen mich immer wieder, siehe zum Beispiel auch " Uniform Syntax " (23. Feb. 2007). Beide Begriffe spielen eine entscheidende Rolle bei jeder Art von maschinell-verarbeitbarer Sprache. Vom Dritten im Bunde, der Pragmatik, will ich an dieser Stelle ganz absehen. Die Syntax bezieht sich auf die Form und die Struktur von Zeichen in einer Sprache, ohne auf die Bedeutung der verwendeten Zeichen in den Formen und Strukturen einzugehen. Syntaktisch korrekte Ausdrücke werden auch als "wohlgeformt" ( well-formed ) bezeichnet. Die Semantik befasst sich mit der Bedeutung syntaktisch korrekter Zeichenfolgen einer Sprache. Im Zusammenhang mit Programmiersprachen bedeutet Semantik die Beschreibung des Verhaltens, das mit einer Interpretation (Auslegung) eines syntaktisch korrekten Ausdrucks verbunden ist. [Die obigen Begriffserläuterungen sind angelehnt an das Buch von Kenneth Slonneger und Barry L. Kurtz: Formal Syn

Mit Prof. Handke im Gespräch: Vom Workbook zum Inverted Classroom

Aus dem Netz in Handkes Büro Es gibt diese schönen Momente, da führen soziale Medien zu sozialen Begegnungen im echten Leben. Ich twittere im Nachgang zur #BiDiWe16, ein Dialog mit Jürgen Handke ergibt sich, er schickt mir seine Telefonnummer, ich rufe sofort durch, wir verabreden uns. Drei Tage nach der #BiDiWe16 sitze ich bei Handke im Büro, das gleichzeitig sein beachtlich ausgestattetes Aufnahmestudio beherbergt. Es ist Freitagmorgen, 9. September 2016. Jürgen Handke ist mir kein Fremder. Ich habe zwei seiner ICM-Konferenzen besucht, auf der #BiDiWe16 in Berlin hielt er die Keynote. Er hat für seine Lehre Preise erhalten, zuletzt 2015 den Ars Legendi-Preis für exzellente Hochschullehre. Zugegeben, ich hadere mit dem Konzept des Inverted Classroom -- auch Flipped Classroom genannt. Meine Erfahrungen mit der Programmierausbildung von Informatik-Studierenden des 1. und 2. Semesters lassen mich zweifeln. Videos habe ich auch schon produziert, aber vor allem das selbstgesteuerte