From d101f88e6f21feff1716e7732ff63daa788b4385 Mon Sep 17 00:00:00 2001
From: Nicolas Lenz <nicolas@eisfunke.com>
Date: Thu, 26 Aug 2021 23:30:00 +0200
Subject: [PATCH] Formatting coaching
---
coaching/0-intro.md | 27 ++++++++++++----------
coaching/1-1-lambda.md | 51 +++++++++++++++++++++++-------------------
coaching/4-outro.md | 32 ++++++++++++++------------
3 files changed, 61 insertions(+), 49 deletions(-)
diff --git a/coaching/0-intro.md b/coaching/0-intro.md
index d7b7cbb..e93965d 100644
--- a/coaching/0-intro.md
+++ b/coaching/0-intro.md
@@ -2,16 +2,16 @@
## Kontakt
-Matrix: @eisfunke:eisfunke.com / https://matrix.to/#/@eisfunke:eisfunke.com
-EisfunkeLab-Chatgruppe auf Matrix: #lab:eisfunke.com / https://matrix.to/#/#lab:eisfunke.com
-Mail: nicolas.lenz@udo.edu
-Website: https://www.eisfunke.com
-EisfunkeLab-Newsletter: https://lab.eisfunke.com
-Bytegeschichten: https://bytegeschichten.eisfunke.com
-Meine FuPro-Folien: https://git.eisfunke.com/lab/fupro (vielleicht hilfreich für die Grundlagen)
+- Matrix: @eisfunke:eisfunke.com / https://matrix.to/#/@eisfunke:eisfunke.com
+- EisfunkeLab-Chatgruppe auf Matrix: #lab:eisfunke.com / https://matrix.to/#/#lab:eisfunke.com
+- Mail: nicolas.lenz@udo.edu
+- Website: https://www.eisfunke.com
+- EisfunkeLab-Newsletter: https://lab.eisfunke.com
+- Bytegeschichten: https://bytegeschichten.eisfunke.com
+- Meine FuPro-Folien: https://git.eisfunke.com/lab/fupro (vielleicht hilfreich für die Grundlagen)
+
+**Alles auch nochmal auf:** https://events.eisfunke.com/lab/cfupro21
-Alles auch nochmal auf:
-https://events.eisfunke.com/lab/cfupro21
## Plan
@@ -21,18 +21,21 @@ Drei Themenblöcke mit je drei Themen:
- Datentypen: Wie funktioniert das, Listen, Strings, Tupel, Zahlen, Booleans, Maybe, Either und Typvariablen
- Rekursive Funktionen, Pattern Matching, Bedingungen, wichtige Funktionen
+
- Typklassen, Kinds, higher-order functions
- Modellierung mit Datentypen
- Faltungen und Church-Kodierung
+
- Listenkomprehensionen
- Funktoren, Applikative, Monaden, Plusmonaden, bind- und do-Notation
- Wichtige Monaden: IO, Liste, Leser, Schreiber, Zustand, Zustandstransformer
+
## Zeitplan
-09:00 bis 12:00 Block 1 & 2
-12:00 bis 13:00 Mittagspause
-13:00 bis 15:00 Block 3
+- **09:00 bis 12:00:** Block 1 & 2
+- **12:00 bis 13:00:** Mittagspause
+- **13:00 bis 15:00:** Block 3
**Fragen? Gerne jederzeit!**
diff --git a/coaching/1-1-lambda.md b/coaching/1-1-lambda.md
index 247735f..9efb1c4 100644
--- a/coaching/1-1-lambda.md
+++ b/coaching/1-1-lambda.md
@@ -11,40 +11,38 @@ https://bytegeschichten.eisfunke.com/2021/08/17/bg006-lambda-kalkuel/
Die Definition von Lambda-Termen als Backus-Naur-Form:
-Term ::= x | (Term Term) | λx . Term (x steht für beliebige Variable)
+`Term ::= x | (Term Term) | λx . Term` (x steht für beliebige Variable)
Beispiele:
-- y
-- λz . (x y)
-- (λj . j j) z
- ~> z z
-- (λx . x) y
- ~> y
+- `y`
+- `λz . (x y)`
+- `(λj . j j) z ~> z z`
+- `(λx . x) y ~> y`
## β-Reduktion
Regeln der Beta-Reduktion:
-- (λx.P) Q -->β P[x:=Q]
+- `(λx.P) Q -->β P[x:=Q]`
-- P -->β P' ==> P Q -->β P' Q
+- `P -->β P' ==> P Q -->β P' Q`
-- Q -->β Q' ==> P Q -->β P Q'
+- `Q -->β Q' ==> P Q -->β P Q'`
-- P -->β P' ==> λx.P -->β λx.P'
+- `P -->β P' ==> λx.P -->β λx.P'`
Bedeutet letztendlich: Argumente in Lambda-Funktionen einsetzen
Wichtig: Verschattung
-- (λx.(λx.x)) y --->β λx.x
-- (λx.(λx.x)) y -/->β λx.y
+- `(λx.(λx.x)) y --->β λx.x`
+- `(λx.(λx.x)) y -/->β λx.y`
Wichtig: Umbenennung
-- (λx.(λy.x y)) y --->β λy.y' y
-- (λx.(λy.x y)) y -/->β λy.y y
+- `(λx.(λy.x y)) y --->β λy.y' y`
+- `(λx.(λy.x y)) y -/->β λy.y y`
@@ -52,28 +50,32 @@ Wichtig: Umbenennung
Die Idee:
-λx.x : c -> c
-λy.z : a -> b
+`λx.x : c -> c`
+`λy.z : a -> b`
Die drei Regeln:
+```
----------------------(var)
A ∪ {x : τ} |- x : τ
+```
-
+```
A |- M : σ → τ A |- N : σ
---------------------------------(app)
A |- (M N) : τ
+```
-
+```
A ∪ {x : σ} |- M : τ
----------------------(abs)
A |- λx.M : σ → τ
-
+```
Beispiel-Typableitungsbaum für λs . λz . s (s z):
+```
----------------------------------(var) ------------------------------(var)
{s : a -> a, z : a} |- s : a -> a {s : a -> a, z : a} |- z : a
----------------------------------(var) -------------------------------------------------------------------------(app)
@@ -84,22 +86,24 @@ Beispiel-Typableitungsbaum für λs . λz . s (s z):
{s : a -> a} |- \z . s (s z) : a -> a
-----------------------------------------(abs)
_ |- \s . \z . s (s z) : (a -> a) -> a -> a
+```
Beachten: Es kann mehrere gültig ableitbare Typen für einen Term geben!
-Z.B. \x.x : a -> a, aber auch \x.x : (a -> a) -> (a -> a)
+Z.B. `\x.x : a -> a`, aber auch `\x.x : (a -> a) -> (a -> a)`
Es gibt aber auch Terme und Kontexte, für die es keinen gültigen Typen gibt.
-Beispiel: λx.x x
+Beispiel: `λx.x x`
Tipp: Um Schreibarbeit zu sparen, Kontext getrennt definieren
-Sei K = {s : a -> a, z : ???}
+Sei `K = {s : a -> a, z : ???}`
Zunächst Baum von unten aus aufbauen und die Typen einfach leer lassen
Welche Regel eingesetzt werden muss und wie die Terme aussehen, ist immer eindeutig!
+```
...
-----------------(var) ---------------------(app)
K |- s : a -> a K |- s z : ???
@@ -109,6 +113,7 @@ Welche Regel eingesetzt werden muss und wie die Terme aussehen, ist immer eindeu
{s : a -> a} |- \z . s (s z) : ???
------------------------------------(abs)
_ |- \s . \z . s (s z) : ???
+```
Wenn der Baum fertig aufgebaut ist, Typen erst einsetzen.
diff --git a/coaching/4-outro.md b/coaching/4-outro.md
index e7c6751..444ab0f 100644
--- a/coaching/4-outro.md
+++ b/coaching/4-outro.md
@@ -14,32 +14,36 @@ Falls ihr Lust habt, schreibt mir gerne nach der Klausur mal, wie es gelaufen is
EisfunkeLab-Newsletter: lab.eisfunke.com
+
## Mich unterstützen
-Mehr davon, und noch viel mehr? Z.B. Haskell in der Praxis?
+Die Vorbereitung, das Coaching und die Nachbereitung des Materials hat mich viele Stunden Zeit
+gekostet, für die ich nicht bezahlt werde
+
+In Zukunft würde ich außerdem gerne mehr solche und ähnlicher Veranstaltungen machen!
Ihr könnt mir helfen mit Feedback, Werbung, Mitmachen oder natürlich mit...:
-Überweisung: Nicolas Lenz, IBAN: DE46 4306 0967 1089 7106 00, BIC: GENODEM1GLS
+**Überweisung:** Nicolas Lenz, IBAN: DE46 4306 0967 1089 7106 00, BIC: GENODEM1GLS \
(für mich gebührenfrei, nicht anonym, bevorzugt)
-PayPal: https://paypal.me/eisfunke
+**PayPal:** https://paypal.me/eisfunke \
(für mich gebührenfrei, nicht anonym)
-LiberaPay: https://liberapay.com/Eisfunke/
+**LiberaPay:** https://liberapay.com/Eisfunke/ \
(kostet mich Gebühren, anonym)
-Vielen Dank!
+**Vielen Dank!**
+
## Kontakt
-Matrix: @eisfunke:eisfunke.com / https://matrix.to/#/@eisfunke:eisfunke.com
-EisfunkeLab-Chatgruppe auf Matrix: #lab:eisfunke.com / https://matrix.to/#/#lab:eisfunke.com
-Mail: nicolas.lenz@udo.edu
-Website: https://www.eisfunke.com
-EisfunkeLab-Newsletter: https://lab.eisfunke.com
-Bytegeschichten: https://bytegeschichten.eisfunke.com
-Meine FuPro-Folien: https://git.eisfunke.com/lab/fupro
+- Matrix: @eisfunke:eisfunke.com / https://matrix.to/#/@eisfunke:eisfunke.com
+- EisfunkeLab-Chatgruppe auf Matrix: #lab:eisfunke.com / https://matrix.to/#/#lab:eisfunke.com
+- Mail: nicolas.lenz@udo.edu
+- Website: https://www.eisfunke.com
+- EisfunkeLab-Newsletter: https://lab.eisfunke.com
+- Bytegeschichten: https://bytegeschichten.eisfunke.com
+- Meine FuPro-Folien: https://git.eisfunke.com/lab/fupro (vielleicht hilfreich für die Grundlagen)
-Alles auch nochmal auf:
-https://events.eisfunke.com/lab/cfupro21
+**Alles auch nochmal auf:** https://events.eisfunke.com/lab/cfupro21
--
GitLab