JKF
113 lines
2.3 KiB
Markdown
113 lines
2.3 KiB
Markdown
---
|
|
theme: dracula
|
|
paginate: true
|
|
_paginate: false
|
|
footer: Topics in Compilers and Concurrency · Julius Fischer · 10.06.2026
|
|
_footer: ""
|
|
style: |
|
|
h1 {
|
|
position: absolute;
|
|
top: 60px;
|
|
left: 75px;
|
|
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{{\;|\;}}
|
|
|
|
$$
|
|
|
|
---
|
|
# What are Destinations?
|
|
- Destination Passing Style
|
|
- Imperative
|
|
- Function takes destination instead of returning structure
|
|
---
|
|
# Example in C
|
|
```
|
|
int* vec_add(int v1[], int v2[], int size) {
|
|
int* res = malloc(size * sizeof(int));
|
|
for (int i = 0; i < size; i++) {
|
|
res[i] = v1[i] + v2[i];
|
|
}
|
|
return res;
|
|
}
|
|
```
|
|
- Add an 'out parameter'
|
|
```
|
|
void dps_vec_add(int res[], int v1[], int v2[], int size) {
|
|
for (int i = 0; i < size; i++) {
|
|
res[i] = v1[i] + v2[i];
|
|
}
|
|
}
|
|
```
|
|
---
|
|
# Motivation for DPS
|
|
- Typical functional map implementation
|
|
```
|
|
map f (x:xs) = (f x : map f xs1)
|
|
> (f x : map f xs)
|
|
> (map f x1 : (f x2 : map f xs2))
|
|
> ...
|
|
```
|
|
- Not tail recursive
|
|
- Performance issue
|
|
- Inefficient stack growth
|
|
```
|
|
map f (x:xs) dest = map f xs (push dest (f x))
|
|
> map f xs1 (push dest (f x1))
|
|
> map f xs2 (push dest (f x2))
|
|
```
|
|
---
|
|
# DPS in functional languages
|
|
- Just add pointers to mutable data?
|
|
- $Int \mapsto Int \mapsto \textcolor{red}{T}$
|
|
- $\textcolor{red}{T *}\mapsto Int \mapsto Int \mapsto \dots$
|
|
- Multiple issues with this
|
|
- Memory safety
|
|
- Multilpe writes on shared memory
|
|
- Purity
|
|
|
|
---
|
|
# Destination Calculus
|
|
- Basic FP terms
|
|
$$
|
|
t, u := x \myor t' t \;|\; t ; t' \;|\; \dots
|
|
$$
|
|
- Case for all datatypes
|
|
$$
|
|
\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
|
|
\end{align}
|
|
$$
|
|
- Additions for destination passing
|
|
$$
|
|
\begin{align}
|
|
\dots \myor
|
|
&
|
|
new_\ltimes \myor
|
|
from_\ltimes t \myor
|
|
to_\ltimes t \myor
|
|
upd_\ltimes \; t \; with \; x \mapsto t' \myor\\
|
|
&
|
|
t \blacktriangleleft t' \myor
|
|
t \leftcirc t' \myor
|
|
t \triangleleft () \myor
|
|
t \triangleleft Inl \myor
|
|
t \triangleleft (,) \myor \dots
|
|
\end{align}
|
|
$$
|
|
|
|
---
|
|
# Referenes
|