From 6f8168610566d1d0d84eae46356041700e55a3e6 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 5 Sep 2024 11:20:21 +0200 Subject: [PATCH] paper: define morphism-path relation, redefine typing-relation \& translation --- paper/main.tex | 324 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 223 insertions(+), 101 deletions(-) diff --git a/paper/main.tex b/paper/main.tex index 3a21b30..b15f3cc 100644 --- a/paper/main.tex +++ b/paper/main.tex @@ -6,7 +6,7 @@ \usepackage{mathpartir} \usepackage{hyperref} \usepackage{url} - +\usepackage{stmaryrd} \usepackage{minted} \usemintedstyle{tango} @@ -21,6 +21,7 @@ \DeclareUnicodeCharacter{03B3}{$\gamma$} \DeclareUnicodeCharacter{03B4}{$\delta$} \DeclareUnicodeCharacter{0393}{$\Gamma$} +\DeclareUnicodeCharacter{211D}{$\mathbb{R}$} \newcommand{\metavariable}[1]{\textcolor{teal}{#1}} \newcommand{\typeterminal}[1]{\textcolor{brown}{#1}} @@ -522,34 +523,66 @@ while preserving its semantics. 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 \(\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} +of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\). +\begin{definition}[Morphism Paths] +Given a typing context \(\Gamma\), any type \(\metavariable{\tau}\) can be transformed into \(\metavariable{\tau'}\), provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\), written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\). +\label{def:pathrules} +\begin{mathpar} + + \inferrule[M-Sub]{ + \metavariable{\tau} \leq \metavariable{\tau'} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } + + \inferrule[M-Single]{ + (\metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}) \in \Gamma + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } + + \inferrule[M-Chain]{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\ + \Gamma \vdash \metavariable{\tau'} \leadsto \metavariable{\tau''} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau''} + } + + \inferrule[M-MapSeq]{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + }{ + \Gamma \vdash + \typeterminal{\langle\text{Seq } \metavariable{\tau}\rangle} \leadsto + \typeterminal{\langle\text{Seq } \metavariable{\tau'}\rangle} + } +\end{mathpar} -\begin{definition}[Representational Well-Typedness] -An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{representationally 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}[Compatible Well-Typedness] -An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{compatibly 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{example}[Morphism Graph] +Assume \(\Gamma := \{\\ + \exprterminal{\text{degrees-to-turns}} : \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R} \rightarrow_\text{morph} \text{Angle}\sim\text{Turns}\sim\mathbb{R}},\\ + \exprterminal{\text{turns-to-radians}} : \typeterminal{\text{Angle}\sim\text{Turns}\sim\mathbb{R} \rightarrow_\text{morph} \text{Angle}\sim\text{Radians}\sim\mathbb{R}},\\ +\}\). +Then +\begin{itemize} +\item \(\Gamma \vdash \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R}} \leadsto \typeterminal{\mathbb{R}}\) (by \textsc{M-Sub}) +\item \(\Gamma \vdash \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R}} \leadsto \typeterminal{\text{Angle}\sim\text{Radians}\sim\mathbb{R}}\) (by \textsc{M-Chain}) +\item \(\Gamma \vdash \typeterminal{\langle\text{Seq }\text{Angle}\sim\text{Degrees}\sim\mathbb{R}\rangle} \leadsto \typeterminal{\langle\text{Seq }\text{Angle}\sim\text{Radians}\sim\mathbb{R}\rangle}\) (by \textsc{M-MapSeq}) +\end{itemize} + +\end{example} -\begin{definition}["is" Typing Relation] +\begin{definition}[Typing Relation] \label{def:typerules} \begin{mathpar} \inferrule[T-Variable]{ -% \metavariable{x} \in \exprvars\\ -% \metavariable{\tau} \in \nonterm{T}\\ \metavariable{x}:\metavariable{\tau} \in \Gamma\\ }{ \Gamma \vdash \metavariable{x}:\metavariable{\tau} @@ -563,46 +596,39 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b } \inferrule[T-TypeAbs]{ -% \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} \\ \Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\ \metavariable{\sigma} \in \nonterm{T} }{ \Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \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-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-MorphAbs]{ -% \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 (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\metavariable{\tau'} }\and + \inferrule[T-App]{ + \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ + \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\ + \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} + }{ + \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} + }\and + \inferrule[T-MorphFun]{ \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau} }{ @@ -626,95 +652,191 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b \end{mathpar} \end{definition} -\begin{definition}["compatible" Typing Relation] -\label{def:semtyperules} -\begin{mathpar} - \inferrule[TCompat-NativeRepr]{ - \Gamma\vdash \metavariable{e} : \metavariable{\tau} - }{ - \Gamma\vdash \metavariable{e} :\approx \metavariable{\tau} - } - \inferrule[TCompat-Let]{ - \Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\ - \Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} :\approx \metavariable{\tau} - }{ - \Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) :\approx \metavariable{\tau} - } - - - \inferrule[TCompat-Morph]{ - \Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\ -% \metavariable{\tau} \precsim \metavariable{\tau'}\\ - %\exists \metavariable{h} \text{ s.t. } - \metavariable{h}:\typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}} \in \Gamma - }{ - \Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'} - } - - \inferrule[TCompat-App]{ - \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ - \Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma} - }{ - \Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} :\approx \metavariable{\tau} - } -\end{mathpar} +\begin{definition}[Well-Typedness] +An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{well-typed} if there exist \(\Gamma\) and \(\metavariable{\tau}\) +such that \( \Gamma \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}. \end{definition} \subsection{Coercion Semantics} +%We define the translation function \(\llbracket . \rrbracket\) which translates morphism-paths into +%expressions that define a transformation function, and also translates type-derivations into expressions with expanded type coercions. -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\)". +%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 :: \tau \leadsto \tau'\) to mean "C is a morphism-path derivation tree whose conclusion is \(\tau \leadsto \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{definition}[Morphism Translation] +%Translates a morphism-path derivation into an expression that defines a coercion function + \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[M-Sub]{ + \metavariable{\tau} \leq \metavariable{\tau'} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } +\Big{\rrbracket} = \exprterminal{\lambda x:\metavariable{\tau} \mapsto x} +\and \Big{\llbracket} -\inferrule[\emph{Otherwise}]{}{ -D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau} -} -\Big{\rrbracket} = \metavariable{e} + \inferrule[M-Single]{ + (\metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}) \in \Gamma + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + } +\Big{\rrbracket} = \metavariable{h} +\and + + +\Big{\llbracket} + \inferrule[M-Chain]{ + C_1 :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\ + C_2 :: \Gamma \vdash \metavariable{\tau'} \leadsto \metavariable{\tau''} + }{ + \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau''} + } +\Big{\rrbracket} = \exprterminal{\lambda \text{x}:\metavariable{\tau} \mapsto} + \Big{\llbracket} C_2 \Big{\rrbracket} + \exprterminal{(}\Big{\llbracket} C_1 \Big{\rrbracket} \exprterminal{\text{x})} +\and + + +\Big{\llbracket} + \inferrule[M-MapSeq]{ + C_1 :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'} + }{ + \Gamma \vdash + \typeterminal{\langle\text{Seq } \metavariable{\tau}\rangle} \leadsto + \typeterminal{\langle\text{Seq } \metavariable{\tau'}\rangle} + } +\Big{\rrbracket} = \exprterminal{\lambda \text{xs}:\typeterminal{\langle\text{Seq }\metavariable{\tau}\rangle} \mapsto} + \exprterminal{( \text{map}} \Big{\llbracket} C_1 \Big{\rrbracket} \exprterminal{\text{xs})} \end{mathpar} \end{definition} -\begin{lemma}[Elimination of \(:\approx\)] -\label{lemma:translation} +\begin{definition}[Expression Translation] +%Translates a type-derivation tree into a fully expanded expression -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{mathpar} +\Big{\llbracket} \inferrule[T-Variable]{ + \metavariable{x}:\metavariable{\tau} \in \Gamma +}{ + \Gamma \vdash \metavariable{x}:\metavariable{\tau} +}\Big{\rrbracket} = \metavariable{x} +\and + +\Big{\llbracket} \inferrule[T-LetBinding]{ + D_1 ::\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\ + D_2 :: \Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau} +}{ + \Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau} +}\Big{\rrbracket} = \exprterminal{\text{let }\metavariable{x} = } +\Big{\llbracket} D_1 \Big{\rrbracket} +\exprterminal{\text{ in }} +\Big{\llbracket} D_2 \Big{\rrbracket} +\and + + +\Big{\llbracket} + \inferrule[T-TypeAbs]{ + D_1 :: \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ + }{ + \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau} + } +\Big{\rrbracket} = \exprterminal{\Lambda \metavariable{\alpha} \mapsto} \Big{\llbracket} D_1 \Big{\rrbracket} +\and + + +\Big{\llbracket} + \inferrule[T-TypeApp]{ + D_1 :: \Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\ + \metavariable{\sigma} \in \nonterm{T} + }{ + \Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau} + } +\Big{\rrbracket} = +\exprterminal{(} +\Big{\llbracket} +D_1 +\Big{\rrbracket} +\metavariable{\sigma} +\exprterminal{)} +\and + + +\Big{\llbracket} + \inferrule[T-Abs]{ + D_1 :: \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} + } +\Big{\rrbracket} = +\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} +\exprterminal{\mapsto} \Big{\llbracket}D_1\Big{\rrbracket} +\and + + +\Big{\llbracket} + \inferrule[T-App]{ + D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ + D_2 :: \Gamma \vdash \metavariable{a} : \metavariable{\sigma'}\\\\ + C :: \Gamma \vdash \metavariable{\sigma'} \leadsto \metavariable{\sigma} + }{ + \Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau} + } +\Big{\rrbracket} = + \Big{\llbracket}D_1\Big{\rrbracket} + \exprterminal{(} + \Big{\llbracket}C\Big{\rrbracket} + \Big{\llbracket}D_2\Big{\rrbracket} + \exprterminal{)} +\and + +\Big{\llbracket} + \inferrule[T-MorphFun]{ + D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau} + }{ + \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau} + } +\Big{\rrbracket} = \Big{\llbracket} D_1 \Big{\rrbracket} +\and + +\Big{\llbracket} + \inferrule[T-Ascension]{ + D_1 :: \Gamma \vdash \metavariable{e} : \metavariable{\tau} \\ + \metavariable{\tau'} \leq \metavariable{\tau} + }{ + \Gamma \vdash (\metavariable{e} \exprterminal{\text{ as }} \metavariable{\tau'}) : \metavariable{\tau'} + } +\Big{\rrbracket} = + \Big{\llbracket}D_1\Big{\rrbracket} \exprterminal{\text{ as }} \metavariable{\tau'} +\and + + +\Big{\llbracket} + \inferrule[T-Descension]{ + D_1 :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ + \metavariable{\tau} \leq \metavariable{\tau'} + }{ + \Gamma \vdash \metavariable{e} : \metavariable{\tau'} + } +\Big{\rrbracket} = + \Big{\llbracket} + D_1 + \Big{\rrbracket} + + +\end{mathpar} +\end{definition} -\begin{proof} -\todo{} -\end{proof} -\end{lemma} \subsection{Evaluation}