From c25dbed7c5e8dd099b0c68f74228a9a0feca862a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 30 Jan 2020 15:53:07 +0000 Subject: [PATCH] Minor edits. --- thesis.tex | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/thesis.tex b/thesis.tex index c87f35a..f9283cf 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1274,16 +1274,16 @@ operation in order to type check. A possible inconvenience of the current formulation of $\tylab{Rec}^\ast$ is that it recursion cannot be mixed with other computational effects. The reason being that the effect row on -$A \to B\eff \{\dec{Div}:\Zero\}$ is closed. Thus in practical -programming language implementation it would be more convenient to -leave the tail of the effect row open as to allow recursion to be used -in larger effect contexts. The rule formulation is also rather coarse -as it renders every $\Rec$-definition as possibly divergent -- even -definitions that are obviously non-divergent such as the -$\Rec$-variation of the identity function: $\Rec\;f\,x.x$. A practical -implementation could utilise a static termination -checker~\cite{Walther94} to obtain more fine-grained tracking of -divergence. +$A \to B\eff \{\dec{Div}:\Zero\}$ is closed. Thus in a practical +general-purpose programming language implementation it is likely be +more convenient to leave the tail of the effect row open as to allow +recursion to be used in larger effect contexts. The rule formulation +is also rather coarse as it renders every $\Rec$-definition as +possibly divergent -- even definitions that are obviously +non-divergent such as the $\Rec$-variation of the identity function: +$\Rec\;f\,x.x$. A practical implementation could utilise a static +termination checker~\cite{Walther94} to obtain more fine-grained +tracking of divergence. % By fairly lightweight means we can obtain a finer analysis of % $\Rec$-definitions by simply having an additional typing rule for % the application of $\Rec$.