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

Fix positioning of derivation

Browse Source
This commit is contained in:
Daniel Hillerström
2020-04-08 13:15:20 +01:00
parent 3fc9899400
commit 4bc6da9010
1 changed files with 5 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
thesis.tex
View File

@@ -949,8 +949,8 @@ cannot occur more than once in the record. Similarly, the dual rule
\tylab{Inject} states that the injection $(\ell~V)^R$ has type \tylab{Inject} states that the injection $(\ell~V)^R$ has type
$[\ell : \Pre{A}; R]$ if the payload $V$ is well-typed. The implicit $[\ell : \Pre{A}; R]$ if the payload $V$ is well-typed. The implicit
well-kindedness condition on $R$ ensures that $\ell$ cannot be well-kindedness condition on $R$ ensures that $\ell$ cannot be
injected twice. As an example consider the following ill-typed injected twice. To illustrate how the kinding system prevents
injection into a singleton variant type duplicated labels consider the following ill-typed example
% %
\[ \[
(\dec{S}~\Unit)^{\dec{S}:\UnitType} : [\dec{S}:\UnitType;\dec{S}:\UnitType]. (\dec{S}~\Unit)^{\dec{S}:\UnitType} : [\dec{S}:\UnitType;\dec{S}:\UnitType].
@@ -959,27 +959,12 @@ injection into a singleton variant type
Typing fails because the resulting row type is ill-kinded by the Typing fails because the resulting row type is ill-kinded by the
\klab{ExtendRow}-rule: \klab{ExtendRow}-rule:
\begin{mathpar} \begin{mathpar}
\inferrule*[] \inferrule*[leftskip=6.5em,Right={\klab{Variant}}]
{\inferrule*[] {\inferrule*[Right={\klab{ExtendRow}}]
{\vdash \Pre{\UnitType} : \Presence \\ {\vdash \Pre{\UnitType} : \Presence \\
\inferrule*[] \inferrule*[Right={\klab{ExtendRow}}]
{\vdash \Pre{\UnitType} : \Presence \\ \vdash \cdot : \Row_{\color{red}{\{\dec{S}\} \uplus \{\dec{S}\}}}} {\vdash \Pre{\UnitType} : \Presence \\ \vdash \cdot : \Row_{\color{red}{\{\dec{S}\} \uplus \{\dec{S}\}}}}
{\vdash \dec{S}:\Pre{\UnitType};\cdot : \Row_{\emptyset \uplus \{\dec{S}\}}}} {\vdash \dec{S}:\Pre{\UnitType};\cdot : \Row_{\emptyset \uplus \{\dec{S}\}}}}
% {\inferrule[]
% {\vdash \UnitType : \Type}
% {\vdash \Pre{\UnitType} : \Presence}
% \\
% \inferrule*[]
% {\inferrule*[]
% {\vdash \UnitType : \Type}
% {\vdash \Pre{\UnitType} : \Presence}
% \\
% \inferrule*[]
% {}
% {\vdash \dec{None} : \Pre{\UnitType} : \Row_{\{\dec{Some}\} \uplus \{\dec{Some}\}}}
% }
% {\vdash \dec{Some}:\Pre{\UnitType};\dec{None}:\Pre{\UnitType} : \Row_{{\emptyset \uplus \{\dec{Some}\}}}}
% }
{\vdash \dec{S}:\Pre{\UnitType};\dec{S}:\Pre{\UnitType};\cdot : \Row_{\emptyset}} {\vdash \dec{S}:\Pre{\UnitType};\dec{S}:\Pre{\UnitType};\cdot : \Row_{\emptyset}}
} }
{\vdash [\dec{S}:\Pre{\UnitType};\dec{S}:\Pre{\UnitType};\cdot] : \Type} {\vdash [\dec{S}:\Pre{\UnitType};\dec{S}:\Pre{\UnitType};\cdot] : \Type}