Recently, I've been spending my free time learning functional programming. To understand comprehensively about functional programming, it is need to mention Lambda Calculus - a completed computation model for functional programming.
I am a developer and didn't have Lambda Calculus academic training, so at the beginning, I was very confused about some concepts. From my perspective, trying to implement it in a specific programming language makes it much easier to understand and explain to someone else. I chose Clojure for this purpose because it is a Lisp dialect language and has coherence and elegance of design.
This post just focuses on representing λ-calculus in Clojure. I suppose that you have basic knowledge about λ-calculus, if not, try to read Lambda Calculus theory or search on Wikipedia.
Some basic λ expressions
Function abstraction: All functions of the lambda calculus are anonymous and only take one parameter.
For example: λx.e
function accepts an argument x and returns the value of y. In Clojure, we'd write this as:
(fn [x] y)
Function application: (f e)
means the applied function f to e. It has a similar form in Clojure:
(f e)
Let's explore some other λ expressions:
-
λx.x
called the identity function.
(fn [x] x)
- Applied identity function above to
a
we have(λx.x a)
:
((fn [x] x) a)
-
(λ f. λ x. f x)
equivalent to:
(fn [f] (fn [x] (f x))
Function composition
This function takes 2 functions as arguments and returns a function that is the composition of those.
comp = λg. λf. λx. g (f x)
Now we'll write Clojure code to represent comp
function and define 2 functions add
and subtract
for testing. In Clojure:
(def comp
(fn [f g]
(fn [x] (f (g x)))))
(def add (fn [n] (+ n 2)))
(def subtract (fn [n] (- n 4)))
((comp add subtract) 8)
;; => 6
In the next part, I'll introduce Church encoding - a tool for representing numbers, booleans, conditionals, and data structures in Lambda Calculus
Church encoding
Church encoding, in Lambda calculus, is a way to encode data and operators using only a combination of anonymous functions.
Booleans
Let's define an abstraction for the booleans.
true = λx. λy. x
false = λx. λy. y
These functions receive two arguments and, If true
, the first argument is returned. If false
, the second argument is returned.
(def fst (fn [x y] x))
(def snd (fn [x y] y))
Pair
pair = λx. λy. λf. f xy
The pair function takes two arguments x and y and returns a function that contains x and y in its body.
In Clojure, this term is equivalent to:
(def pair (fn [x t]
(fn [func] (func x t))))
Given a pair, we can extract the first and second items using selection functions - these functions with similar form to boolean functions above.
Clojure code:
(def fst (fn [a b] a))
(def snd (fn [a b] b))
((pair 3 5) fst)) ;; => 3
((pair 3 5) snd)) ;; => 5
Numerals
A Church numeral applies its first argument to its second argument n times. For example, the definition of numbers from 0-3 in λ-Calculus:
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
In summary, the definition of the numeral n is the application of a given function f n times to a given value.
;; 0
(def zero (fn [f] (fn [x] x)))
;; 1
(def one (fn [f] (fn [x] (f x))))
;; 2
(def two (fn [f] (fn [x] (f (f x)))))
We can define a succ
function, which takes a Church numeral n and returns n + 1 by applying f to x one more time than the original number
succ = λn.λf.λx.f (n f x)
We'll try the function by applying function two
defined before and check the result:
(def succ (fn [n]
(fn [f]
(fn [x]
(f ((n f) x))))))
;; helper function to-int helps us check numerals
(def to-int (fn [n]
((n (fn [i]
(+ i 1))) 0)))
(to-int (succ two)) ;; => 3
(to-int (succ (succ two))) ;; => 4
There are more exercises in Church encoding, how to express conditional expressions, arithmetic operations, lists, etc and you can define them by yourself.
More resources
- Henri Borges'article Functions Describe the World
- Lambda calculus represented in both Clojure and Elixir: https://hungle00.github.io/content.html?id=15
- Matthew Might's work on FP and Lambda calculus is amazing.
Top comments (0)