title: Function all the way down. Programming in λ calculus. author: Andrea Bedini ...
- @andreabedini (GitHub ✅, Facebook ✗, Twitter ✗)
- Data Scientist @Fortescue by day
- Programming languages nerd
. . .
What if I told you you don't need data but just functions?
. . .
- λ-calculus
- Encoding data types
- Recusive data types
- Pattern matching
- Smallest Turing-complete language
- ~2 yr older than the Turing machine itself
- One of the original three models of computation
- variables:
x
- functions:
λx.M
(aka abstractions) - application:
M N
+-------------+-------------------+
| Examples | ... in Javascript |
+=============+===================+
| x
| x
|
| λx.x
| x => x
|
| (λx.x) y
| (x => x) y
|
| λx.λy.x
| x => y => x
|
| λx.λf.f x
| x => f => f(x)
|
+-------------+-------------------+
Note no constants! no data! just functions and variables.
Syntax warning Types in Haskel, values in Javascript
Algebraic data types.
data Boolean = True | False
data PairInt = MkPairInt int int
data MaybeInt = JustInt Int | NoInt
. . .
also
data ListInt = Cons int ListInt | Nil
data Boolean = True | False
A program taking a boolean as input is like two different programs: whenTrue
and whenFalse
.
var true = whenTrue => whenFalse => whenTrue
var false = whenTrue => whenFalse => whenFalse
. . .
More succintly
var true = t => f => t
var false = t => f => f
i.e. Tell me what you want to do with the bool, and I will pick the right thing to do.
. . .
var ifte = b => t => f => b(t)(f)
(b
, a bool, is a function!)
data PairInt = MkPairInt int int
We stores the two integers in a closure
var mkPairInt = a => b => f => f(a)(b)
i.e. Tell me what you want to do with a and b, and I'll give them to you.
var fst = p => p(a => b => a)
var snd = p => p(a => b => b)
. . .
bonus, swap function
var swap = p => mkPair(snd(p))(fst(p))
data MaybeInt = JustInt Int | NoInt
var noInt = j => n => n
var justInt = a => j => n => j(a)
. . .
a j n
^ ^ ^
| | |
| | +- second case
| +---- first case
+------- closure (only for first case)
+----------+----------------+----------+ | bool | true, false | ifte | | pairInt | mkPair | fst, snd | | maybeInt | noInt, justInt | ? | +----------+----------------+----------+
. . .
var's call it useMaybe
- a maybe
- a function to apply to
a
in the just case - the value to return in the nothing case
var useMaybe = m => j => n => m(j)(n)
var ifte = b => t => f => b(t)(f)
var useMaybe = m => j => n => m(j)(n)
but
var fst = p => p(a => b => a)
var snd = p => p(a => b => b)
. . .
perhaps we should say
var usePair = p => f => p(f)
var fst = p => usePair(a => b => a)
var snd = p => usePair(a => b => b)
var swap = p => usePair(a => b => mkPair(b)(a))
. . .
then we get
var useBool = b => t => f => b(t)(f)
var useMaybe = m => j => n => m(j)(n)
var usePair = p => f => f(p)
data ListInt = Cons Int ListInt | Nil
var nil = r => n => n
var cons = h => t => r => n => r(h)(t(r)(n)) // 🤯
. . .
h t r n
^ ^ ^ ^
| | | |
| | | + base case
| | +- recusive case
| +---- tail
+------- head
. . .
var useList = l => r => n => l(r)(n)
var sumList = l => useList(l)(h => t => h + t)(0)
var printList = l => useList(l)(h => t => `${h}:${t}`)("nil")
var useBool = b => t => f => b(t)(f)
var usePair = p => f => p(f)
var useMaybe = m => j => n => m(j)(n)
var useList = l => r => n => l(r)(n)
data Boolean = True | False
data PairInt = MkPairInt int int
data MaybeInt = JustInt int | NoInt
data ListInt = Cons int ListInt | Nil
foldBool :: a -> a -> Boolean -> a
foldPair :: (Int -> Int -> a) -> PairInt -> a
foldMaybeInt :: (Int -> a) -> a -> MaybeInt -> a
foldListInt :: (Int -> a -> a) -> a -> ListInt -> a
Church encodes types as their own fold function.
Closely related to Continuation-Passing Style (CPS).
This is awesome.
With only functions we can define all ADT and do arbitrary operations on them.
Even recusion happens magically.
. . .
Turns out that some (simple?) functions like tail
cannot implemented easily.
data ListInt = Cons Int ListInt | Nil
var nil = c => n => n
var cons = h => t => c => n => c(h)(t)
. . .
h t c n
^ ^ ^ ^
| | | |
| | | + nil case
| | +- cons case
| +---- tail
+------- head
. . .
var useList = l => c => n => l(c)(n)
This looks more like pattern matching.
var tail = l => useList(l)(h => t => t)(undefined)
Problem recusion is not magical anymore, you need to explictly handle it yourself.
var sumList = l => useList(l)(h => t => h + sumList(t))(0)
var printList = l => useList(l)(h => t => `${h}:${printList(t)}`)("nil")
- With a bit of work you can figure out the pattern and the general case
- You don't need your favourite language to implement ADT or pattern-matching Implement them yourself with λ calculus (and watch your codebase burn)
- Types and Programming Languages. Benjamin C. Pierce, MIT Press
- Haskell programming from first principles (AKA haskellbook). C. Allen, J. Moronuki. Lorepub.
- Comprehensive Encoding of Data Types and Algorithms in the λ-Calculus. J. Func. Prog. Jansen et al. (2010)
- Lambda calculus
- Church encoding
- Mogensen–Scott encoding