From d116a549406b35583fbaf7edbbb89ae8dd03378e Mon Sep 17 00:00:00 2001 From: Max New <maxsnew@gmail.com> Date: Fri, 26 Oct 2018 13:57:44 -0400 Subject: [PATCH] laziness tweak, typo --- paper/gtt.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/paper/gtt.tex b/paper/gtt.tex index 6a15c56..1ee325d 100644 --- a/paper/gtt.tex +++ b/paper/gtt.tex @@ -4508,7 +4508,7 @@ The following lemma shows this forms a computation ep pair: From this, we see that the easiest way to construct an interpretation of the dynamic computation type is to make it a lazy product of all -the ground types $\u G$: $\dyns \cong \With_{\u G} \u G$. +the ground types $\u G$: $\dync \cong \With_{\u G} \u G$. Using recursive types, we can easily make this a definition of the interpretations: @@ -9383,8 +9383,9 @@ Finally note that once we have introduced the extra thunks to model difference between call-by-name and call-by-need is only relevant for performance reasons. % -Therefore the resulting cast semantics we produce should also be -valid for call-by-need evaluation. +Since divergence and uncatchable errors are idempotent, and these are +usually the only effects in lazy languages, the resulting cast +semantics GTT produces should also be valid for call-by-need. \citet{Degen2012TheIO} give an analysis of different cast semantics for contracts in lazy languages, specifically based on Haskell, so -- GitLab