eighty-twenty

I’m running Debian testing, with gnome-flashback. At present, it has installed gnome-flashback 3.20.2-1 alongside gnome-settings-daemon 3.21.90-2.

Symptoms

By default, there are some problems:

• The “Displays” section of the config tool says only “Could not get screen information”. This prevents GUI access to a lot of functionality, including arrangement of multiple monitors.

• The brightness adjustment keys do not work.

The root of the problem is that the DBus interface org.gnome.Mutter.DisplayConfig changed between GNOME 3.20 and GNOME 3.21; the GetResources method produces an additional result in 3.21 that is not present in 3.20’s version of the same interface.¹

If you see messages similar to the following from stderr of gnome-settings-daemon at startup, you are suffering from this problem too:

(gnome-settings-daemon:7149): power-plugin-WARNING **: Could not create GnomeRRScreen: Method 'GetResources' returned type '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuud)ii)', but expected '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuudu)ii)'
(gnome-settings-daemon:7149): wacom-plugin-WARNING **: Failed to create GnomeRRScreen: Method 'GetResources' returned type '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuud)ii)', but expected '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuudu)ii)'
(gnome-settings-daemon:7149): color-plugin-WARNING **: failed to get screens: Method 'GetResources' returned type '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuud)ii)', but expected '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuudu)ii)'
(gnome-settings-daemon:7149): common-plugin-WARNING **: Failed to construct RR screen: Method 'GetResources' returned type '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuud)ii)', but expected '(ua(uxiiiiiuaua{sv})a(uxiausauaua{sv})a(uxuudu)ii)'

Fixing the problem

To fix the problem, I patched and rebuilt gnome-flashback with these commands:

sudo apt-get build-dep gnome-flashback
apt-get source gnome-flashback
wget "https://eighty-twenty.org/files/gnome-flashback-hack-20160918.patch"
patch -p0 < gnome-flashback-hack-20160918.patch
(cd gnome-flashback-3.20.2; fakeroot ./debian/rules binary)

After these steps, you should have a new gnome-flashback binary, gnome-flashback-3.20.2/gnome-flashback/gnome-flashback. You can now move the existing one out of the way and install it:

sudo mv /usr/bin/gnome-flashback /usr/bin/gnome-flashback-AS-INSTALLED
sudo cp gnome-flashback-3.20.2/gnome-flashback/gnome-flashback /usr/bin
sudo chown root:root /usr/bin/gnome-flashback

Now restart both gnome-flashback and gnome-settings-daemon. (You should arrange for gnome-flashback to be started after gnome-settings-daemon.)

You should no longer have the stderr output complaining about the RR screen DBus signatures, and both the “Displays” section of the config tool and the brightness keys should work.

This is the second part of a series of three articles on modelling actor-like systems^1 2 using PLT Redex.

• Part I: The Functional Fragment: ISWIM in Redex
• Part II: The Communicating Fragment: Actors in Redex
• Part III: Efficiency vs. Nondeterminism

Like the previous post, this post is written as a literate Racket source file, and is licensed CC-BY 4.0. You can download it and run it yourself.

The Communicating Fragment: Actors in Redex

Here, we build on the functional fragment language that we developed in Part I, adding communication primitives to it.

Here’s a little program in the extended language. It creates an initial configuration holding a “boot” actor, which spawns two more actors, which each send themselves a message:

(boot-actor (spawn (send (self) 0))
            (spawn (send (self) 0)))

Nondeterminism enters the mix in a big way at this point, even for such a small, simple program as this. The traces for this example show a lot of branching, and the more complex a program is, the more possible interleavings it will have:

Preliminaries

As before, we need the Racket #lang header, and we need to load Redex itself. Since we’re also making use of the model we developed last time, we load that too. It is contained in a file called redex-iswim.rkt in the same directory as this file.

#lang racket
(require redex)
(require "redex-iswim.rkt")

Syntax

We define our Actor language by extending the syntax of the plain ISWIM-like language we developed last time.

We add four new kinds of primitive expressions, one new primitive type, and a bunch of structure related to representing entire groups of actors syntactically.

A syntax extension is declared by invoking define-extended-language with the name of the extended language, ISWIM+Actors, and the name of the language to be extended, ISWIM, which was imported from redex-iswim.rkt above.

(define-extended-language ISWIM+Actors ISWIM

Expressions, Values, Process IDs and Contexts

Starting with the new expressions, we let actors send messages to peers with (send ...), receive messages sent to them by their peers with (receive), discover their own identities with (self), and spawn new actors with (spawn ...).

  (expr ....
        (send expr expr)   ;; sends the second arg to the first arg, a PID
        (receive)          ;; blocks, waiting for the next message
        (self)             ;; evaluates to the PID of the calling actor
        (spawn expr ...))  ;; spawns a new actor which performs the exprs.

Values in our extended language include all the values from before, namely numbers, strings, booleans and so on, plus the addition of Process IDs, PIDs.

  (value ....
         pid)

We choose to represent PIDs using symbols—variable names—since that way, we can use Redex’s built-in name-freshening machinery to guarantee that a newly-spawned actor receives a genuinely fresh PID that is shared by no other actor in the group.

  (pid variable-not-otherwise-mentioned)

Our evaluation contexts also need to be updated for the new syntax. Here, only send expressions involve evaluating subterms before being processed, so we have only a small change to make to the context nonterminal from ISWIM.

  (context ....
           (send context expr)
           (send pid context))

Writing it this way forces evaluation order in a send to be left-to-right, consistent with all the other syntactic forms in the language.

Configurations

The main difference between the reduction relation we’ll build and the one we built last time is that this one will operate on whole configurations of actors rather than on individual ISWIM expressions.

We introduce a new syntactic category, configuration, which represents a pair of a queue of messages yet to be delivered, and a process table.

  (configuration ((queued-message ...) (actor ...)))

A queued message is a pair of an ISWIM value and the PID that it is addressed to. (The => is punctuation which makes reading terms in interactive use easier.) I’ve chosen the convention of adding new entries at the right-hand end of the queue, and removing entries from the left-hand end.

  (queued-message (value => pid))

An entry in the process table, an actor, is a triple of the actor’s PID, its mailbox, and its current program state in the form of an expression in the extended ISWIM+Actors syntax. The mailbox is a queue of messages, keeping the same convention described above.

  (actor (pid : mailbox expr))
  (mailbox (value ...)))

