Skip to content

Commit 50e7369

Browse files
committed
Add some slides
1 parent 5c6d80e commit 50e7369

2 files changed

Lines changed: 516 additions & 0 deletions

File tree

slides/slides.md

Lines changed: 375 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,375 @@
1+
---
2+
title: "Nette Effekte"
3+
sub_title: "(EPE Project, Marvin Borner)"
4+
date: ""
5+
theme:
6+
path: theme.yaml
7+
---
8+
9+
<!-- alignment: center -->
10+
<!-- jump_to_middle -->
11+
12+
`Nette Effekte` \
13+
(interaction net in effekt)
14+
15+
```
16+
╭─────╮
17+
╭─┴─╮ ╭─┴─╮
18+
│ ζ │ │ δ │
19+
╰┬─┬╯ ╰┬─┬╯
20+
│ ╰───╯ │
21+
╰───────╯
22+
```
23+
24+
<!-- end_slide -->
25+
26+
# why?
27+
28+
- literature often obscure => clean™ implementation
29+
- no online reducer for pure interaction combinators
30+
- especially with interaction calculus input
31+
32+
<!-- end_slide -->
33+
34+
# what?
35+
36+
<!-- column_layout: [5,1] -->
37+
38+
<!-- column: 0 -->
39+
40+
- `interaction combinators`: graph-based model of computation
41+
- web interface (elm-ish):
42+
- **parse** calculus
43+
- "**type-check**" etc.
44+
- **compile** to interaction calculus
45+
- **rule** stepper (by DSL)
46+
- interactive **force-directed** rendering
47+
48+
<!-- column: 1 -->
49+
50+
```
51+
╭─────╮
52+
╭─┴─╮ ╭─┴─╮
53+
│ ζ │ │ δ │
54+
╰┬─┬╯ ╰┬─┬╯
55+
│ ╰───╯ │
56+
╰───────╯
57+
```
58+
59+
<!-- end_slide -->
60+
61+
# effects
62+
## model
63+
64+
<!-- column_layout: [4,4] -->
65+
66+
<!-- column: 1 -->
67+
68+
```scala
69+
70+
71+
interface Model[C, O] {
72+
def render(): Unit / Redraw
73+
def stepReduction(): Unit / Redraw
74+
def stepAnimation(): Unit / Redraw
75+
def nextMode(): Unit / Redraw
76+
def source(s: String): Unit / Redraw
77+
def onContext(op: O): Unit / Redraw
78+
// partial redrawing!
79+
80+
def getMode(): Mode
81+
def getSource(mode: Mode): TextStream
82+
def getContext(): C
83+
def getErrors(): String
84+
}
85+
```
86+
87+
<!-- pause -->
88+
89+
<!-- column: 0 -->
90+
91+
```scala
92+
def dispatch(msg: Event): Unit / { Model[Canvas, CanvasOp], Redraw } =
93+
msg match {
94+
...
95+
case SetCanvasSize(v) =>
96+
do onContext(Size(v))
97+
case PanCanvas(v) =>
98+
do onContext(Pan(v))
99+
case ZoomCanvas(d) =>
100+
do onContext(Zoom(d))
101+
}
102+
```
103+
104+
<!-- end_slide -->
105+
106+
# effects
107+
## web model
108+
109+
```scala
110+
...
111+
div([
112+
OnDrag(box { v => PanCanvas(v) }),
113+
OnScroll(box { d => ZoomCanvas(d) })
114+
], ["right"], [
115+
canvas([
116+
OnResize(box { v => SetCanvasSize(v) }),
117+
OnTick(StepAnimation()),
118+
], ["inet"], do getContext())
119+
]),
120+
...
121+
```
122+
123+
<!-- end_slide -->
124+
125+
# effects
126+
## web pipeline from LC (roughly)
127+
128+
```scala {1|1-3|3-5|5-8|7-10|10-12|12-14|14-16|16-18}
129+
lc::parser::parse!() / { read[Char], emit[Term] } // parse to term
130+
-->
131+
lc::netter::net! / { read[Term], emit[Constructor] } // translate to IC constructors
132+
-->
133+
ic::ruler::redexes { / emit[Constructor] } / emit[Redex] // find redexes
134+
-->
135+
ic::ruler::step { / emit[Constructor], emit[Redex] } / {
136+
emit[Constructor], emit[Redex] } // apply one rule to some redex (+repeat)
137+
-->
138+
net::net! / { read[Constructor], NetStream } // to positioned nodes with explicit edges
139+
-->
140+
net::layout { / NetStream } / NetStream // single-step force-directed layout (+repeat)
141+
-->
142+
[frontend] { / NetStream } / Draw // convert to canvas elements
143+
-->
144+
ui::canvas::draw { / Draw }: Canvas // apply geometries to internal canvas structure
145+
-->
146+
ui::canvas::applyTo(canvas, node) // apply canvas to HTML node
147+
```
148+
149+
<!-- end_slide -->
150+
151+
# effects
152+
## force-directed layout Ⅰ
153+
154+
```scala
155+
interface Force {
156+
def origin(): Vector
157+
def strength(x: Double): Double
158+
}
159+
```
160+
161+
<!-- pause -->
162+
163+
```scala
164+
def force(f: Vector): Vector / Force =
165+
do origin() + f.normalize * do strength(f.magnitude)
166+
167+
def repulsion(from: Vector, position: Vector): Vector / Force =
168+
force(position - from)
169+
170+
def attraction(towards: Vector, position: Vector): Vector / Force =
171+
force(towards - position)
172+
```
173+
174+
<!-- end_slide -->
175+
176+
# effects
177+
## force-directed layout Ⅱ
178+
179+
```scala
180+
def centralGravitation(agent: Agent): Vector / Force =
181+
Vector(0.0, 0.0).attraction(agent.pos)
182+
183+
def coulombForce(agent: Agent) { agents: => Unit / AgentStream }: Vector / Force =
184+
with average
185+
with source[Vector] { agentPositions {agents} }
186+
with loop
187+
do emit(repulsion(do read[Vector], agent.pos))
188+
189+
def springForce(agent: Agent, length: Double) { net: => Unit / NetStream }: Vector / Force =
190+
with average
191+
with agent.wireForce(length) { agents{net} }
192+
agent.attachedWires { wires{net} }
193+
```
194+
195+
<!-- end_slide -->
196+
197+
# effects
198+
## catamorphism
199+
200+
<!-- column_layout: [4,3] -->
201+
202+
<!-- column: 0 -->
203+
204+
```scala
205+
def length(t: Term) =
206+
try t.cata
207+
with TermF[Int] {
208+
def sym(x) = resume(1)
209+
def abs(x, b) = resume(1 + b)
210+
def app(f, a) = resume(1 + f + a)
211+
}
212+
```
213+
214+
```scala
215+
def show(t: Term) =
216+
try t.cata
217+
with TermF[String] {
218+
def sym(x) = resume("${x}")
219+
def abs(x, b) = resume("λ${x}.${b}")
220+
def app(f, a) = resume("(${f} ${a})")
221+
}
222+
```
223+
224+
<!-- column: 1 -->
225+
226+
```scala
227+
def cata[A](t: Term): A / TermF[A] =
228+
t match {
229+
case Sym(x) =>
230+
do sym(x)
231+
case Abs(x, b) =>
232+
do abs(x, b.cata)
233+
case App(f, a) =>
234+
do app(f.cata, a.cata)
235+
}
236+
```
237+
238+
<!-- end_slide -->
239+
240+
# effects
241+
## compilation
242+
243+
<!-- column_layout: [3,2] -->
244+
245+
<!-- column: 0 -->
246+
247+
```scala
248+
try term.cata
249+
with TermF[Context] {
250+
...
251+
252+
def abs(x, b) = {
253+
val Context(bPort, bBinds) = b
254+
val kPort = do port("k")
255+
val xPort = bBinds.bind(x)
256+
do emit(Constructor(Port(kPort, Pos()), [
257+
Port(xPort, Pos()), Port(bPort, Neg())]))
258+
resume(Context(kPort, bBinds.delete(x)))
259+
}
260+
261+
...
262+
}
263+
```
264+
265+
<!-- column: 1 -->
266+
267+
```
268+
k
269+
┌┄┄┄┄┄┄┄│┄┄┄┄┄┄┄┄┄┄┄┐
270+
┊ ╭─┴─╮+ ┊
271+
┊ │ ζ │ ┊
272+
┊ +╰┬─┬╯- ┊
273+
⟦λx.b⟧ₖ = ┊ x╭─╯ ╰───╮b ┊
274+
┊ ┌─┴─┐ ┌┄┄┴┄┄┄┐ ┊
275+
┊ │ δ ╞══╡ ⟦M⟧₆ ┊ ┊
276+
┊ └───┘ └┄┄╥┄┄┄┘ ┊
277+
└┄┄┄┄┄┄┄┄┄┄┄┄║┄┄┄┄┄┄┘
278+
fv(λx.b)
279+
```
280+
281+
<!-- end_slide -->
282+
283+
# effects
284+
## other
285+
286+
- fresh ports
287+
- exceptions
288+
- lexing/parsing
289+
- net inspection
290+
- partial redrawing (+ tagging system)
291+
292+
<!-- end_slide -->
293+
294+
# problems
295+
296+
- records: `Agent(...) { .name = "foo" }`
297+
- memory leaks (browser OOM)
298+
- long compilation times
299+
- reification of streams with side effects (e.g. parsing)
300+
301+
<!-- end_slide -->
302+
303+
# stats
304+
305+
<!-- alignment: center -->
306+
307+
| **language** | **loc** |
308+
|---------------|---------|
309+
| effekt | 1700 |
310+
| js-web -O0 | 9500 |
311+
| js-web -O3 | 8300 |
312+
313+
<!-- end_slide -->
314+
315+
<!-- column_layout: [3,3] -->
316+
<!-- column: 0 -->
317+
318+
```
319+
ₚ┌┄┄┄┄┄┄┐
320+
⟦M⟧ = ◯──┤ ⟦M⟧ₚ ┊
321+
└┄┄┄┄┄┄┘
322+
323+
324+
325+
fv(M)
326+
┌┄┄┄┄┄┄┄┄║┄┄┄┄┄┄┐
327+
┊ ┌┄┄╨┄┄┄┐ ┊
328+
┊ ┊ ⟦M⟧ₘ ┊ ┊
329+
┊ └┄┄┬┄┄┄┘ ┊
330+
┊ │m ┊
331+
┊ ╭─┴─╮- ┊
332+
⟦M N⟧ₚ = ┊ │ ζ │ ┊ = m-(n-, p+)
333+
┊ -╰┬─┬╯+ ┊
334+
┊ n╭─╯ ╰─╮ ┊
335+
┊ ┌┄┄┴┄┄┄┐ │ ┊
336+
┊ ┊ ⟦N⟧ₙ ┊ │ ┊
337+
┊ └┄┄╥┄┄┄┘ │ ┊
338+
└┄┄┄┄┄║┄┄┄┄┄│┄┄┄┘
339+
fv(N) p
340+
```
341+
342+
<!-- column: 1 -->
343+
344+
```
345+
346+
347+
348+
p
349+
┌┄┄┄┄┄┄┄│┄┄┄┄┄┄┄┄┄┄┄┐
350+
┊ ╭─┴─╮+ ┊
351+
┊ │ ζ │ ┊
352+
┊ +╰┬─┬╯- ┊
353+
⟦λx.M⟧ₚ = ┊ x╭─╯ ╰───╮m ┊ = p+(x+, m-)
354+
┊ ┌─┴─┐ ┌┄┄┴┄┄┄┐ ┊
355+
┊ │ δ ╞══╡ ⟦M⟧ₘ ┊ ┊
356+
┊ └───┘ └┄┄╥┄┄┄┘ ┊
357+
└┄┄┄┄┄┄┄┄┄┄┄┄║┄┄┄┄┄┄┘
358+
fv(λx.M)
359+
```
360+
361+
<!-- end_slide -->
362+
363+
```
364+
f (Fix f) --- fmap (cata alg) ----> f a
365+
| |
366+
| |
367+
| |
368+
| |
369+
Fix alg
370+
| |
371+
| |
372+
| |
373+
v v
374+
Fix f ------- cata alg -------> a
375+
```

0 commit comments

Comments
 (0)