Skip to content

Commit

Permalink
Try to fix #175
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed Nov 2, 2022
1 parent f4889ea commit 440ad1a
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 3 deletions.
2 changes: 1 addition & 1 deletion src/packages/gc.fdoc
Original file line number Diff line number Diff line change
Expand Up @@ -2464,7 +2464,7 @@ includes: '"flx_gc.hpp"'
Requires: judy
library: flx_gc
macros: BUILD_FLX_GC
Requires: judy flx_exceptions
Requires: judy flx_exceptions pthread
srcdir: src/gc
src: .*\.cpp
@
Expand Down
6 changes: 4 additions & 2 deletions src/tex/technote-compact-linear-types.tex
Original file line number Diff line number Diff line change
Expand Up @@ -510,10 +510,11 @@ \subsection{Product Encoding}
First, for products the constructor is given by
\begin{align*}
\tt{rep}: \prod_{i=0}^{n-1}X_i &\longrightarrow \mathbb{N}\\
(v0, ... ,v_{n-1}) &\mapsto \sum_{i=0}^{n-1}v_i | \prod_{j=i+1}^{n-1} X_j|
(v0, ... ,v_{n-1}) &\mapsto \sum_{i=0}^{n-1}\rm{rep}(v_i) | \prod_{j=i+1}^{n-1} X_j|
\end{align*}
and the projections are given by
\begin{align*}
\mathbb{N} \longrightarrow \mathbb{N}
\pi_j (p) = p \quot (|\prod_{i=j+1}^{n-1}X_i|) \, \rmd \, |X_j|
\end{align*}
In other words, we simply divide by the size of the tail of a component
Expand All @@ -530,7 +531,8 @@ \subsection{Product Encoding}
\subsection{Sum Encoding}
For sum types, the constructors are injection functions:
\begin{align*}
v_i &\mapsto \sum_{i=0}^{n-1}v_i | \sum_{j=i+1}^{n-1} X_j|
X^i\longrightarrow \sum_{j=0}^{n-1}X_j\\
v_i &\mapsto \sum_{i=0}^{n-1}\rm{rep}(v_i) | \sum_{j=i+1}^{n-1} X_j|
\end{align*}
The interpretation is that, for component we sequentially assign a subrange
of natural numbers correpsonding to the number of values of that component.
Expand Down

0 comments on commit 440ad1a

Please sign in to comment.