How far can you go with functions alone? Lambda calculus is Turing complete, so you should be able to do all the things you do in Python or C.
Here are some classical programming constructs written just as (lambda) functions.
I'll write definitions in Lambda Calculus, but also (sometimes) in Python and Haskell, so worry not if you don't know lambda calculus. Below is a little refresher, and a longer discussion and explanation is at the bottom of the article.
Lambda calculus is a formal system to express functions, in the programmer's familiar definition of function: via variable substitution.
When we write a function like:
def multiply(x, y):
return x*y
multiply x y = x * y
We know that when calling multiply(3, 4) the arguments 3 and 4 will be substituted
in place of x and y in the body of the function.
This is the multiply function in lambda calculus:
multiply := λx y. x * y
And this is how you'd call it:
multiply 3 4 (or, equivalently)
(λx y. x * y) 3 4
In lambda calculus, we define a function using λ followed by its arguments. The dot separates the arguments from the body of the function, and to apply a function we simply write the arguments afterwards. We might need parentheses, because conventionally the dot binds the entire expression to the right:
λx y. x * y 3 2
is very different from
(λx y. x * y) 3 2
In this example, I used *, which is not really a lambda calculus term. In fact,
we'll basically only have functions. We'll name those functions using := sometimes,
but the names are just shorthands for the full formula, and are not part of lambda
calculus itself. Sometimes I'll pretend to also have constants, such as 1, 2, etc.
Later, we'll define exactly how to give meaning to numbers and do math on them.
Throughout the article I'll use lambda calculus like some sort of programming language:
# this is a comment
# this is a definition
id := λx.x
# this is lambda application, sometimes I'll write out the steps below:
id 3
# this is actually
(λx.x) 3
# performing the substitution x = 3 yields 3.
3
# another example:
f := λx.x x
g := λz. f z
g id
(λz. f z) (λx.x)
(λz. f z) (λx.x)
f (λx.x)
(λx.x x) (λx.x)
(λx.x) (λx.x)
(λx.x)
# we're done. This is basically just id.
In this first example I'll dig deeper in the reasoning, since many tricks we're going to use will be first introduced here.
Let's start by encoding "pairs", like (1, 2). In a language like C, we could use "a struct or something" to express how the data is laid on disk. But there's no disk here: just functions at our disposal. What is a pair really? It might seem counterintuitive at first, but let's define a pair through its "API" (or rather, universal property):
A pair is some "object" for which two projections exist: In some weird pseudocode:
pair = [...] // we're trying to define this
a = first(pair) // these two functions must exist!
b = second(pair)
Anything worthy of being called a pair, in any language or context, must have some way of extracting the two elements inside the pair.
So, we have to come up with "a thing" and two functions which acts on that thing.
In lambda calculus (and this is where it gets tricky), the only "thing" we have is
functions (lambda terms). Our "pair" must be some sort of function, and two other functions will take
that function as input and do something to finally "return" our a and b.
Here are the code listings in Python, Haskell, and my brand of Lambda Calculus.
pair = lambda a, b: lambda c: c(a, b)
fst = lambda c: c(lambda a, _: a)
scd = lambda c: c(lambda _, b: b)
# longer, but equivalent, definitions without "lambda"
def pair_long(a, b):
def tmp(c):
return c(a, b)
return tmp
def fst_long(pair):
def proj1(a, b):
return a
return pair(proj1)
def scd_long(pair):
def proj2(a, b):
return b
return pair(proj2)
pair = \a b -> \c -> c a b
first = \c -> c (\a b -> a) -- or first c = c (\a b -> a)
second = \c -> c (\a b -> b) -- or second c = c (\a b -> b)
pair := λa b . λc. c a b
fst := λc . c (λ a b. a)
scd := λc . c (λ a b. b)
Our function pair takes two things a and b and creates a pair, which is a function
that simply takes another function and applies it to a and b. So our fst and scd
functions simply pick one of the two arguments. the λc . c at the start makes our
syntax look sort of familiar: this is what the evaluation looks like:
fst (pair 1 2)
# this reads as, in our lambda calculus:
(λc . c (λ a b. a)) ((\a b -> \c -> c a b)(1, 2))
# let's evaluate the "pair" bit:
(λc . c (λ a b. a)) (\c -> c 1 2))
# so our pair is now simply a function that takes another function
# and applies 1, 2 to it. Substituting in the fst bit:
(\c -> c 1 2) (λ a b. a)
(λ a b. a) 1 2
1
So, we have "sort of" encoded a pair, using a lambda which captures the two elements of the pair. This is how we'll encode state from now on. By saving constants in the parameters of a lambda function, you can encode any kind of struct. (Scott Encoding, more below)
In a classic "if (condition) then (a) else (b)" block in most programming languages, three things are needed: a condition for the if, something to execute (or return) in case the condition is true, and something to execute (or return) otherwise.
The way we created our fst and scd functions before might be useful here: we could define
if sort of like a pair (a, b), and use true to extract a, and false to get b.
The order of arguments will be a bit different, but the concept is essentially the same:
my_if = lambda c, a, b: c(a, b)
true = lambda a, _: a
false = lambda _, b: b
my_if = \c a b -> c a b
true = \a b -> a
false = \a b -> b
if := λc a b . c a b
true = λa b. a
false = λa b. b
if true 1 2
(λc a b . c a b) true 1 2
true 1 2
1
if false 1 2
(λc a b . c a b) false 1 2
false 1 2
2
Notice how the if is just gone. We could've used true and false directly if we needed.
What about not, and and or?
not := λf.λa b. f b a
and := λc q.λa b. c (q a b) b
or := λc q.λa b. c a (q a b)
not(true)
(λf.λa b. f b a) (λa b. a)
(λa b. (λa b. a) b a)
(λa b. b) # false
and true false
(λc q.λa b. c (q a b) b) (λa b. a) (λa b. b)
(λa b. (λa b. a) ((λa b. b) a b) b)
(λa b. (λa b. b) a b)
(λa b. b) # false again
Numbers in Church encoding are expressed as nested function application:
zero := λf.x. x
one := λf.x.f x
two := λf.x.f (f x)
zero = lambda f: lambda x: x
one = lambda f: lambda x: f(x)
two = lambda f: lambda x: f(f(x))
Or you could use the successor function, which given a number outputs the next number:
successor = lambda n: lambda f: lambda x: f(n(f)(x))
one = successor(zero)
two = successor(one)
Using the successor function we can define addition, which is just repeated "succession":
add = lambda m: lambda n: m(successor)(n)
You can materialize these results in Python by providing, for example, +1 as function and 0 as initial value:
def church_to_int(n):
return n(lambda x: x + 1)(0)
# Example: one + two
result = add(one)(two)
print(church_to_int(result))
This should print 3. Funnily, multiplication is simpler and can be expressed as
mul = lambda m: lambda n: m(n)
If you enjoyed this, you should explore the natural numbers game, the wiki page for church encoding, Mogensen-Scott encoding and This C compiler written as a single lambda function