Compare commits

...

4 commits

View file

@ -116,6 +116,13 @@ $$\\$$
{ \metavariable{x}
} {Variable}
\otherform{
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
\nonterm{ E }
\quad \exprterminal{in} \quad
\nonterm{ E }
}{Variable Binding}
\otherform{
$$ \exprterminal{\Lambda} \metavariable{\alpha}
\quad \exprterminal{\mapsto} \quad $$
@ -136,13 +143,6 @@ $$\\$$
\nonterm{ E }
}{Value Morphism}
\otherform{
\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad
\nonterm{ E }
\quad \exprterminal{in} \quad
\nonterm{ E }
}{Variable Binding}
\otherform{
\nonterm{ E }
\quad
@ -161,23 +161,25 @@ $$\\$$
\exprterminal{as}
\quad
\nonterm{ T }
}{Up-Cast}
}{Ascription}
\otherform{
\nonterm{ E }
\quad
\exprterminal{to}
\quad
\nonterm{ T }
}{Transformation}
\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
%\otherform{
% \nonterm{ E }
% \quad
% \exprterminal{to}
% \quad
% \nonterm{ T }
%}{Transformation}
%\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
$$\\$$
\firstcase{V}{
\exprterminal{\epsilon}
}{Empty Value}
\nonterm{ V } \quad
\exprterminal{as} \quad
\nonterm{ T }
}{Ascribed Value}
\otherform{
\exprterminal{\Lambda} \metavariable{\alpha} \quad
@ -193,19 +195,14 @@ $$\\$$
\nonterm{ E }
}{Abstraction Value}
\otherform{
\nonterm{ V } \quad
\exprterminal{as} \quad
\nonterm{ T }
}{Cast Value}
\end{grammar}
\caption{Syntax of the core calculus with colors for \metavariable{metavariables}, \typeterminal{type-level terminal symbols}, \exprterminal{expression-level terminal symbols}
where $\typenames, \typevars, \exprvars$ are mutually disjoint, countable sets of symbols to denote atomic type identifiers (\(\typenames\)), typevariables (\(\typevars\)), and expression variables (\(\exprvars\)).
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\).
For simplicity, we write \(\metavariable{e} \in \nonterm{E}\) to say that the term \metavariable{e} is contained in the language generated by the nonterminal \(\nonterm{E}\).
$$\\$$}
\end{figure}
@ -242,9 +239,9 @@ The following terms are valid types over \(\Sigma\):
\begin{definition}[Substitution in Types]
Given a type-variable assignment \(\psi_t = \{ \metavariable{\alpha_1} \mapsto \metavariable{\tau_1}, \quad \metavariable{\alpha_2} \mapsto \metavariable{\tau_2}, \quad \dots \}\),
the thereby induced, substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \typenonterm{\{\metavariable{\alpha_1}, \quad \metavariable{\alpha_2}, \quad \dots\}}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\).
Occourences of bound variables \(\metavariable{\alpha_i}\) are
the thereby induced substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \nonterm{T}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\)
, while occurences of bound variables are left untouched.
Further, we assume that for all \(\tau_i\), all variable names are disjunct with the free variables of the term to which the substitution is applied.
Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
@ -261,9 +258,39 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\[\overline{\psi_t} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{ if } \metavariable{e} \text{ is a variable}
\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'} \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}\\
\\
\exprterminal{\text{let } \metavariable{x} = }\overline{\psi_t}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{\text{let } \metavariable{x} = \metavariable{a} \text{ in } \metavariable{e'}}
\\
\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}
\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}
\\
\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'}
\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}
\\
\overline{\psi_t} \metavariable{e'} \overline{\psi_t}\metavariable{\tau}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{( \metavariable{e'} \metavariable{\tau} )}
\\
\overline{\psi_t} \metavariable{e_1} \overline{\psi_t} \metavariable{e_2}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{(\metavariable{e_1} \metavariable{e_2})}
\\
\overline{\psi_t} \metavariable{e'} \exprterminal{\text{ as }} \overline{\psi_t}\metavariable{\tau}
\quad \text{ if \metavariable{e} is of the form }
\exprterminal{ \metavariable{e'} \text{ as } \metavariable{\tau} }
\end{cases}\]
@ -276,96 +303,247 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
\begin{definition}[Substitution in Expressions]
\todo{complete}
Given an expression-variable assignment \(\psi_e = \{ \metavariable{x_1} \mapsto \metavariable{t_1}, \quad \metavariable{x_2} \mapsto \metavariable{t_2}, \quad \dots \}\),
the thereby induced, lexically scoped substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
in an expression \(
e \in
\exprnonterm
{\typevars}
{\{\metavariable{x_1}, \quad \metavariable{x_2}, \quad \dots\}}
\). Lexical scoping is implemented by simply not substituting any bound occourences of variables \(\metavariable{\alpha_i}\). This allows to skip \(\alpha\)-conversion as done in classical \(\lambda\)-calculus.
the thereby induced substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
\[\overline{\psi_e} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } \metavariable{e} \notin \text{Dom}(\psi_e)\\
\metavariable{t} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } (\metavariable{e}\mapsto\metavariable{t}) \in \psi_e\\
\exprterminal{\text{let } \metavariable{x} \text{ = }} \overline{\psi_e}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_e}\metavariable{e'}
\quad \text{if }
\\
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto } \overline{\psi_e} \metavariable{e'}
\quad \text{if \metavariable{e} is of the form }
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
\text{ and } \metavariable{x} \notin \text{Dom}(\psi_e)
\\
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto } \overline{\psi_e \setminus \{\metavariable{x} \mapsto \metavariable{t}\}} \metavariable{e'}
\quad \text{if \metavariable{e} is of the form }
\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
\text{ and } (\metavariable{x}\mapsto\metavariable{t}) \in \psi_e
\\
\[\overline{\psi} \metavariable{e} = \begin{cases}
\metavariable{e} \quad \text{if } \metavariable{\xi} \in \typenames\\
\metavariable{\tau} \quad \text{if } (\metavariable{\xi} \mapsto \metavariable{\tau}) \in \psi\\
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \notin \text{Dom}(\psi)\\
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \in \text{Dom}(\psi)\\
\typeterminal{<} (\overline{\psi} \metavariable{\xi_1}) \quad (\overline{\psi} \metavariable{\xi_2}) \typeterminal{>} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{<} \metavariable{\xi_1} \quad \metavariable{\xi_2} \typeterminal{>}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow} \metavariable{\xi_2}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow_{morph}} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow_{morph}} \metavariable{\xi_2}\\
(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\sim} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\sim} \metavariable{\xi_2}\\
\end{cases}\]
\end{definition}
\subsection{Typing}
\subsubsection{Equivalence of Type Terms}
\begin{definition}[Distributivity]
\todo{}
%We want distributivity of ladders over type-specialization as well as over function/morphism types.
\begin{definition}[Distributivity in Types]
\begin{mathpar}
\typeterminal{< \metavariable{\sigma}\sim\metavariable{\sigma'} \quad \metavariable{\tau} >}
\rightarrow_\text{distribute}
\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma'} \quad \metavariable{\tau} > }
\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau}\sim\metavariable{\tau'} >}
\rightarrow_\text{distribute}
\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma} \quad \metavariable{\tau'} > }
\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow \metavariable{\tau} }
\rightarrow_\text{distribute}
\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow \metavariable{\tau} ) }
\typeterminal{ \metavariable{\sigma} \rightarrow \metavariable{\tau}\sim\metavariable{\tau'} }
\rightarrow_\text{distribute}
\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow \metavariable{\tau'} ) }
\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} }
\rightarrow_\text{distribute}
\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} ) }
\typeterminal{ \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau}\sim\metavariable{\tau'} }
\rightarrow_\text{distribute}
\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau'} ) }
\end{mathpar}
Let \(\rightarrow_\text{condense}\) be the inverse to \(\rightarrow_\text{distribute}\).
See \hyperref[coq:type-dist]{equiv.v:\ref{coq:type-dist}}.
\end{definition}
\begin{definition}[Equivalence Relation]
\todo{}
\begin{definition}[Alpha Conversion in Types]
\begin{mathpar}
\typeterminal{\forall \metavariable{\alpha} . \metavariable{\tau}}
\rightarrow_{\alpha}
\typeterminal{\forall \metavariable{\alpha'} . } \{ \metavariable{\alpha} \mapsto \metavariable{\alpha'} \} \metavariable{\tau}
\end{mathpar}
\end{definition}
\begin{definition}[Equivalence Relation]
Transitive closure over \(\rightarrow_\text{distribute}\), \(\rightarrow_\text{condense}\) and \(\rightarrow_\alpha\).
\begin{mathpar}
\inferrule[E-Refl]{
\metavariable{\tau} \in \nonterm{T}
}{
\metavariable{\tau} \equiv \metavariable{\tau}
}\and
\inferrule[E-Trans]{
\metavariable{\tau_1} \equiv \metavariable{\tau_2}\\
\metavariable{\tau_2} \equiv \metavariable{\tau_3}
}{
\metavariable{\tau_1} \equiv \metavariable{\tau_3}
}
\inferrule[E-Rename]{
\metavariable{\tau_1} \rightarrow_\alpha \metavariable{\tau_2}
}{
\metavariable{\tau_1} \equiv \metavariable{\tau_2}
}
\inferrule[E-Distribute]{
\metavariable{\tau_1} \rightarrow_\text{distribute} \metavariable{\tau_2}
}{
\metavariable{\tau_1} \equiv \metavariable{\tau_2}
}\and
\inferrule[E-Condense]{
\metavariable{\tau_1} \rightarrow_\text{condense} \metavariable{\tau_2}
}{
\metavariable{\tau_1} \equiv \metavariable{\tau_2}
}
\end{mathpar}
See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
\end{definition}
\begin{lemma}[Symmetry of \(\equiv\)]
\begin{mathpar}
\inferrule[E-Symm]{
\metavariable{\tau_1} \equiv \metavariable{\tau_2}
}{
\metavariable{\tau_2} \equiv \metavariable{\tau_1}
}
\end{mathpar}
\begin{proof}
\(\rightarrow_{distribute}\) is the inverse of \(\rightarrow_{condense}\) and \(\rightarrow_{\alpha}\) is symmetric by itself.
\end{proof}
\end{lemma}
\subsubsection{Normal Forms}
\begin{definition}[Ladder Normal Form]
\todo{}
LNF is reached by exhaustive application of \(\rightarrow_\text{distribute}\).
\end{definition}
\subsubsection{Subtyping}
\begin{definition}[Syntactic Subtyping]
\todo{}
\begin{definition}[Parameter Normal Form]
PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
\end{definition}
\begin{definition}[Semantic Subtyping]
\todo{}
\subsubsection{Subtype Relations}
We define two relations: first the syntatic subtype relation \(\leq\) and second the semantic subtype relation \(\precsim\).
\begin{definition}[Syntactic Subtype (\(\tau_1\leq\tau_2\))]
\begin{mathpar}
\inferrule[S-Refl]{
\metavariable{\tau} \equiv \metavariable{\tau'}
}{
\metavariable{\tau} \leq \metavariable{\tau'}
}
\inferrule[S-Syntactic]{
\metavariable{\sigma} \leq \metavariable{\tau}
}{
\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \leq \metavariable{\tau}
}
\end{mathpar}
\end{definition}
\begin{definition}[Semantic Subtype (\(\tau_1\precsim\tau_2\))]
\begin{mathpar}
\inferrule[S-Refl]{
\metavariable{\tau} \equiv \metavariable{\tau'}
}{
\metavariable{\tau} \precsim \metavariable{\tau'}
}
\inferrule[S-Syntactic]{
\metavariable{\sigma} \precsim \metavariable{\tau}
}{
\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \precsim \metavariable{\tau}
}
\inferrule[S-Semantic]{
\metavariable{\sigma} \equiv \metavariable{\tau}
}{
\metavariable{\sigma} \typeterminal{\sim} \metavariable{\sigma'} \precsim \metavariable{\tau} \typeterminal{\sim} \metavariable{\tau'}
}
\end{mathpar}
\end{definition}
\begin{example}[Syntactic \& Semantic Subtypes]$\\$
\begin{enumerate}
\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \leq \quad \) Char }\\
.. is a \emph{syntactic subtype}, because the representation of \typeterminal{<Digit 10>} is \emph{embedded} into \typeterminal{Char}.\\
\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \precsim \quad \) <Digit 10> \(\sim\) machine.UInt64}\\
.. is a \emph{semantic subtype}, because the \typeterminal{Char} based representation can be transformed into a representation based on \typeterminal{machine.UInt64},
while preserving its semantics.
\end{enumerate}
\end{example}
\subsubsection{Inference of Expression Types}
The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).
As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
Using the inference rules given in \ref{def:typerules}, further typing-judgements
of the form
\begin{itemize}
\item \(\metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
\item \(\metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
\item \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
\item \(\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
\end{itemize}
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
\begin{definition}[Syntactic Well-Typedness]
An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
\end{definition}
\begin{definition}[Semantic Well-Typedness]
An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules}.
An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
\end{definition}
\begin{definition}[Inference Rules for the Typing Relation.]
\label{def:typerules}
As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
\begin{definition}[Syntactic Typing Relation]
\label{def:typerules}
\begin{mathpar}
\inferrule[T-Variable]{
\metavariable{x} \in \exprvars\\
\metavariable{\tau} \in \nonterm{T}\\
% \metavariable{x} \in \exprvars\\
% \metavariable{\tau} \in \nonterm{T}\\
\metavariable{x}:\metavariable{\tau} \in \Gamma\\
}{
\Gamma \vdash \metavariable{x}:\metavariable{\tau}
}\and
\inferrule[T-LetBinding]{
\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau}
@ -373,17 +551,16 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau}
}
\inferrule[T-TypeAbs]{
\metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \nonterm{E} \\
% \metavariable{\tau} \in \nonterm{T} \\
% \metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
}{
\Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
}
\inferrule[T-TypeApp]{
\metavariable{\tau} \in \nonterm{T} \\
% \metavariable{\tau} \in \nonterm{T} \\
\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
\metavariable{\sigma} \in \nonterm{T}
}{
@ -391,42 +568,34 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
}
\inferrule[T-ValueAbs]{
\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
\inferrule[T-Abs]{
% \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
% \metavariable{e} \in \nonterm{E} \\
\Gamma,\metavariable{x}:\metavariable{\sigma} \vdash \metavariable{e} : \metavariable{\tau} \\
}{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
}
\inferrule[T-ValueApp]{
\inferrule[T-App]{
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
\Gamma \vdash \metavariable{a} : \metavariable{\sigma} \\
}{
\Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau}
}\and
\inferrule[T-Compatible]{
\Gamma \vdash \metavariable{e} : \metavariable{\tau}
}{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}
}\and
\inferrule[T-MorphAbs]{
\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
\metavariable{e} \in \nonterm{E} \\
\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
}{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
}\and
\inferrule[T-MorphApp]{
\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
% \metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
% \metavariable{e} \in \nonterm{E} \\
\Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
\metavariable{\tau} \precsim \metavariable{\tau'}
}{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\metavariable{\tau'}
}\and
\inferrule[T-MorphFun]{
\Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
}{
\Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
}\and
\inferrule[T-Ascension]{
@ -441,16 +610,98 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
\metavariable{\tau} \leq \metavariable{\tau'}
}{
\Gamma \vdash \metavariable{e} : \metavariable{\tau'}
}\and
}
\end{mathpar}
\end{definition}
\begin{definition}[Semantic Typing Relation]
\label{def:semtyperules}
\begin{mathpar}
\inferrule[T-NativeRepr]{
\Gamma\vdash \metavariable{e} : \metavariable{\tau}
}{
\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
}
\inferrule[T-CoercedRepr]{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
% \metavariable{\tau} \precsim \metavariable{\tau'}\\
%\exists \metavariable{h} \text{ s.t. }
\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
}{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
}
\inferrule[T-CompatibleApp]{
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
}{
\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
}
\end{mathpar}
\end{definition}
\subsection{Coercion Semantics}
We define the translation function \(\llbracket . \rrbracket\) which completes a \emph{semantically well-typed} expression
by inserting all required coercions based on the typing derivation of the expression.
The result shall be a \emph{syntactically well-typed} expression.
We write \(C :: \sigma \precsim \tau\) to mean "C is a subtyping derivation tree whose conclusion is \(\sigma \precsim \tau\)".
Similarly, we write \(D :: \Gamma \vdash e : \tau\) to mean "D is a typing derivation whose conclusion is \(\Gamma \vdash e : \tau\)"
\begin{definition}[Translation]
\begin{mathpar}
\Big{\llbracket} \inferrule[T-SemanticSubtype]{
D_1 :: \Gamma \vdash \metavariable{h}:\metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}\\
D_2 :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\\
% C :: \metavariable{\tau} \precsim \metavariable{\tau'}
}{
\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
}\Big{\rrbracket} = \exprterminal{(}
\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
%\metavariable{h} \llbracket D_2 \rrbracket
\exprterminal{)}
\Big{\llbracket} \inferrule[T-CoercedApp]{
D_1 :: \Gamma \vdash \metavariable{f}:\metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
D_2 :: \Gamma \vdash \metavariable{a}:\approx\metavariable{\sigma}
}{
\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
}\Big{\rrbracket} = \exprterminal{(}
%\exprterminal{(}\metavariable{f} \llbracket D_2 \rrbracket \exprterminal{)}
\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
\exprterminal{)}
\Big{\llbracket}
\inferrule[\emph{Otherwise}]{}{
D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}
}
\Big{\rrbracket} = \metavariable{e}
\end{mathpar}
\end{definition}
\begin{lemma}[Elimination of \(:\approx\)]
\label{lemma:translation}
For all \emph{semantically well-typed} expressions \metavariable{e} with the typing derivation \(D :: \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\),
the translation \(\llbracket D \rrbracket = \metavariable{e'}\), yields a \emph{syntactically well-typed} expression \metavariable{e'} with
\(\emptyset \vdash \metavariable{e'} : \metavariable{\tau} \)
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\subsection{Evaluation}
Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
which are given in \ref{def:evalrules}.
Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by exhaustive application of the rewrite rule \(\rightarrow_\beta\) as in \ref{def:evalrules}.
\begin{definition}[Inference Rules for Evaluation]
\label{def:evalrules}
@ -468,13 +719,13 @@ which are given in \ref{def:evalrules}.
\inferrule[E-App2]{
\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
}{
\metavariable{e_1} \metavariable{e_2}
\metavariable{v_1} \metavariable{e_2}
\rightarrow_\beta
\metavariable{e_1} \metavariable{e_2'}
}
\metavariable{v_1} \metavariable{e_2'}
}\and
\inferrule[E-TypApp]{
\metavariable{\tau} \in \typenonterm{\emptyset}\\
% \metavariable{\tau} \in \typenonterm{\emptyset}\\
\metavariable{e} \rightarrow_\beta \metavariable{e'}
}{
\metavariable{e}
@ -495,7 +746,6 @@ which are given in \ref{def:evalrules}.
\rightarrow_\beta
\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
}\and
\inferrule[E-AppLam]{
}{
\exprterminal{(\lambda} \metavariable{x}
@ -514,64 +764,27 @@ which are given in \ref{def:evalrules}.
\exprterminal{\text{ in }}\metavariable{e}
\rightarrow_\beta
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
}
\inferrule[E-ImplicitCast]{
\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
\Gamma \vdash \metavariable{h} : \metavariable{\sigma'} \typeterminal{\rightarrow_{morph}} \metavariable{\sigma} \\
\Gamma \vdash \metavariable{a} : \metavariable{\sigma'}
}\and
\inferrule[E-Ascribe]{
}{
\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
\rightarrow_\delta
\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
\metavariable{e}
\exprterminal{\text{ as }}
\metavariable{\tau}
\rightarrow_\beta
\metavariable{e}
}
\end{mathpar}
\end{definition}
\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
\label{lemma:preserve-delta-normalform}
Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow_\beta \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[\(\delta\)-normalform eliminates compatibility]
\label{lemma:eliminate-compat}
Assume \(\emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\) and \(\metavariable{e} \rightarrow_{\delta}^* \metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\)
\begin{proof}
\end{proof}
\end{lemma}
\subsection{Soundness}
\begin{lemma}[\(\beta\)-Preservation]
\label{lemma:beta-preservation}
Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[\(\delta\)-Preservation]
\label{lemma:delta-preservation}
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{lemma}[Preservation]
\label{lemma:preservation}
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\).
Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof}
\todo{}
@ -580,23 +793,44 @@ Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdas
\begin{lemma}[Progress]
\label{lemma:progress}
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
then either \(\metavariable{e}\) is a value
or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{theorem}[Soundness]
If \(\emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{theorem}[Syntactic Type Soundness]
\label{theorem:syntactic-soundness}
No syntactically well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof}
By \ref{lemma:}
Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
\end{proof}
\end{theorem}
\begin{theorem}[Semantic Type Soundness]
\label{theorem:semantic-soundness}
No semantically well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof}
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
\end{proof}
\end{theorem}
\newpage
\section{Boehm-Berarducci Encoding}