Practicing Functional Programming: Logic

Most of what I want to write about today can be found in Chapter 3 of An Introduction to Functional Programming Through Lambda Calculus, by Greg Michaelson. However, I'll be working through it with JavaScript to try and give it some tangible application.

Disclaimer: this isn't really a post for teaching you; it's a post for me to review what I've learned. If you see that I've made some sort of error, ping me on twitter.


To build a condition, you first need a basis for negotiating one value over the other. In my last post about vectors, I accomplished a similar task. Here's how I represented it in that post:

λx.λy.λf.((f x) y)

As it turns out, a two dimensional vector has a lot in common with a conditional. If we rewrite it a bit (taken from the book):

def cond = λexpression1.λexpression2.λcond.((cond expression1) expression2)

NOTE: that bound values are at work here. The first occurrence of cond (before the =) is a shortcut name for the whole expression. The second occurrence of cond (next to the λ) binds a value to the name inside the function body.

The first two functions take the expressions that we hope to operate on, leaving us with:

λcond.((cond expression1) expression2)

Let's examine this function for a moment and try to suss out what kind of expression would be suitable input (cond) for this expression. cond is applied to expression1, and the result of that is applied to expression2:


This seems like a solid start. It is quite close to the ternary operator (commonly ?: in C style languages). Given a boolean value, choose the left expression or the right expression. So this means the body of our cond will have to negotiate one value over another. The ternary operator is a great source of inspiration, with many similarities to how I represented choosing a vector's X or Y value, respectively. Given two options, we can arbitrarily return one of them. From this, we can extract a definition for true and false:

def true = λexpression1.λexpression2.expression1
def false = λexpression1.λexpression2.expression2

So let's put this together in JavaScript:

const TRUE = x => y => x;
const FALSE = x => y => y;
const COND = x => y => cond => cond(x)(y);

And here's an example of how you'd be able to use this:

COND(1)(2)(TRUE); // returns 1
COND(1)(2)(FALSE); // returns 2

Given a selector, we can choose one expression over another.

NOT Operation

It may seem trivial, but we can learn a lot about how to implement the NOT operation through a truth table.

X     | RESULT

We can see that this is essentially the opposite of a conditional, X ? FALSE : TRUE. Although, it's a tad strange because we use cond to do the opposite of what it would normally do. Let's take a look at something kind of redundant:

((cond true) false)

This is the same thing as cond, right? Apply it to true or false and you get the same value out.

(((cond true) false) true) => true
(((cond true) false) false) => false

In JavaScript you might execute these statements:

COND(TRUE)(FALSE)(TRUE)(1)(2)  // returns 1
COND(TRUE)(FALSE)(FALSE)(1)(2) // returns 2

So if we want to define not, it'll just be the opposite:

def not = λx.(((cond false) true) x)

To depart from an accurate deconstruction of this expression, for a moment, I'd like to share my simplified understanding. We can examine a portion of this function body, ((cond false) true). This leaves us with a simple function that takes the input and returns the opposite. If the input is true, then it returns us the opposite. If you're still with me, I'm about to make a leap to simplify this definition a bit:

def not = ((cond false) true)

Based on our definition for cond above, we know that there are three functions involved. In this simplified definition for not we are applying the first two lambda expressions, which returns a function. There is probably a name for this kind of refactoring/simplification, but I don't know it yet.

Now let's whip up some JavaScript to bring it all together:

const NOT = x => COND(FALSE)(TRUE)(x);

Pretty straight forward, I think. However, the execution might throw you a curve ball. Here's an example of using it:

NOT(FALSE)       // returns a function.... wat?
NOT(FALSE)(1)    // still returns a function... wat?
NOT(FALSE)(1)(2) // returns 1!
NOT(TRUE)(1)(2)  // returns 2!

Okay, so the trick is that you're selecting an expression, not a value. Our definitions for TRUE and FALSE are selectors given two values. NOT is going to return a selector for the opposite value. Am I helping you understand this yet? The node.js REPL is a great place for trying this stuff out.

AND Operation

Once again, we'll start by examining a truth table. The thing I found surprising was just exactly how literally the truth table laid out the implementations for these logical operations.

X     | Y     | RESULT

When reading this truth table, consider that you'll want to capture that value in a λ function. By composing our λ functions we'll end up with an expression that perfectly represents this truth table. If you think back to short circuiting for a moment, you remember that the AND operation is only true if both values are true. That means half of the time we know the result just by examining the first expression alone.

def and = λx.λy.(((cond y) false) x)

This looks like a tangled mess, but bear with me. The Y value determines the value of the expression when X is true, and when X is false, we know the whole expression is false. We can simplify the expression a bit by walking through a substitution.

// here's our expression
((and true) false) ==
// replace "and" with its definition above
((λx.λy.(((cond y) false) x) true) false) =>
// substitute true for the first input of "and" (λx)
(λy.(((cond y) false) true) false) =>
// substitute false for the second input of "and" (λy)
(((cond false) false) true) =>
// evaluate cond (true ? false : false)

Let's try it again with different input.

// here's our expression
((and true) true) ==
// replace "and" with its definition above
((λx.λy.(((cond y) false) x) true) true) =>
// substitute true for the first input of "and" (λx)
((λy.(((cond y) false) true) true) =>
// substitute true for the second input of "and" (λy)
(((cond true) false) true) =>
// evaluate cond (true ? true : false)

Hopefully this helps clarify how this gets evaluated. The AND operation is a tad trickier than NOT. Let's take a look at some JavaScript examples.

const AND = x => y => COND(y)(FALSE)(x);

With this definition we can try and evaluate the above examples. Remember that you'll be getting back a function!

AND(FALSE)(FALSE)       // returns a function!
AND(FALSE)(FALSE)(1)(2) // returns 2
AND(FALSE)(TRUE)(1)(2)  // returns 2
AND(TRUE)(FALSE)(1)(2)  // returns 2
AND(TRUE)(TRUE)(1)(2)   // returns 1

OR Operation

Now we're starting to cruise. Again let's start with the truth table.

X     | Y     | RESULT

This table has two real cases. Either the first value is true, and we know the whole expression is true, or the first value is false and the value of the entire expression is equal to the second value. Given that, we can figure out the definition:

def or = λx.λy.(((cond true) x) y)

I'll leave the step-by-step evaluation for you to do. Instead I'll get right to the JavaScript version:

const OR = x => y => COND(TRUE)(x)(y);

And here's some examples of calling it:

OR(FALSE)(FALSE)       // returns a function!
OR(FALSE)(FALSE)(1)(2) // returns 2
OR(FALSE)(TRUE)(1)(2)  // returns 1
OR(TRUE)(FALSE)(1)(2)  // returns 1
OR(TRUE)(TRUE)(1)(1)   // returns 1


Now that we have some JavaScript and functions for doing logic, let's try something a bit more complicated:

const COND = x => y => cond => cond(x)(y);
const TRUE = x => y => x;
const FALSE = x => y => y;
const NOT = x => COND(FALSE)(TRUE)(x);
const AND = x => y => COND(y)(FALSE)(x);
const OR = x => y => COND(TRUE)(x)(y);

); // prints 2

); // prints 1


I hope that this has been helpful for you. I find it useful to try and apply this information by writing code. It helps to solidify my understanding. Chapter 3 has more information about representing natural numbers. I understood it pretty well, but I think I will write about it soon so that I can really grok it.

Show Comments