Short-Circuits in the Lambda Calculus

I recently gave a talk at Lambda Jam on building compilers/interpreters for a version of the lambda calculus extended with integers, booleans, if expressions, and binary arithmetic and relation operators. The list of binary operators included “or” and “and” for boolean values and of course this brought up the question of whether or not they do short-circuiting evaluation.

So what exactly is short-circuiting evaluation? Consider the expressions:

(let (x 1)
    (or (= x 1) (= x 2)))

This simple expression will return True is x is either 1 or 2, and False otherwise, but the idea of short-circuit evaluation is that the “or” operation should not evaluate it’s second argument if the first one returns True. This is because the expression (or True x) is always True, so there is no need to evaluate the x argument. In my implementation “or” and “and” do not perform short-circuit evaluation, as we can see if we print at different points in the evaluation.

(print
    (let (x 1)
        (or (print (= x 1))
            (print (= x 2)))))

This will prints: True False True.

Clearly this isn’t what we really want to happen, because if the second argument to or were a more complicated expression because it would waste a lot of time and processing power just to return an already evaluated True.

So how can we fix this? In my implementation there is one operator that already performs a sort of short-circuiting, the if expression. Consider the following code:

(let (x 1)
    (if (= x 1)
        (print (+ x 1))
        (print (- x 1))))

This expression just prints: 2. So how is short circuiting handled here, but not in the case of the “and” and “or” operators. The answer is that binary operations and if expressions are handled entirely differently by the CEK machine that evaluates expressions. In the case of is expressions it intentionally leaves code for the true and false branches unevaluated until after the condition has been evaluated, the way that this happens by building continuations is not important to understand why it behaves differently from the binary operations. In the case of binary operators such as “and” and “or”, all arguments are evaluated before the operation is applied, thus there is no opportunity for short-circuiting to occur.

How can we fix this? Desugaring. In many lisp or scheme like languages “or” and “and” are implemented as macros in order to deal with this short circuit evaluation, so how can a similar thing be done in our small extension of the lambda calculus.

Well we already have an if expression which can perform short circuit evaluation so consider the similarities between the following two snippets of code:

;; example with or
(let (x 1)
    (or (= x 1)
        (= x 2)))

;; short-circuiting with if
(let (x 1)
    (if (= x 1)
        (= x 1)
        (= x 2)))

Well that’s a little better, now the (= x 2) expression isn’t evaluated unless (= x 1) turns out to be false, but this still has a problem we evaluate the (= x 1) expression twice which is still wasteful.

We can fix that extra step of evaluation if we pull out the expression into a let so putting everything we’ve done so far together we finally have the following:

;; or desugaring
(or x y)
--->
(let (z x)
    (if z z y))

;; and desugaring
(and x y)
--->
(let (z x)
    (if z y z))

Taking this one step further, the core language implemented in my talk did not include let expressions, they were desugared in applications of lambda abstractions, so the final desugaring of these expressions will actually be

;; desugared or
(or x y)   --->   ((lambda z (if z z y)) x)

;; desugared and
(and x y)   --->   ((lambda z (if z y z)) x)

Thus as long as we have if expressions that correctly defer the evaluation of their arguments, then we can easily define the “or” and “and” operations without needing them to be built in as binary operations.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s