talk-perth-fp-meetup-2020-07-13.md

---

title: Function all the way down. Programming in λ calculus. author: Andrea Bedini ...

Hello

• @andreabedini (GitHub ✅, Facebook ✗, Twitter ✗)
• Data Scientist @Fortescue by day
• Programming languages nerd

. . .

tl;dr

What if I told you you don't need data but just functions?

. . .

Today

• λ-calculus
• Encoding data types
• Recusive data types
• Pattern matching

λ-calculus

• Smallest Turing-complete language
• ~2 yr older than the Turing machine itself
• One of the original three models of computation

Syntax fits half of a slide

• 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

What is data

Algebraic data types.

data Boolean     = True | False
data PairInt     = MkPairInt int int
data MaybeInt    = JustInt Int | NoInt

. . .

also

data ListInt     = Cons int ListInt | Nil

Intuition with booleans

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.

. . .

if-then-else

var ifte = b => t => f => b(t)(f)

(b, a bool, is a function!)

How about pairs?

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))

MaybeInt?

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)

How do we use a maybe?

+----------+----------------+----------+ | 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)

Recursive types (à la Church)

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")

Folds

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).

Checkpoint

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.

Recursive types (à la Scott)

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")

Take away

1. With a bit of work you can figure out the pattern and the general case
2. You don't need your favourite language to implement ADT or pattern-matching Implement them yourself with λ calculus (and watch your codebase burn)

References

• 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