dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Reword

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-25 13:03:22 +01:00
parent 650de85238
commit 3438581826
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
thesis.tex
View File

@@ -6749,7 +6749,7 @@ elaboration for top-level function types.
\begin{equations} \begin{equations}
\trval{-} &:& \ValTypeCat \to \ValTypeCat\\ \trval{-} &:& \ValTypeCat \to \ValTypeCat\\
\trval{A \to B \eff E} &\defas& \pval{A}_{E'} \to \pval{B}_{E'} \eff E'\\ \trval{A \to B \eff E} &\defas& \pval{A}_{E'} \to \pval{B}_{E'} \eff E'\\
\multicolumn{3}{l}{\quad\where~E' = (\xval{A} \blacktriangleright E) \blacktriangleright (\xval{B} \blacktriangleright E)} \multicolumn{3}{l}{\quad\where~E' = (\xval{A} \blacktriangleright E) \vartriangleright (\xval{B} \blacktriangleright E)}
\end{equations} \end{equations}
% %
The function $\trval{-}$ traverses the abstract syntax of its argument The function $\trval{-}$ traverses the abstract syntax of its argument
@@ -6757,6 +6757,9 @@ twice. The first traversal propagates effect information outwards to
the ambient effect row $E$. The second traversal pushes the full the ambient effect row $E$. The second traversal pushes the full
ambient information $E'$ inwards. ambient information $E'$ inwards.
% %
The construction of $E'$ makes use of the fact that
$E \vartriangleright E = E$.
%
As a remark, note that the function $\trval{-}$ do not have to As a remark, note that the function $\trval{-}$ do not have to
consider handler types, because they cannot appear at the top-level in consider handler types, because they cannot appear at the top-level in
$\HCalc$. With this syntactic sugar in place we can program with $\HCalc$. With this syntactic sugar in place we can program with