From 3fc98994003ddfb4f75397253ede14c3af2ccd0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Mon, 6 Apr 2020 14:59:59 +0100
Subject: [PATCH] Variant typing example

---
 thesis.tex | 55 +++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 48 insertions(+), 7 deletions(-)

diff --git a/thesis.tex b/thesis.tex
index 32a6af7..e1a185c 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -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