summaryrefslogtreecommitdiffhomepage
path: root/slides
diff options
context:
space:
mode:
Diffstat (limited to 'slides')
-rw-r--r--slides/readme.md2
-rw-r--r--slides/slides.md692
2 files changed, 694 insertions, 0 deletions
diff --git a/slides/readme.md b/slides/readme.md
new file mode 100644
index 0000000..26ece5e
--- /dev/null
+++ b/slides/readme.md
@@ -0,0 +1,2 @@
+Uses Slidev, see [here](https://marvinborner.github.io/tuela24/1) for
+compiled version.
diff --git a/slides/slides.md b/slides/slides.md
new file mode 100644
index 0000000..d3732ee
--- /dev/null
+++ b/slides/slides.md
@@ -0,0 +1,692 @@
+---
+#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)