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

Variant typing example

Browse Source
This commit is contained in:
Daniel Hillerström
2020-04-06 14:59:59 +01:00
parent cb1d5c056a
commit 3fc9899400
1 changed files with 48 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

55
thesis.tex
View File

@@ -596,13 +596,16 @@ to $\alpha$-conversion~\cite{Church32} of types.
\paragraph{Type substitution}
We define a type substitution map,
$\sigma : (\TyVarCat \times \TypeCat)^\ast$ as list of pairs mapping a
type variable to its replacement. The domain of a substitution map is
set generated by projecting the first component, i.e.
type variable to its replacement. We denote a single mapping as
$T/\alpha$ meaning substitute $T$ for the variable $\alpha$. We write
multiple mappings using list notation,
i.e. $[T_0/\alpha_0,\dots,T_n/\alpha_n]$. The domain of a substitution
map is set generated by projecting the first component, i.e.
%
\[
\bl
\dom : (\TyVarCat \times \TypeCat)^\ast \to \TyVarCat\\
\dom(\sigma) \defas \{ \alpha \mid (\alpha,\_) \in \sigma \}
\dom(\sigma) \defas \{ \alpha \mid (\_/\alpha) \in \sigma \}
\el
\]
%
@@ -616,7 +619,7 @@ structure as follows.
\begin{eqs}
(A \eff E)\sigma &\defas& A\sigma \eff E\sigma\\
(A \to C)\sigma &\defas& A\sigma \to C\sigma\\
(\forall \alpha^K.C)\sigma &\defas& \forall \alpha^K.C\sigma \quad \text{if } \alpha \notin \dom(\sigma)\\
(\forall \alpha^K.C)\sigma &\defas& \forall \alpha^K.C\sigma \quad \text{convert if } \alpha \in \dom(\sigma)\\
\alpha\sigma &\defas& \begin{cases}
A & \text{if } (\alpha,A) \in \sigma\\
\alpha & \text{otherwise}
@@ -944,9 +947,47 @@ $\Record{\ell : \Abs; R}$ must be well-kinded with respect to
$\Delta$, the label $\ell$ cannot be mentioned in $W$, thus $\ell$
cannot occur more than once in the record. Similarly, the dual rule
\tylab{Inject} states that the injection $(\ell~V)^R$ has type
$[\ell : \Pre{A}; R]$ if the payload $V$ is well-typed. Again since
$[\ell : \Pre{A}; R]$ is well-kinded, it must be that $\ell$ is not
mentioned by $R$. In other words, the tag cannot be injected twice.
$[\ell : \Pre{A}; R]$ if the payload $V$ is well-typed. The implicit
well-kindedness condition on $R$ ensures that $\ell$ cannot be
injected twice. As an example consider the following ill-typed
injection into a singleton variant type
%
\[
(\dec{S}~\Unit)^{\dec{S}:\UnitType} : [\dec{S}:\UnitType;\dec{S}:\UnitType].
\]
%
Typing fails because the resulting row type is ill-kinded by the
\klab{ExtendRow}-rule:
\begin{mathpar}
\inferrule*[]
{\inferrule*[]
{\vdash \Pre{\UnitType} : \Presence \\
\inferrule*[]
{\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}\}}}}
% {\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] : \Type}
\end{mathpar}
%
The two sets $\{\dec{S}\}$ and $\{\dec{S}\}$ are clearly not disjoint,
thus the second premise of the last application of \klab{ExtendRow}
cannot be satisfied.
\paragraph{Typing computations}
The \tylab{App} rule states that an application $V\,W$ has computation