We didn’t introduce any new binding constructs, so we don’t have to mention #:binding-forms like we did for ISWIM.

Operational Semantics

Reduction Rules

While Redex does offer extend-reduction-relation, it doesn’t work well for us here because we are going to be interpreting ISWIM’s notions of reduction with a new kind of context: with configurations carrying contexts instead of plain contexts alone.

Instead, we define a new reduction relation.

(define ISWIM+Actors-red
 (reduction-relation ISWIM+Actors

Our first rule, send, queues the message to be sent and the pid naming its target in the configuration’s buffer, and replaces the (send ...) expression with #t.

  (--> ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context (send pid value_0)))
         actor_1 ...))

       ((queued-message ... (value_0 => pid))
        (actor_0 ... (pid_1 : mailbox (in-hole context #t))
         actor_1 ...))

       send)

Notice the “actor_0 ...” and “actor_1 ...” subpatterns. These allow Redex to pick any actor that matches the rest of the pattern, nondeterministically. As we will see, such subpatterns also occur in each of the remaining rules.

After a send rule has placed a message addressed to some pid in the configuration’s buffer, the deliver rule then takes it, finds the actor named pid in the process table, and places the message in its mailbox. Everything else is left unchanged.

  (--> (((value_0 => pid) queued-message ...)
        (actor_0 ... (pid : (value_1 ...        ) expr) actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid : (value_1 ... value_0) expr) actor_1 ...))

       deliver)

But what if the addressee no longer exists? This can’t happen with this version of the language (see exercises), but could happen if we were to alter the language in one of any number of simple, harmless ways. The failed-delivery rule simply drops buffered messages in the case that the addressee is not in the process table.

  (--> (((value_0 => pid) queued-message ...) ((pid_0 : mailbox expr) ...))
       ((                 queued-message ...) ((pid_0 : mailbox expr) ...))
       (side-condition (not (memq (term pid) (term (pid_0 ...)))))
       failed-delivery)

The receive rule selects the next ready message from an actor’s mailbox. The way the rule is written, it is only applicable if the mailbox is nonempty. This automatically makes actors block if they invoke (receive) when they have empty mailboxes: their term is simply stuck until some matching message comes along.

  (--> ((queued-message ...)
        (actor_0 ... (pid :
                          (value_0 value_1 ...)
                          (in-hole context (receive)))
         actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid :
                          (        value_1 ...)
                          (in-hole context value_0  ))
         actor_1 ...))

       receive)

The self rule replaces occurrences of (self) that are (a) in some evaluation context that is in turn (b) in some actor that is in turn (c) in our global configuration. We know syntactically which actor it is that’s invoking (self) so it’s easy to choose which pid to replace (self) with.

  (--> ((queued-message ...)
        (actor_0 ... (pid : mailbox (in-hole context (self))) actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid : mailbox (in-hole context pid   )) actor_1 ...))

       self)

Finally, spawn is handled by allocating a fresh PID using Redex’s fresh side-condition and turning the exprs into a new actor alongside its parent.

Here I’ve chosen to replace the (spawn ...) expression with the new actor’s PID, but this isn’t absolutely necessary; something like #t would do.

  (--> ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context (spawn expr ...)))
         actor_1 ...))

       ((queued-message ...)
        (actor_0 ... (pid_1 : mailbox (in-hole context pid_new))
         actor_1 ... (pid_new : () (begin expr ...))))

       (fresh pid_new)
       spawn)

Finally, we copy the beta, delta, begin-one, begin-many, if-true, if-false and unfold rules from ISWIM verbatim.³ Because they’re exactly the same as before, I’ve omitted them from the write-up; they are, however, still in the program source code.

;; (ISWIM notions of reduction omitted from presentation)

Following these ISWIM notions of reduction, we define what the ==> shortcut arrow means. Here it’s expressed in terms of our configurations, not just in terms of context the way that plain ISWIM assigned meaning to it. This lets the plain ISWIM notions of reduction function in any reducible actor in the process table.

  with
  [(--> ((queued-message ...)
         (actor_0 ... (pid : mailbox (in-hole context A)) actor_1 ...))

        ((queued-message ...)
         (actor_0 ... (pid : mailbox (in-hole context B)) actor_1 ...)))

   (==> A B)]))

Metafunctions

The delta, subst-all and let metafunctions are identical to those presented last time, so I’ll omit them in this write-up. (They are in the source code, however.)

;; (Metafunctions `delta`, `subst-all` and `let` omitted)

However, for our new system we do need one new metafunction, boot-actor, which takes a sequence of exprs and places it in a starting configuration for the reduction relation to operate on.

(define-metafunction ISWIM+Actors
  boot-actor : expr ... -> configuration
  [(boot-actor expr ...) (() ((boot : () (begin expr ...))))])

Examples and Tests

As before, we put a few simple tests in a test submodule.

