diff --git a/slides/img/FILLCOMP.jpg b/slides/img/FILLCOMP.jpg new file mode 100644 index 0000000..47f2bd4 Binary files /dev/null and b/slides/img/FILLCOMP.jpg differ diff --git a/slides/img/FILLLEAVE.jpg b/slides/img/FILLLEAVE.jpg new file mode 100644 index 0000000..b4a0466 Binary files /dev/null and b/slides/img/FILLLEAVE.jpg differ diff --git a/slides/img/FILLPAIR.jpg b/slides/img/FILLPAIR.jpg new file mode 100644 index 0000000..1824668 Binary files /dev/null and b/slides/img/FILLPAIR.jpg differ diff --git a/slides/img/FROMA'.jpg b/slides/img/FROMA'.jpg new file mode 100644 index 0000000..62bdae3 Binary files /dev/null and b/slides/img/FROMA'.jpg differ diff --git a/slides/img/PATE.jpg b/slides/img/PATE.jpg new file mode 100644 index 0000000..41da8e8 Binary files /dev/null and b/slides/img/PATE.jpg differ diff --git a/slides/img/UPDA.jpg b/slides/img/UPDA.jpg new file mode 100644 index 0000000..78db16e Binary files /dev/null and b/slides/img/UPDA.jpg differ diff --git a/slides/img/linear_fails.jpg b/slides/img/linear_fails.jpg new file mode 100644 index 0000000..d2d4e7f Binary files /dev/null and b/slides/img/linear_fails.jpg differ diff --git a/slides/img/linear_works.jpg b/slides/img/linear_works.jpg new file mode 100644 index 0000000..cb89e8b Binary files /dev/null and b/slides/img/linear_works.jpg differ diff --git a/slides/img/map_dps.jpg b/slides/img/map_dps.jpg new file mode 100644 index 0000000..4eb7153 Binary files /dev/null and b/slides/img/map_dps.jpg differ diff --git a/slides/main.md b/slides/main.md index 8737ded..aa7d4c0 100644 --- a/slides/main.md +++ b/slides/main.md @@ -1,5 +1,4 @@ --- -theme: dracula paginate: true _paginate: false footer: Topics in Compilers and Concurrency ยท Julius Fischer ยท 10.06.2026 @@ -12,19 +11,24 @@ style: | right: 75px; } --- - -# Destination Calculus: -## A Linear ๐œ†-Calculus for Purely Functional Memory Writes -### Topics in Compiler and Concurrency -#### Julius Fischer - -###### 10. Juni 2026 $$ \def\leftcirc{{\triangleleft\kern-0.1em\circ}} \def\myor{{\;|\;}} +\def\dest{{\rightarrow}} +\def\lad{\lambda_d\;} +\newcommand{\htype}[1]{{\lfloor #1 \rfloor}} +\newcommand{\ampar}[3]{{\;_#1\langle #2 \;_{\tiny \land} \; #3 \rangle}} +\newcommand{\mapstom}[1]{{\sideset{_#1}{}\mapsto}} $$ +# Destination Calculus: +## A Linear ๐œ†-Calculus for Purely Functional Memory Writes +## Thomas Bagrel, Arnaud Spiwack +#### Topics in Compiler and Concurrency +#### Julius Fischer + +###### 10. Juni 2026 --- # What are Destinations? - Destination Passing Style @@ -77,7 +81,17 @@ map f (x:xs) dest = map f xs (push dest (f x)) - Purity --- -# Destination Calculus +# Destination Calculus: Terminology +- Holes +Values $h_1, h_2, \dots$ +- Destination +$\dest h_1 \dest h_2, \dots$ +- Ampars +$\ampar{H}{v_1}{v_2}$, i.e. $\ampar{{\{h\}}}{(h, 15)}{\dest h}$ +- $v_1$ "value with holes" +- $v_2$ "value of destinations" +--- +# Destination Calculus: Terms in $\lad$ - Basic FP terms $$ t, u := x \myor t' t \;|\; t ; t' \;|\; \dots @@ -86,8 +100,8 @@ $$ $$ \begin{align} \dots \myor - &case_m\;t\;of\;(v_1, v_2) \mapsto u \myor\\ - &case_m\;t\;of\;(Inl\;v_1) \mapsto u \myor \dots + &case\;t\;of\;(v_1, v_2) \mapsto u \myor\\ + &case\;t\;of\;(Inl\;v_1) \mapsto u \myor \dots \end{align} $$ - Additions for destination passing @@ -107,6 +121,68 @@ $$ t \triangleleft (,) \myor \dots \end{align} $$ +--- +# Destination Calculus: Constructors +- Usually constructors are required +$Inl, Inr, (a, b), \lambda x \mapsto t$ +- In $\lad$ we simply 'refine' holes +$Inl \; t \triangleq from_\ltimes' (upd_\ltimes\; new_\ltimes\; with \; d \mapsto d \triangleleft Inl \blacktriangleleft t)$ +$\lambda x \mapsto t \; \triangleq from_\ltimes' (upd_\ltimes\; new_\ltimes\; with \; d \mapsto d \triangleleft (\lambda x \mapsto t))$ --- -# Referenes +# Destination Calculus: Map example +![h:450](img/map_dps.jpg) +[1] Thomas Bagel + +--- +# Destination Calculus: Linearity and Modality +- Double writes are an issue + - If a hole is used more than once $(dest \blacktriangleleft v_1; dest \blacktriangleleft v_2; \dots)$ + - In types like $\htype{\htype{T}}$ +- Solved using modality of *Multiplicity* and *Age* +$m = p \cdot a$ +$p = 1 \myor \omega$ +$a =\; \uparrow^k \myor \infty$ for $k \in \mathbb{N}_0$ +- With $1 \underset{\raise{0.4em}{\leftarrow}}{<}^p \omega, \uparrow^k \underset{\raise{0.4em}{\leftarrow}}{<}^a \infty$ + +--- +# Destination Calculus: Linearity and Modality +- Add modalities to variable bindings +$$ +\begin{align} + \dots \myor + &case_m\;t\;of\;(v_1, v_2) \mapsto u \myor\\ + &case_m\;t\;of\;(Inl\;v_1) \mapsto u \myor\\ + &\lambda x\; \mapstom{m} \; t \myor \dots +\end{align} +$$ +- And add add exponential modality to weaken constraints +$$ +\begin{align} + \dots \myor + &Mod_m\; t \myor \dots +\end{align} +$$ + +--- +# Destination Calculus: Typing +- Mostly standard + +--- +# Referenes and Further Reading + +--- +# Extra Slides If needed + +--- + +# Example for linear types + +![](img/linear_works.jpg) +[1] Page 7 + +--- + +# Example for linear types +![](img/linear_fails.jpg) +[1] Page 8 diff --git a/slides/makefile b/slides/makefile index 1ea7333..407fca5 100644 --- a/slides/makefile +++ b/slides/makefile @@ -5,4 +5,7 @@ all: clean bib compile clean: rm -rf ./out compile: - marp main.md --theme ./themes/academic.css -o out/presentation.html + mkdir out + cp -r img ./out/img + marp main.md --base . -o out/presentation.html + #marp main.md --base . --allow-local-files -o out/presentation.pdf