From 6492391ed4873ba5a57d14c18ee482b12b8b956d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 17 Dec 2021 17:23:01 +0000 Subject: [PATCH] Section 2.2 --- thesis.tex | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/thesis.tex b/thesis.tex index d889604..c1af18d 100644 --- a/thesis.tex +++ b/thesis.tex @@ -2914,7 +2914,7 @@ We can now write some contents to the file and observe the effects. \ea \] -\section{Exceptions: non-local exits} +\section{Exceptions: process termination} \label{sec:tiny-unix-exit} A process may terminate successfully by running to completion, or it @@ -2975,6 +2975,12 @@ returns whatever payload the $\Exit$ operation was carrying. As a consequence, outside of $\status$, an invocation of $\Exit~0$ in $m$ is indistinguishable from $m$ returning normally, e.g. $\status\,(\lambda\Unit.\exit~0) = \status\,(\lambda\Unit.\Unit)$. +% +Technically, the $\Exit$-case provides access to the resumption of +$\Exit$ in $m$, however, we do not write this resumption here, because +it is useless as its type is $\ZeroType \to \Int$. It expects as +argument an element of the empty type, which is of course impossible +to provide, hence we can never invoke it. To illustrate $\status$ and $\exit$ in action consider the following example, where the computation gets terminated mid-way.