blob: 3506d52836aea25c0f8a92d540e511481bfde6f6 (
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
67
68
69
|
---
title: How I learnt to love typed λ-calculus
subtitle: "**A NewCrafts 2025 Hands-On Lab**"
date: 2025-11-06
author:
- Arnaud Bailly
- Emmanuel Gaillot
---
## Introduction
> An experimental workshop to explore the computational foundation of the universe, and have fun
---
## λ-Calculus Syntax
A term from the λ-Calculus is either:
* A _Symbol_: `x`, `y`, `Foo`, `++`...
* An _Abstraction_: `(lam (x) x)`
* An _Application_: `(foo bar)`
## λ-Calculus Rules
Terms from the λ-Calculus can be _rewritten_ using various rules the two main ones being:
* α-renaming:
> `(lam (x) x)` ⟹ `(lam (y) y)`
* β-reduction:
> `((lam (x) body) term)` ⟹ `body[x ← term]`
## λ-Calculus Extensions
* Syntactic sugar:
* `(lam (x) (lam (y) y))` ⟹ `(lam (x y) y)`
* `((foo bar) baz)` ⟹ `(foo bar baz)`
* Local definitions: `(let ((id (lam (x) x))) (id foo))`
* Global definitions: `(def id (lam (x) x))`
## λ-Calculus Extensions
* Primitive data:
* booleans: `true`, `false`
* numbers: `12`, `0.27`
* strings: `"λ-calculus rocks"`
## Typed λ-Calculus
* The λ-Calculus is the favorite playground of type theorists
* There's a whole zoo of type systems we won't dive into (see you next year!)
* Search for _λ Cube_online...
* We'll introduce _Simply Typed λ-Calculus_ aka. $\lambda_{\rightarrow}$
## The Code
## Action
## Conclusion
|
