---
#theme: seriph
canvasWidth: 750
title: Really Functional Data Structures
author: Marvin Borner
colorSchema: light
class: text-center
transition: instant
mdc: true
# take snapshot for each slide in the overview
# overviewSnapshots: true
---
# *Really* Functional<br>Data Structures
[Marvin Borner](https://marvinborner.de)
<!--
Datenstrukturen nur aus Funktionen! Und wie man mit ihnen umgeht!
Frage: Erfahrung mit Lambdakalkül und Datenstrukturen?
Wieso, weshalb???
-->
---
# Goal/Motivation
<v-clicks>
- Represent arbitrary data using only functions
- No classes, structs, numbers, etc.
- Basically pure lambda calculus
- Think/program more functionally
- Elegant and minimal solutions
- Useful for theorem proving?
- Really fun!
</v-clicks>
<!--
- ..
- übertragbar
- e.g. easily typable
- ..
-->
---
# Anonymous Functions (Lambdas)
- Functions (abstractions) have an argument and a body
- Applying a function with an argument substitutes it
- Functions can be assigned to names (easier to read)
---
## JavaScript Notation
```js {monaco-run} {showOutputAt:1}
f = x => x + 42
console.log(f(2))
```
<div v-click=2>
```js {monaco-run} {showOutputAt:3}
f = x => y => x + y
console.log(f(2)(42))
```
</div>
---
# Really Functional Data Structures
<v-clicks>
- Only use pure, closed terms
- Multiple states are encoded via (unapplied) arguments and applications
- Carefully, such that data doesn't reduce itself!
- State can often be extracted using "selector" argument
</v-clicks>
<!--
Wie Daten rein funktional darstellen?
-->
---
layout: cover
---
# Common
---
# Boolean Logic
- **Capacity**: 1 Bit (true/false)
- **Operations**: and/not/etc.
<!--
mit was einfachem starten :)
-->
---
## Church Booleans
```js
tru = t => f => t
fls = t => f => f
```
---
## Church Booleans
```js {monaco-run} {showOutputAt:'+1'}
tru = t => f => t
fls = t => f => f
evalBool = bool => bool("true")("false")
console.log(evalBool(tru))
console.log(evalBool(fls))
```
---
## Example: Negation
<v-clicks>
- We know: `bool = t => f => t/f`
- If `bool = t => f => t`, then `!bool = t => f => f`
- If `bool = t => f => f`, then `!bool = t => f => t`
- Therefore:
``` js
negate = bool => t => f => bool(f)(t)
// ^ ^
// one will be eliminated!
```
</v-clicks>
---
## Example: Negation
```js {monaco-run} {showOutputAt:'+1'}
tru = t => f => t
fls = t => f => f
negate = bool => t => f => bool(f)(t)
evalBool = bool => bool("true")("false")
console.log(evalBool(negate(tru)))
console.log(evalBool(negate(fls)))
```
---
## Other Operators
- ``` js
and = a => b => b(a)(b)
```
- ``` js
xor = a => b => b(a(fls)(b))(a)
```
- ``` js
xnor = a => b => b(a)(a(b)(tru))
```
- ``` js
impl = a => b => a(b)(tru)
```
- ...
---
# Church Pairs
<v-clicks>
- Stores two values
- The selector function gets applied to both values:
``` js
examplePair = s => s(A)(B)
```
</v-clicks>
---
## Construction/Selection
```js {monaco-run} {showOutputAt:'+1'}
cons = a => b => s => s(a)(b)
car = pair => pair(a => b => a)
cdr = pair => pair(a => b => b)
// ^^^^^^^^^^^
// selector function
examplePair = cons("a")("b")
console.log(car(examplePair))
console.log(cdr(examplePair))
```
---
layout: cover
---
# Lists
---
# Church Lists
<v-clicks depth=2>
- Idea: A list is just a composition of pairs:<br>`[A, B, C, D] = (A, (B, (C, (D, NIL))))`
- But what is `NIL`?
- marks the end of the list
- differentiable from other elements
</v-clicks>
---
## `isNil`?
- We define NIL such that it *ignores* its selector argument
```js
cons = a => b => s => s(a)(b)
nil = s => x => x
exampleList = cons("a")(cons("b")(cons("c")(nil)))
// = s1 => s1("a")(s2 => s2("b")(s3 => s3("c")(nil)))
```
---
## `isNil`?
- We define NIL such that it *ignores* its selector argument
```js {monaco-run} {showOutputAt:'+1'}
cons = a => b => s => s(a)(b)
nil = s => x => x
exampleList = cons("a")(cons("b")(cons("c")(nil)))
// = s1 => s1("a")(s2 => s2("b")(s3 => s3("c")(nil)))
isNil = list => list(head => tail => right => fls)(tru)
// ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^
// cons/nil pair selector nil selector
console.log(evalBool(isNil(nil)))
console.log(evalBool(isNil(exampleList)))
```
---
## Example: Iteration
```js {monaco-run} {showOutputAt:'+1'}
y = f => x => f(y(f))(x)
exampleList = cons("a")(cons("b")(cons("c")(nil)))
length = y(rec => n => list => isNil(list)
(() => n)
(() => rec(n + 1)(cdr(list))()))
(0)
console.log(length(exampleList)())
```
---
# Other Lists
Example: Encoding of `["a", "b"]`
<v-clicks>
- Parigot:
```js
end => s1 => s2("a")(s2 => s2("b")(end))
```
- Scott:
```js
s1 => end1 => s1("a")(s2 => end2 => s2("b")(s3 => end3 => end3))
```
- $n$-Tuple:
```js
s => s("a")("b")...
```
</v-clicks>
<!--
Parigot: Triviales append
Scott: Kein wirklicher Sinn
n-Tupel: Vorteile siehe später, length/pop schwierig/unmöglich
-->
---
layout: cover
---
# Numbers
(brief overview)
---
# Church Numerals
- Idea: Represent a number $n$ by applying $n$ composed functions to some argument!
---
# Church Numerals
- Idea: Represent a number $n$ by applying $n$ composed functions to some argument!
- For example:
```js {monaco-run} {showOutputAt:'+1'}
three = s => z => s(s(s(z)))
evalChurch = n => n(x => x + 1)(0)
console.log(evalChurch(three))
```
---
## Successor
- Add another `s` to the composition
- We also need to "rebind" existing `s` and `z`!
---
## Successor
- Add another `s` to the composition
- We also need to "rebind" existing `s` and `z`!
```js {monaco-run} {showOutputAt:'+1'}
// three = s => z => s(s(s(z)))
zero = s => z => z
succ = n => s => z => s(n(s)(z))
console.log(evalChurch(succ(succ(succ(zero)))))
```
<!--
Predecessor really hard :(
-->
---
## `isZero`?
Similar to `isNil`!
```js {monaco-run} {showOutputAt:'+1'}
// three = s => z => s(s(s(z)))
isZero = n => n(z => fls)(tru)
console.log(evalBool(isZero(zero)))
console.log(evalBool(isZero(succ(zero))))
```
---
# Other Numeral Systems
Example: Encoding of $3$
<v-clicks>
- Scott:
```js
s1 => z1 => s1(s2 => z2 => s2(s3 => z3 => s3(s4 => z4 => z4)))
```
- Parigot:
```js
end => s1 => s1(s2 => s2(s3 => s3(s4 => end)))
```
- Mogensen:
```js
end => b1 => b0 => b1(b1(end)) // binary
end => tn => tp => t0 => t0(tp(end)) // balanced ternary
```
- Wadsworth, de Bruijn, Rationals, ...
</v-clicks>
<!--
Scott: Trivial pred, add komplexer
Parigot: pred/add beide in einem Schritt!
-->
---
layout: cover
---
# Algebraic Types
<!--
Wie man diese speichern kann
Typen haben wir natürlich nicht
-->
---
# Products/Records
- Stores multiple elements, supports construction and extraction
- For two elements: Just a Church pair
- For multiple elements: Extend the pair!
---
# Products/Records
- Stores multiple elements, supports construction and extraction
- For two elements: Just a Church pair
- For multiple elements: Extend the pair!
```js {monaco-run} {showOutputAt:'+1'}
// data Friends = Friends { best :: String, friendly :: String, weird :: String }
Friends = best => friendly => weird => s => s(best)(friendly)(weird)
best = friends => friends(best => _ => _ => best)
friendly = friends => friends(_ => friendly => _ => friendly)
weird = friends => friends(_ => _ => weird => weird)
friends = Friends("Alice")("Bob")("Carol")
console.log(best(friends))
```
---
# Sums/Unions
- Similar: Stores multiple *types*, but only one at a time
- Typical functional data structure (e.g. Haskell's `data` "|")
<!--
Selektion/etc. sehr ähnlich zu Produkttypen, nur mit *mehr* Selektoren!
-->
---
```js {monaco-run}
// data Tree = Leaf Int | Node Tree Tree
Leaf = n => leaf => node => leaf(n)
Node = a => b => leaf => node => node(a)(b)
nodeLeft = node => node(_ => _)(a => b => a)
nodeRight = node => node(_ => _)(a => b => b)
leafValue = leaf => leaf(n => n)(_ => _)
isLeaf = tree => tree(n => tru)(a => b => fls)
isNode = tree => tree(n => fls)(a => b => tru)
```
---
```js {monaco-run}
// data Tree = Leaf Int | Node Tree Tree
Leaf = n => leaf => node => leaf(n)
Node = a => b => leaf => node => node(a)(b)
nodeLeft = node => node(_ => _)(a => b => a)
nodeRight = node => node(_ => _)(a => b => b)
leafValue = leaf => leaf(n => n)(_ => _)
isLeaf = tree => tree(n => tru)(a => b => fls)
isNode = tree => tree(n => fls)(a => b => tru)
exampleTree = Node(Leaf(1))(Node(Leaf(2))(Leaf(3)))
console.log(evalBool(isNode(exampleTree)))
console.log(evalBool(isLeaf(nodeLeft(exampleTree))))
console.log(leafValue(nodeLeft(exampleTree)))
console.log(leafValue(nodeRight(nodeRight(exampleTree))))
```
---
layout: cover
---
# Trees
Trivial with presented data structures
- Rose trees
- Binary trees
- Finger trees
- Balanced trees
---
layout: cover
---
# Monads
---
# Maybe
Stores either nothing or a value, but *tagged*
```js {monaco-run} {showOutputAt:'+1'}
// data Maybe a = Nothing | Just a
Nothing = nothing => just => nothing
Just = v => nothing => just => just(v)
// instance Monad
pure = Just
bind = mx => f => mx(mx)(f)
// ------------^^ ^-----------------
// case Nothing case Just (apply)
evalMaybe = maybe => maybe("Nothing")(v => "Just " + v)
console.log(evalMaybe(bind(Nothing)(n => pure(n + 1))))
console.log(evalMaybe(bind(Just(42))(n => pure(n + 1))))
```
<!--
Basically just a tagged union... boring
-->
---
# Either
Stores either a value or another value, but *tagged*
```js {monaco-run} {showOutputAt:'+1'}
// data Either a b = Left a | Right b
Left = a => left => right => left(a)
Right = b => left => right => right(b)
// instance Monad
pure = Right
bind = mx => f => mx(Left)(f)
// ---------^^^^ ^------------------
// case Left case Right (apply)
evalEither = either => either(a => "Left " + a)(b => "Right " + b)
console.log(evalEither(bind(Left(42))(n => pure(n + 1))))
console.log(evalEither(bind(Right(42))(n => pure(n + 1))))
```
---
layout: cover
---
# Meta
(little detour)
---
# Mogensen-Scott
- Meta encoding of lambda terms
- Tagged union: `Symbol x | Application Term Term | Lambda Term`
- Translation:
```js
enc[x] = sym => app => lam => sym(x)
enc[f(x)] = sym => app => lam => app(enc[f])(enc[x])
enc[x => m] = sym => app => lam => lam(x => enc[m])
```
---
## Meta-Circular Interpreter
Evaluate lambda terms using the lambda implementation of the language itself!
```js
enc[x] = sym => app => lam => sym(x)
enc[f(x)] = sym => app => lam => app(enc[f])(enc[x])
enc[x => m] = sym => app => lam => lam(x => enc[m])
```
```js
eval = term => term
(x => x)
(f => x => eval(f)(eval(x)))
(m => x => eval(m(x)))
```
---
# de Bruijn-Church
- Idea: Encode symbols as Church-encoded de Bruijn indices
- Abstractions are simpler and allow open terms
- Translation:
```js
enc[i] = idx => app => lam => church[idx]
enc[f(x)] = idx => app => lam => app(enc[f])(enc[x])
enc[b] = idx => app => lam => lam(enc[b])
```
---
## 194 bit self interpreter
Minimal data structures allow minimal interpreters!
<style>
pre, code, pre * {
color: black !important;
background-color: transparent !important;
margin: 0 auto;
width: min-content;
font-size: 90%;
line-height: 1.1 !important;
}
small {
font-size: 50%;
}
</style>
```
01010001 00011100
11010000 ###### 11100110
10000 ############ 00001
01011 ##### ##### 00001
11100 #### #### 00101
01110 #### ##### 00011
00000 #### ###### 10100
00011 #### ### #### 00111
10000 #### ## #### 11111
00001 #### ### #### 11110
00010 ###### #### 11110
10011 ##### #### 10100
11110 #### #### 00011
11000 ##### ##### 00011
11000 ############ 01011
01101110 ###### 00011001
00011010 00011010
```
<small>
See [Metaprogramming and Self-Interpretation](https://text.marvinborner.de/2023-09-03-21.html)
</small>
<!--
Learning: minimale Datenstrukturen können zu minimalem Code führen!
-->
---
layout: cover
class: text-left
---
# Other Data?
- Strings? List of 2-ary numerals.
- Bits? List of Church booleans.
- Maps? Balanced tree with Church pairs.
---
layout: cover
---
# Images
---
# Quad Trees
- Leafs/pixels:
```js
black = w => b => b
white = w => b => w
```
- 4-tuple (product type):
```js
screen = s => s(TL)(TR)(BL)(BR)
```
- Where `TL`,`TR`,`BL`,`BR` are either a screen or a pixel
---
layout: cover
---
# Demo
[Lambda Screen](https://lambda-screen.marvinborner.de)