blob: d568ace15cbd0bceef1ce1d05960da6d394a0711 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
# minilang
A minimal functional language to learn and experiment with type systems.
* http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf
* https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
* https://github.com/kino3/Mini-TT
# Agenda
## Notes
* How do we make a language?
* How do you make a baby?
* Things we use everyday but don't know how it works?
* Why?
* empower and free oneself
* Uxntal -> 100 rabbits
* How do I talk about my world/domain?
* would it not make sense to find better ways to express it?
* ensure code complexity does not map 1-1 with domain complexity
* What would it entail?
* reuse "simple" existing language focusing on _understanding_
* parser -> interpreter -> pretty-printer
* If I can make my own language, I can bring the language _where_ I
need it or want it to be
* starting point: how to talk to a machine?
## Plan A
* (5') Intro:
* How to talk to machines?
* not reinvent the wheel -> use existing knowledge
* Collective coding
* (5') play with parser/pretty-printer -> relate internal representation w/ external representation (human readable)
* representation for humans vs. for machines
* (45') focus on the interpreter
* introduce the rules of the λ-calculus
* implement evaluator
* use the leaderboard
* use the web UI for checking/troubleshooting
* (20') simply typed λ-calculus
* (5') type inference
* (5') Closing thoughts
* we'll be exchanging beers for knowledge
## Plan B
* (5') Intro:
* How to talk to machines?
* not reinvent the wheel -> use existing knowledge
* Collective coding
* (15-20') play with parser/pretty-printer/interpreter -> relate internal representation w/ external representation (human readable)
* representation for humans vs. for machines
* boolean algebra (together)
* (45') focus on the type-checker
* motivated by the fact it's easier to write with types
* simply typed version
* Problem: can we leverage the types to write stuff?
* need to modify evaluator to introduce primitive interpretation
* (10') type inference
* (10') Closing thoughts
* we'll be exchanging beers for knowledge
|
