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

Simplify example 4.1

Browse Source
This commit is contained in:
Daniel Hillerström
2020-01-29 19:52:34 +00:00
parent 539e5e6bb1
commit bbbc6bc2da
1 changed files with 5 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
thesis.tex
View File

@@ -1243,7 +1243,7 @@ operation in order to type check.
% %
We will now show that this suspended computation fails to type check We will now show that this suspended computation fails to type check
with the above type signature. Let with the above type signature. Let
$\Gamma_0 = \{\dec{fac} : \Int \to \Int \eff $\Gamma = \{\dec{fac} : \Int \to \Int \eff
\{\dec{Div}:\Zero\}\}$. The following typing derivation shows that \{\dec{Div}:\Zero\}\}$. The following typing derivation shows that
the application of $\dec{fac}$ causes its effect row to be the application of $\dec{fac}$ causes its effect row to be
propagated outwards. propagated outwards.
@@ -1251,12 +1251,12 @@ operation in order to type check.
\begin{mathpar} \begin{mathpar}
\inferrule*[Right={\tylab{Lam}}] \inferrule*[Right={\tylab{Lam}}]
{\inferrule*[Right={\tylab{App}}] {\inferrule*[Right={\tylab{App}}]
{\typ{\emptyset;\Gamma_0,\Unit:\Record{}}{\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\Zero\}}\\ {\typ{\emptyset;\Gamma,\Unit:\Record{}}{\dec{fac} : \Int \to \Int \eff \{\dec{Div}:\Zero\}}\\
\typ{\emptyset;\Gamma_0,\Unit:\Record{}}{3 : \Int} \typ{\emptyset;\Gamma,\Unit:\Record{}}{3 : \Int}
} }
{\typ{\emptyset;\Gamma_0,\Unit:\Record{}}{\dec{fac}~3 : \Int \eff \{\dec{Div}:\Zero\}}} {\typ{\emptyset;\Gamma,\Unit:\Record{}}{\dec{fac}~3 : \Int \eff \{\dec{Div}:\Zero\}}}
} }
{\typ{\emptyset;\Gamma_0}{\lambda\Unit.\dec{fac}~3} : \Unit \to \Int \eff \{\dec{Div}:\Zero\}} {\typ{\emptyset;\Gamma}{\lambda\Unit.\dec{fac}~3} : \Unit \to \Int \eff \{\dec{Div}:\Zero\}}
\end{mathpar} \end{mathpar}
% %
It follows from the typing derivation that the effect row on It follows from the typing derivation that the effect row on