(module+ test

This checks that ISWIM reductions can happen in a running actor. The expected result (() ((boot : () 124))) is a configuration with an empty buffer and with one actor, whose PID is boot, with an empty mailbox and an expression that is a value 124.

  (test-->> ISWIM+Actors-red
            (term (boot-actor ((lambda (x) (+ x 1)) 123)))
            (term (() ((boot : () 124)))))

Here we test learning our own PID and sending a message to ourselves: the boot actor sends itself 123, receives it, and adds one to it.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (send (self) 123) (+ (receive) 1)))
            (term (() ((boot : () 124)))))

Here we check that let works as we expect.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) w)))
            (term (() ((boot : () boot)))))

Here we check spawning of multiple actors.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (spawn 1) (spawn 2)))
            (term (() ((boot : () pid_new1) (pid_new : () 1) (pid_new1 : () 2)))))

Here we check cross-actor message sending.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w 123)) (receive))))
            (term (() ((boot : () 123) (pid_new : () #t)))))

Here we check communication of PIDs, not just regular ISWIM values.

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w (self))) (receive))))
            (term (() ((boot : () pid_new) (pid_new : () #t)))))

Here we check recursion combined with message sending.

  (test-->> ISWIM+Actors-red
            (term (boot-actor
                   ((rec loop (lambda (count) (if (= count 0)
                                                  0
                                                  (begin (send (self) count)
                                                         (loop (- count 1)))))) 3)))
            (term (() ((boot : (3 2 1) 0)))))

Nondeterminism is very slow

Try the following command with this file loaded in DrRacket:

(traces ISWIM+Actors-red
        (term (boot-actor
               (spawn (send (self) 0))
               (spawn (send (self) 0)))))

Notice the large number of intermediate terms before the final answer is computed! There are many possible interleavings of execution of this little program, leading to a lot of nondeterminism.

The corresponding test takes a correspondingly long time to execute.

  (test-->> ISWIM+Actors-red

            (term (boot-actor
                   (spawn (send (self) 0))
                   (spawn (send (self) 0))))

            (term (() ((boot : () pid_new1)
                       (pid_new : (0) #t)
                       (pid_new1 : (0) #t))))))

Examples that are even slightly larger take a very, very long time to run. Here is an example I’ve commented out because of its prohibitive slowness.

  ;; (test-->> ISWIM+Actors-red
  ;;           (term (boot-actor
  ;;                  (let ((counter (self)))
  ;;                    (spawn (send counter 1)
  ;;                           (send counter 1)
  ;;                           (send counter 1)))
  ;;                  ((rec loop (lambda (count)
  ;;                               (loop (+ count (receive))))) 0)))
  ;;           (term ???))

What can we do about this slowness? Part III will look into some possibilities.

Conclusion

We have extended our model of an ISWIM-like language with Actor-style facilities including spawn, process IDs, and message sending and receiving. We kept the ISWIM notions of reduction, but placed them into a new kind of context: configurations. We also added new rules that act on configurations directly to perform the Actor-related effects that programs written in our language can now request. In Part III, we will explore ways of reducing inessential nondeterminism in order to gain efficiency.

Exercises

1. (Easy.) Alter the receive rule to nondeterministically choose any of the queued messages in the mailbox. This removes the axiom of ordered delivery from the model.

2. (Easy.) Add a rule called message-loss that nondeterministically leads to the loss of a sent message. From which queue did you choose to remove the message? What other possibilities exist? Can you make an analogy between the different queues in a configuration and the buffers and queues in your operating system kernel and in your Ethernet cards, your LAN switches, and your routers?

   Hint: Because making this change introduces nondeterminism, you will want to add additional possible outcomes to the test-->> forms in the test submodule.

3. (Easy.) Develop an argument for why programs written in our Actor language will never invoke the failed-delivery delivery rule. What assumptions do you need to make for your argument to hold?

4. (Medium.) Add support for a new (quit) expression that terminates the invoking actor and removes it from the process table.

5. (Hard.) Add a garbage-collection rule which removes “finished” actors from the configuration’s process table. When is an actor “finished”? Is there an appropriate syntactic criterion you can use to decide? Is your approach sound? Is it complete?

6. (Medium.) Add support for Erlang-style monitors (see also here) and exit-notification-messages.

References and Footnotes

This is the first part of a series of three articles on modelling actor-like systems,^1 2 similar to Erlang and to my own work on Syndicate, using PLT Redex, “a domain-specific language designed for specifying and debugging operational semantics.”

• Part I: The Functional Fragment: ISWIM in Redex
• Part II: The Communicating Fragment: Actors in Redex
• Part III: Efficiency vs. Nondeterminism

This post is written as a literate Racket source file, and is licensed CC-BY 4.0. You can download it and run it yourself.

The Functional Fragment: ISWIM in Redex

The Redex webpage promises:

Write down a grammar and the reduction rules, and PLT Redex allows you to interactively explore terms and to use randomized test generation to attempt to falsify properties of your semantics.

In this post, I’ll build a model of a simple “ISWIM”-style, lambda-calculus based functional programming language. In subsequent posts, I’ll extend this little model to build it into an Erlang-style actor system.

Here’s an example program in the language:

((rec loop (lambda (count)
             (if (= count 0)
                 nil
                 (cons count (loop (- count 1)))))) 3)

And here’s a screenshot of the Redex trace visualizer showing reductions of the program:

Preliminaries

ISWIM is a programming language gedankenexperiment invented by Peter Landin in his famous paper, “The Next 700 Programming Languages”.³ It is essentially a Scheme-like language; a fairly minimal extension of the lambda calculus.

Our model will be an ISWIM-like language supporting S-expressions, numbers, strings, and booleans.

First of all, we need the Racket #lang header:

#lang racket

Next, we load Redex.

(require redex)

Syntax

We begin by declaring the (S-expression-based) syntax we will use for programs written in our language.

(define-language ISWIM

Expressions, Values and Variables

Our first nonterminal is expr, syntax for expressions in our language. An expression can be any of the following options:

  (expr x                     ;; a variable reference
        value                 ;; a value (see below)
        (cons expr expr)      ;; the construction of a pair
        (expr expr ...)       ;; a function call
        (prim expr ...)       ;; a primitive operation call
        (begin expr ...)      ;; a sequence of expressions
        (if expr expr expr)   ;; a conditional
        (rec x expr))         ;; a recursive expression

Notice the lack of imperative constructions. When we get to Part II, we’ll add some imperative commands, like “send message”.

Despite this lack, we still let programs written in this language use begin, because it is more ISWIM-ish than specifically Actors-ish, and it will be useful later.⁴

Values, value, in our language can be any of the following:

  (value (lambda (x ...) expr ...) ;; a literal function
         number                    ;; a literal number
         string                    ;; a literal string
         boolean                   ;; a literal boolean
         nil                       ;; the special value `nil`
         (cons value value))       ;; a constructed pair of values

We’re playing an interesting trick here, letting the cons constructor serve as both an expression and as a value. Once both arguments to cons have been reduced to values, the whole piece of syntax represents the final pair.

We let the syntactic nonterminal x stand for variables in our language:

  (x variable-not-otherwise-mentioned)

Evaluation Contexts and Primitive Operators

Our model uses the idea of evaluation contexts invented by Felleisen et al. in 1986.^5 6 7 An evaluation context is a term with a hole in it. The hole is, roughly, the position in the term where some reduction can happen: where a redex is waiting to be reduced.

This definition of evaluation contexts forces evaluation of function arguments to happen in left-to-right order.

  (context hole
           (value ... context expr ...)
           (prim value ... context expr ...)
           (cons context expr)
           (cons value context)
           (begin context expr expr ...)
           (if context expr expr))

We define a small set of primitive operators for manipulating data in our language. Other operators can be added by extending the definition of the prim nonterminal and by adding clauses to the metafunction delta below.

  (prim + - = car cdr pair? null?)

Binding structure of the language

I first learned Redex by taking a course based on “Semantics Engineering with PLT Redex”.⁸ An important part of programming with Redex at the time was implementing substitution functions correctly, respecting the binding structure of the language. This was a difficult, error-prone and annoying part of using the system.

Since then, Paul Stansifer has completed his dissertation work,⁹ and as a result, Redex programmers can specify a language’s binding structure directly as part of the syntax, meaning that substitution and alpha-equivalence functions can be automatically produced by the system.

We no longer have to write substitution functions by hand!

Here, to make use of Paul’s work, we specify the binding structure for lambda and rec forms: the formal parameters to a function are bound in the function body, and the recursively-bound identifier is bound in the contained expression, respectively.

  #:binding-forms
  (lambda (x ...) expr #:refers-to (shadow x ...) ...)
  (rec x expr #:refers-to x))

The documentation for this neat feature is available here.

Operational Semantics

Reduction Rules

Our reduction relation will combine a notion of reduction, capturing the essence of each reduction rule, with use of the evaluation contexts we defined earlier. Roughly speaking, the way we use evaluation contexts makes a notion of reduction in every potentially-reducible position in a complex term, even though the notion of reduction is specified in terms of a particular redex and reduct isolated from their context.

(define ISWIM-red
  (reduction-relation ISWIM

The first notion of reduction is the beta rule, for function calls. We will see the definition of the subst-all metafunction below.

    (==> ((lambda (x ...) expr ...) value ...)
         (begin (subst-all expr (x ...) (value ...)) ...)
         beta)

Primitive operators are interpreted by delegating to the delta metafunction, also defined below.

    (==> (prim value ...)
         (delta prim (value ...))
         delta)

When only one expression remains in a begin expression, we should replace the begin with the expression.

    (==> (begin expr)
         expr
         begin-one)

If the first expression in a begin has been completely reduced (to a value), then discard the value, and move on to reducing the remaining expressions in the begin.

    (==> (begin value expr_0 expr ...)
         (begin expr_0 expr ...)
         begin-many)

If the test position in an if has reduced to #t (Scheme notation for “true”), then replace the whole if with just the “then”-part.

    (==> (if #t expr_0 expr_1)
         expr_0
         if-true)

Likewise with the “else” part, in case the test position reduced to #f (“false”).

    (==> (if #f expr_0 expr_1)
         expr_1
         if-false)

Recursive values, usually functions, are handled by unfolding them: replacing uses of the recursively-bound variable in the body with a copy of the whole recursive value itself.

    (==> (rec x expr)
         (substitute expr x (rec x expr))
         unfold)

This is the first use we’ve seen of the generic substitute metafunction that Redex provides for us when we specify binding structure in the way we did above.

Finally, we bring together the notions of reduction with the contexts, by introducing what Redex calls a shortcut. This little snippet of syntax gives meaning to the ==> arrow used above for the notions of reduction by relating it to an overall reduction arrow --> by placing the arguments to ==> in a particular context.

    with
    [(--> (in-hole context A) (in-hole context B))
     (==> A B)]))

Metafunctions

Our primitive operators are given meaning by the delta metafunction, which uses Redex’s ability to reach out to the host language, Racket, to actually perform computations on base data like numbers and strings.

Pairs and nil aren’t treated quite the same as numbers and strings, since instead of being underlying Racket values, our pairs are “stuck” terms with the cons constructor at the head of the term.

(define-metafunction ISWIM
  delta : prim (value ...) -> value
  [(delta + (number_0 number_1)) ,(+ (term number_0) (term number_1))]
  [(delta - (number_0 number_1)) ,(- (term number_0) (term number_1))]
  [(delta = (value_0 value_1)) ,(equal? (term value_0) (term value_1))]
  [(delta car ((cons value_0 value_1))) value_0]
  [(delta cdr ((cons value_0 value_1))) value_1]
  [(delta pair? ((cons value_0 value_1))) #t]
  [(delta pair? (value)) #f
   (side-condition (or (not (pair? (term value)))
                       (not (eq? (car (term value)) 'cons))))]
  [(delta null? (nil)) #t]
  [(delta null? (value)) #f
   (side-condition (not (eq? (term value) 'nil)))])

Substitution is taken care of us by the substitute metafunction, but we define subst-all here to perform many substitutions at once.

(define-metafunction ISWIM
  subst-all : expr (x ...) (value ...) -> expr
  [(subst-all expr () ()) expr]
  [(subst-all expr (x x_0 ...) (value value_0 ...))
   (subst-all (substitute expr x value) (x_0 ...) (value_0 ...))])

Finally, we build a kind of macro for our little language: the let form expands into a use of lambda.

(define-metafunction ISWIM
  let : ((x expr) ...) expr ... -> expr
  [(let ((x_0 expr_0) ...) expr_1 ...)
   ((lambda (x_0 ...) expr_1 ...) expr_0 ...)])

Examples and Tests

At last, we have all the pieces we need to try out our language!

If you’re following along in DrRacket, or have a graphical environment available, try the following expression in your REPL or IDE. It should open a window that lets you explore the reduction of the term that we saw at the beginning of this article:

(traces ISWIM-red
        (term ((rec loop (lambda (count)
                           (if (= count 0)
                               nil
                               (cons count (loop (- count 1)))))) 3)))

For noninteractive use such as test cases, Redex’s test-->> function takes a term, reduces it as far as it will go, and compares the result to another term.

Here we put a few simple unit tests in a test submodule, so that they can be run by either DrRacket or by raco test on the command-line.

(module+ test
  (test-equal (term (delta null? (nil))) (term #t))
  (test-->> ISWIM-red (term ((lambda (x) (+ x 1)) 123)) (term 124))
  (test-->> ISWIM-red (term (let ((x 123)) (+ x 1))) (term 124))
  (test-equal (term (delta = (1 2))) (term #f))
  (test-equal (term (delta + (1 2))) (term 3))
  (test-->> ISWIM-red (term (car (cons 1 (cons 2 nil)))) (term 1))

  (test-->> ISWIM-red
            (term ((rec loop (lambda (count)
                               (if (= count 0)
                                   nil
                                   (cons count (loop (- count 1)))))) 3))
            (term (cons 3 (cons 2 (cons 1 nil)))))
  )

Conclusion

We have built a model of a simple lambda-calculus based programming language. We used the idea of evaluation contexts to specify the evaluation order of arguments to a function and of subterms of a begin expression. In Part II, we’ll extend this language with some imperative actions, turning it into a model of Actors.

Exercises

1. (Trivial.) Add a new primitive operator, string-append, to the language.

2. (Easy.) By altering the definition of contexts, make the evaluation order of this language right-to-left instead of left-to-right.

3. (Medium-Hard.) What happens if we try to reduce a function call to a function with duplicate names for its formal parameters, such as ((lambda (x x) x) 1 2)? Why does this happen? Alter the model so that such terms become “stuck”.

   Hint: This is “Medium-Hard” rather than just “Medium” because you have to dig into exactly how Redex’s built-in substitution machinery works: the naive fix of a call to Racket’s check-duplicates as a side-condition doesn’t immediately work.

4. (Easy.) Prove that this model is deterministic (confluent):
   For all expressions e, e′, and e″, if e→e′ and e→e″ then e′=e″.

References and Footnotes

Both Racket’s object system and its (separate!) generic interface system offer single-dispatch object-oriented programming: the choice of method body to execute depends on the type of just one of the arguments given to the method, usually the first one.

In some cases, the first thing that a method will do is to decide what to do next based on the type of a second argument. This is called double dispatch, and it has a long history in object-oriented programming languages—at least as far back as the original Smalltalk.

As an example, consider implementing addition for classes representing numbers. A different method body would be needed for each pair of representations of numbers.

I stumbled across the need for something like this when implementing Operational Transformation (OT) for Racket. The macro operation-transformer in that code base is almost the double-dispatch macro from this post; the difference is that for operational transformation, the method concerned yields two results, and if the arguments are switched on the way in, they must be switched on the way out.

Basic Double Dispatch

Here’s a basic double-dispatch macro:

(define-syntax-rule (double-dispatch op (arg1 arg2) [pred? body ...] ...)
  (cond
    [(pred? arg2) body ...] ...
    [else (error 'op "Unimplemented for ~v and ~v" arg1 arg2)]))

It assumes that it will be used in a method where dispatch has already been done on arg1, and that the next step is to inspect arg2. It applies the pred?s in sequence until one of them answers true, and then evaluates the corresponding body. If none of the pred?s hold, it signals an error.

It’s often convenient to use it inside a class definition or generic interface implementation with the following macros, which simply define op to delegate immediately to double-dispatch. The first is to be used with Racket’s object system, where the first argument is bound implicitly to this and where predicates should use Racket’s is-a? function. The second is to be used with Racket’s generic interface system, where both arguments are explicitly specified and predicates are more general.

(define-syntax-rule (define/public/double-dispatch (op arg2) [class body ...] ...)
  (define/public (op arg2)
    (double-dispatch (lambda (a b) (send a op b)) (this arg2)
      [(lambda (v) (is-a? v class)) body ...] ...)))

(define-syntax-rule (define/double-dispatch (op arg1 arg2) [pred? body ...] ...)
  (define (op arg1 arg2)
    (double-dispatch op (arg1 arg2) [pred? body ...] ...)))

Commutative Double Dispatch

For commutative operations like addition, it’s common to see the same code appear for adding an A to a B as for adding a B to an A.

The next macro automatically flips its arguments and tries again to see if B’s method has support for A, if it can’t find support for B within A’s method. That way, code for combining B with A need only be supplied in one place. It uses a parameter to keep track of whether it’s currently trying out a flipped pair of arguments.

(define trying-flipped? (make-parameter #f))

(define-syntax-rule (commutative-double-dispatch op (arg1 arg2) [pred? body ...] ...)
  (cond
    [(pred? arg2) (parameterize ((trying-flipped? #f)) body ...)] ...
    [(trying-flipped?) (error 'op "Unimplemented for ~v and ~v" arg2 arg1)]
    [else (parameterize ((trying-flipped? #t)) (op arg2 arg1))]))

Writing a simple wrapper works well for using commutative-double-dispatch in a class definition:

(define-syntax-rule (define/public/commutative-double-dispatch (op arg2) [class body ...] ...)
  (define/public (op arg2)
    (commutative-double-dispatch (lambda (a b) (send a op b)) (this arg2)
      [(lambda (v) (is-a? v class)) body ...] ...)))

but a wrapper for use with the generic interface system needs to take care not to accidentally shadow the outer dispatch mechanism. This macro uses define/generic to make op* an alias of op that always does a full dispatch on its arguments:

(define-syntax-rule (define/commutative-double-dispatch (op arg1 arg2) [pred? body ...] ...)
  (begin (define/generic op* op)
         (define (op arg1 arg2)
           (commutative-double-dispatch op* (arg1 arg2) [pred? body ...] ...))))

Examples

Let’s see the system in operation! First, using Racket’s object system, and then using Racket’s generic interfaces.

Example Scenario

We will first define two types of value foo and bar, each responding to a single doubly-dispatched method, operator which produces results according to the following table:

     | foo | bar |
-----|-----|-----|
 foo | foo | bar |
 bar | bar | foo |
-----|-----|-----|

Then, we’ll extend the system to include a third type, zot, which yields a zot when combined with any of the three types.

Double Dispatch with Classes

(define foo%
  (class object%
    (super-new)
    (define/public/commutative-double-dispatch (operator other)
      [foo% (new foo%)]
      [bar% (new bar%)])))

(define bar%
  (class object%
    (super-new)
    (define/public/commutative-double-dispatch (operator other)
      [bar% (new foo%)])))

Some tests show that this is doing what we expect. Notice that we get the right result when the first operand is a bar% and the second a foo%, even though bar% only explicitly specified the case for when the second operand is also a bar%. This shows the automatic argument-flipping in operation.

(module+ test
  (require rackunit)
  (check-true (is-a? (send (new foo%) operator (new foo%)) foo%))
  (check-true (is-a? (send (new foo%) operator (new bar%)) bar%))
  (check-true (is-a? (send (new bar%) operator (new foo%)) bar%))
  (check-true (is-a? (send (new bar%) operator (new bar%)) foo%)))

Double Dispatch with Generic Interfaces

(define-generics operand
  (operator operand other))

(struct foo ()
  #:methods gen:operand
  [(define/commutative-double-dispatch (operator this other)
     [foo? (foo)]
     [bar? (bar)])])

(struct bar ()
  #:methods gen:operand
  [(define/commutative-double-dispatch (operator this other)
     [bar? (foo)])])

The tests show the same argument-flipping behavior as for the object system above.

(module+ test
  (require rackunit)
  (check-true (foo? (operator (foo) (foo))))
  (check-true (bar? (operator (foo) (bar))))
  (check-true (bar? (operator (bar) (foo))))
  (check-true (foo? (operator (bar) (bar)))))

Extending The Example

First, we implement and test class zot%…

(define zot%
  (class object%
    (super-new)
    (define/public/commutative-double-dispatch (operator other)
      [foo% (new zot%)]
      [bar% (new zot%)]
      [zot% (new zot%)])))

(module+ test
  (require rackunit)
  (check-true (is-a? (send (new foo%) operator (new zot%)) zot%))
  (check-true (is-a? (send (new bar%) operator (new zot%)) zot%))
  (check-true (is-a? (send (new zot%) operator (new foo%)) zot%))
  (check-true (is-a? (send (new zot%) operator (new bar%)) zot%))
  (check-true (is-a? (send (new zot%) operator (new zot%)) zot%)))

… and then implement and test struct zot.

(struct zot ()
  #:methods gen:operand
  [(define/commutative-double-dispatch (operator this other)
     [foo? (zot)]
     [bar? (zot)]
     [zot? (zot)])])

(module+ test
  (require rackunit)
  (check-true (zot? (operator (foo) (zot))))
  (check-true (zot? (operator (bar) (zot))))
  (check-true (zot? (operator (zot) (foo))))
  (check-true (zot? (operator (zot) (bar))))
  (check-true (zot? (operator (zot) (zot)))))

Conclusion

Double dispatch is a useful addition to the object-oriented programmer’s toolkit, and can be straightforwardly added to both of Racket’s object systems using its macro facility.

This post was written as executable, literate Racket. You can download the program from here.

Unix famously represents all content as byte sequences. This was a great step forward, offering a way of representing arbitrary information without forcing an interpretation on it.

However, it is not enough. Unix is an incomplete design. Supporting only byte sequences, and nothing else, has caused wasted effort, code duplication, and bugs.

Text is an obvious example of the problem

Consider just one data type: text. It has a zillion character sets and encoding schemes. Each application must decide, on its own, which encoding of which character set is being used for a given file.

When applications get this wrong, both obvious bugs like Mojibake and subtler flaws like the IDN homograph attack result.

Massive duplication of code and effort

Lack of system support for text yields massive code duplication. Rather than having a system-wide, comprehensive model of text representation, encoding, display, input, collation, and comparison, each programming language and application must fend for itself.

Because it is difficult and time consuming to properly handle text, developers tend to skimp on text support. Where a weakness is identified, it must be repaired in each application individually rather than at the system level. This is itself difficult and time consuming.

Inconsistent treatment

Finally, dealing only with byte sequences precludes consistent user interface design.

Consider a recent enhancement to Thunderbird, landing in version 45.0. Previously, when exporting an address book as CSV, only the “system character set” was supported. Now, the user must specify which character set and encoding is to be used:

The user cannot simply work with a file containing text; they must make a decision about which encoding to use. Woe betide them if they choose incorrectly.

A consistent approach would separate the question of text encodings entirely from application-specific UIs. System UI for transcoding would exist in one place, common to all applications.

User frustration

A tiny fraction of the frustration this kind of thing causes is recorded in Thunderbird’s bug 117236.

Notice that it took fourteen years to be fixed.

Ubiquitous problem

This Thunderbird change is just one example. Each and every application suffers the same problems, and must have its text support repaired, upgraded, and enhanced independently.

It’s not only a Unix problem. Windows and OS X are just as bad. They, too, offer no higher-level model than byte sequences to their applications. Even Android is a missed opportunity.

Learn from the past

Systems like Smalltalk, for all their flaws, offer a higher-level model to programmers and users alike. In many cases, the user never need learn about text encoding variations.

Instead, the system can separate text from its encoding.

Where encoding is relevant to the user, there can be a single place to work with it. Contrast this with the many places encoding leaks into application UIs today, just one of which is shown in the Thunderbird example above.

It’s not just text

Text is just one example. Pictures are another. You can probably think of more.

Our operating systems do not support sharing of high-level abstractions of data between documents or applications.

An operating system with a mechanism for doing so would take a great burden off both programmers and users.

Let’s start thinking about what a better modern operating system would look like.

Programming language designers often need to experiment with syntax for their new language features. When it comes to Javascript, we rely on language preprocessors, since altering a Javascript engine directly is out of the question if we want our experiments to escape the lab.

Ohm is “a library and domain-specific language for parsing and pattern matching.” In this post, I’m going to use it as a Javascript language preprocessor. I’ll build a simple compiler for ES5 extended with a new kind of for loop, using Ohm and the ES5 grammar included with it.

All the code in this post is available in a Github repo.

Our toy extension: “for five”

We will add a “for five” statement to ES5, which will let us write programs like this:

for five as x { console.log("We have had", x, "iterations so far"); }

The new construct simply runs its body five times in a row, binding a loop variable in the body. Running the program above through our compiler produces:

for (var x = 0; x < 5; x++) { console.log("We have had", x, "iterations so far"); }

Extending the ES5 grammar

We write our extension to the ES5 grammar in a new file for5.ohm as follows:

For5 <: ES5 {
  IterationStatement += for five as identifier Statement  -- for5_named

  five = "five" ~identifierPart
  as = "as" ~identifierPart

  keyword += five
           | as
}

Let’s take this a piece at a time. First of all, the declaration For5 <: ES5 tells Ohm that the new grammar should be called For5, and that it inherits from a grammar called ES5. Next,

  IterationStatement += for five as identifier Statement  -- for5_named

extends the existing ES5 grammar’s IterationStatement nonterminal with a new production that will be called IterationStatement_for5_named.

Finally, we define two new nonterminals as convenient shorthands for parsing the two new keywords, and augment the existing keyword definition:

five = "five" ~identifierPart
as = "as" ~identifierPart

keyword += five
         | as

There are three interesting points to be made about keywords:

• First of all, making something a keyword rules it out as an identifier. In our extended language, writing var five = 5 is a syntax error. Define new keywords with care!

• We make sure to reject input tokens that have our new keywords as a prefix by defining them as their literal text followed by anything that cannot be parsed as a part of an identifier, ~identifierPart. That way, the compiler doesn’t get confused by, say, fivetimes or five_more, which remain valid identifiers.

• By making sure to extend keyword, tooling such as syntax highlighters can automatically take advantage of our extension, if they are given our extended grammar.

Translating source code using the new grammar

First, require the ohm-js NPM module and its included ES5 grammar:

var ohm = require('ohm-js');
var ES5 = require('ohm-js/examples/ecmascript/es5.js');

Next, load our extended grammar from its definition in for5.ohm, and compile it. When we compile the grammar, we pass in a namespace that makes the ES5 grammar available under the name our grammar expects, ES5:

var grammarSource = fs.readFileSync(path.join(__dirname, 'for5.ohm')).toString();
var grammar = ohm.grammar(grammarSource, { ES5: ES5.grammar });

Finally, we define the translation from our extended language to plain ES5. To do this, we extend a semantic function, modifiedSource, adding a method for each new production rule. Ohm automatically uses defaults for rules not mentioned in our extension.

var semantics = grammar.extendSemantics(ES5.semantics);
semantics.extendAttribute('modifiedSource', {
  IterationStatement_for5_named: function(_for, _five, _as, id, body) {
    var c = id.asES5;
    return 'for (var '+c+' = 0; '+c+' < 5; '+c+'++) ' + body.asES5;
  }
});

Each parameter to the IterationStatement_for5_named method is a syntax tree node corresponding positionally to one of the tokens in the definition of the parsing rule. Accessing the asES5 attribute of a syntax tree node computes its translated source code. This is done with recursive calls to the modifiedSource attribute where required.

Our compiler is, at this point, complete. To use it, we need code to feed it input and print the results:

function compileExtendedSource(inputSource) {
  var parseResult = grammar.match(inputSource);
  if (parseResult.failed()) console.error(parseResult.message);
  return parseResult.succeeded() && semantics(parseResult).asES5;
}

That’s it!

> compileExtendedSource("for five as x { console.log(x); }");
'for (var x = 0; x < 5; x++) { console.log(x); }'

Discussion

This style of syntactic extension is quite coarse-grained: we must translate whole compilation units at once, and must specify our extensions separately from the code making use of them. There is no way of adding a local syntax extension scoped precisely to a block of code that needs it (known to Schemers as let-syntax). For Javascript, sweet.js offers a more Schemely style of syntax extension than the one explored in this post.

Mention of sweet.js leads me to the thorny topic of hygiene. Ohm is a parsing toolkit. It lets you define new concrete syntax, but doesn’t know anything about scope, or about how you intend to use identifiers. After all, it can be used for languages that don’t necessarily even have identifiers. So when we write extensions in the style I’ve presented here, we must write our translations carefully to avoid unwanted capture of identifiers. This is a tradeoff: the broad generality of Ohm’s parsing in exchange for less automation in identifier handling.

Ohm’s extensible grammars let us extend any part of the language, not just statements or expressions. We can specify new comment syntax, new string syntax, new formal argument list syntax, and so on. Because Ohm is based on parsing expression grammars, it offers scannerless parsing. Altering or extending a language’s lexical syntax is just as easy as altering its grammar.

Conclusion

We have defined an Ohm-based compiler for an extension to ES5 syntax, using only a few lines of code. Each new production rule requires, roughly, one line of grammar definition, and a short method defining its translation into simpler constructs.

You can try out this little compiler, and maybe experiment with your own extensions, by cloning its Github repo.

Joe Marshall recently measured alist vs hashtable lookup time for MIT/GNU Scheme. I thought I’d do the same for Racket.

I used a 64-bit build of Racket, version 6.3.0.3.

I ran some very quick-and-dirty informal experiments on my Acer C720 laptop, which is running a 64-bit Debian system and has 2GB RAM and a two-core Celeron 2955U at 1.40GHz.

I measured approximate alist and hash table performance for

• fixnum keys, using eq? as the lookup predicate (so assq, hasheq) (fixnum program)
• length-64 byte vector keys, using equal? as the lookup predicate (so assoc, hash) (byte-vector program)

Each chart below has four data series:

• probe/alist, average time taken to search for a key that is present in an alist
• probe/alist/missing, average time taken to search for a key that is not present in an alist
• probe/hasheq or probe/hash, average time taken to search for a key that is present in a hash table
• probe/hasheq/missing or probe/hasheq/missing, average time taken to search for a key that is not present in a hash table

Fixnum keys

Here are average timings for fixnum keys:

Things to note:

• Alists are here always faster than hasheq tables for 7 keys or fewer, whether the key is present or not.

• When the key is present in the lookup table, alists are on average faster up to around 14 keys or so.

Length-64 byte vector keys

Here are average timings for length-64 random byte vector keys:

Things to note:

• Alists are here always faster than hasheq tables for 4 keys or fewer, whether the key is present or not.

• When the key is present in the lookup table, alists are on average faster up to around 16 keys or so.

Conclusions

Alists will be faster when you have very few keys - for eq?, around seven or fewer, or for equal?, perhaps only as many as four, depending on the size of each key.

If you expect with high probability that a given key will be present in the table, the picture changes slightly: then, alists may be faster on average up to around perhaps fifteen keys. Specifics of the insertion order of your keys will naturally be very important in this case.

Resources

The programs I wrote:

• alisttest-fixnums.rkt
• alisttest-bytes-64.rkt

The data I collected:

• alisttest-fixnums.ods
• alisttest-bytes-64.ods

gRPC looks very interesting. From a quick browse of the site, it looks like it differs from CORBA primarily in that

• It is first-order.
• It eschews exceptions.
• It supports streaming requests and/or responses.

(That’s setting aside differences between protobufs and GIOP.)

It’s the first point that I think is likely to be the big win. Much of the complexity I saw with CORBA was to do with trying to pass object (i.e. service endpoint) references back and forth in a transparent way. Drop that misfeature, and everything from the IDL to the protocol to the frameworks to the error handling to the implementations of services themselves will be much simpler.

The way streaming is integrated is interesting too. There’s a clear separation between (finite) data, including lists/arrays, in the protobuf message-definition language, and (possibly non-finite) behavior in the gRPC service-definition language. Streams, being coinductive, fit naturally in the service-definition part.

From time to time, one stumbles across a website that has gone out of its way to make it difficult to save images displayed on the page. A common tactic is to disable right-click for the elements concerned.

The following bookmarklet is a simple workaround.

To use it,

1. drag it to your bookmarks bar
2. when you’re on a page that won’t let you right-click to save images, click the bookmarklet.
3. now, click on any image in the page to simply make your browser go directly to that image.
4. from here, you can use the browser’s “save” functionality directly.

From time to time, I make binary snapshot downloads of the RabbitMQ plugins that I have developed. You will be able to find the most recent downloads from this page. I sign the downloadable files with my public key.

• rabbit_presence_exchange-3.5.1-20150421.ez, the Presence Exchange plugin built for RabbitMQ 3.5.1 using Erlang R13B04. Signature here; source code here.

• rabbit_udp_exchange-3.5.1-20150421.ez, the UDP Exchange plugin built for RabbitMQ 3.5.1 using Erlang R13B04. Signature here; source code here.

Older builds for previous versions of RabbitMQ may be available but not linked above; check the directory itself for a full list.