From 440ad1a6a38975f606f52f028ed8b097c529c189 Mon Sep 17 00:00:00 2001 From: skaller Date: Wed, 2 Nov 2022 12:04:12 +1100 Subject: [PATCH] Try to fix #175 --- src/packages/gc.fdoc | 2 +- src/tex/technote-compact-linear-types.tex | 6 ++++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/packages/gc.fdoc b/src/packages/gc.fdoc index d63de352e..35ef2b63f 100644 --- a/src/packages/gc.fdoc +++ b/src/packages/gc.fdoc @@ -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 @ diff --git a/src/tex/technote-compact-linear-types.tex b/src/tex/technote-compact-linear-types.tex index 504d36223..1aa18388a 100644 --- a/src/tex/technote-compact-linear-types.tex +++ b/src/tex/technote-compact-linear-types.tex @@ -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 @@ -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.