704 lines
18 KiB
TeX
704 lines
18 KiB
TeX
\documentclass{beamer}
|
||
|
||
|
||
\usepackage[utf8]{inputenc}
|
||
\usepackage{formal-grammar}
|
||
\usepackage[dvipsnames]{xcolor}
|
||
\usepackage{mathpartir}
|
||
\usepackage{stmaryrd}
|
||
%\usepackage{minted}
|
||
%\usemintedstyle{tango}
|
||
|
||
|
||
\usepackage{listings}% http://ctan.org/pkg/listings
|
||
\lstset{
|
||
basicstyle=\ttfamily,
|
||
mathescape
|
||
}
|
||
|
||
|
||
\newcommand{\metavariable}[1]{\textcolor{teal}{#1}}
|
||
\newcommand{\typeterminal}[1]{\textcolor{brown}{#1}}
|
||
\newcommand{\exprterminal}[1]{\textcolor{Sepia}{#1}}
|
||
|
||
|
||
|
||
\title{A functional core calculus with ladder-types}
|
||
%\date[ISPN ’80]{27th International Symposium of Prime Numbers}
|
||
|
||
|
||
\author[Euclid]{Michael Sippel \texttt{michael.sippel@mailbox.tu-dresden.de}\inst{1}}
|
||
\institute{\inst{1} Technische Universität Dresden}
|
||
|
||
\usetheme{ccc}
|
||
|
||
\begin{document}
|
||
|
||
\begin{frame}
|
||
\titlepage
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}[t, fragile]
|
||
\frametitle{Type Systems}
|
||
\framesubtitle{Safety <> Flexibility}
|
||
|
||
\centering
|
||
\includegraphics[width=0.9\textwidth]{intro.pdf}
|
||
|
||
\pause
|
||
\begin{block}{type information in comments}
|
||
\begin{lstlisting}
|
||
/* this is an angle in degrees */
|
||
double hue = 156.4;
|
||
\end{lstlisting}
|
||
\end{block}
|
||
|
||
\end{frame}
|
||
|
||
\begin{frame}[t, fragile]{Example - Image Processing}
|
||
\begin{lstlisting}
|
||
image-read :: FilePath -> [Color]
|
||
image-write :: FilePath -> [Color] -> ()
|
||
|
||
image-mix :: $\mathbb{R}$ -> [Color] -> [Color] -> [Color]
|
||
image-saturate :: $\mathbb{R}$ -> [Color] -> [Color]
|
||
|
||
let im1 = image-read "in1.png"
|
||
let im2 = image-read "in2.png"
|
||
let im3 = image-mix 0.5
|
||
im1
|
||
(image-saturate 0.8 im2)
|
||
|
||
image-write "out.png" im3
|
||
\end{lstlisting}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Performance Checklist}
|
||
\framesubtitle{(singlethreaded)}
|
||
\begin{enumerate}
|
||
\item<1-> algorithmic
|
||
\begin{itemize}
|
||
\item choose appropriate data structures\\
|
||
(reduce complexity in frequent cases)
|
||
|
||
\item identify special cases
|
||
\end{itemize}
|
||
|
||
\item<2-> implementation detail:
|
||
\begin{itemize}
|
||
\item optimize memory bottleneck
|
||
\begin{itemize}
|
||
\item improve cache \& bus efficiency with compact representations
|
||
\item<3-> Synchronize locality in access order and memory layout.
|
||
(elements accessed in succession shall be close in memory,
|
||
AoS vs SoA)
|
||
|
||
\item<4-> \(\rightarrow\) De-/Encode Overhead
|
||
vs. Fetch-Overhead,\\
|
||
account for machine specific cache-sizes
|
||
\end{itemize}
|
||
\item
|
||
|
||
\item<6-> use SIMD instructions
|
||
\item<7-> interfacing with kernels running on accelerator devices
|
||
\end{itemize}
|
||
\end{enumerate}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}[t, fragile]{Example - Image Processing}
|
||
\begin{lstlisting}
|
||
image-read :: FilePath -> [Color]
|
||
image-write :: FilePath -> [Color] -> ()
|
||
|
||
image-mix :: $\mathbb{R}$ -> [Color] -> [Color] -> [Color]
|
||
image-saturate :: $\mathbb{R}$ -> [Color] -> [Color]
|
||
|
||
let im1 = image-read "in1.png"
|
||
let im2 = image-read "in2.png"
|
||
let im3 = image-mix 0.5
|
||
im1
|
||
(image-saturate 0.8 im2)
|
||
|
||
image-write "out.png" im3
|
||
\end{lstlisting}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Example - Image Processing}
|
||
\framesubtitle{More Types}
|
||
|
||
\begin{itemize}
|
||
\item \texttt{ColorRGBu8}
|
||
\item \texttt{ColorRGBf32}
|
||
\item \texttt{ColorHSVu8}
|
||
\item \texttt{ColorHSVf32}
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}[t, fragile]{Example - Image Processing}
|
||
\framesubtitle{More Types}
|
||
|
||
\begin{lstlisting}
|
||
image-read :: FilePath -> [ColorRGBu8]
|
||
image-write :: FilePath -> [ColorRGBu8] -> ()
|
||
|
||
image-mix :: f32 -> [ColorRGBf32] -> [ColorRGBf32] -> [ColorRGBf32]
|
||
image-saturate:: f32->[ColorHSVf32]->[ColorHSVf32]
|
||
|
||
let im1 = image-read "in1.png"
|
||
let im2 = image-read "in2.png"
|
||
let im3 = image-mix 0.5
|
||
im1
|
||
(image-saturate 0.8 im2)
|
||
|
||
image-write "out.png" im3
|
||
\end{lstlisting}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}[t, fragile]{Example - Image Processing}
|
||
|
||
\framesubtitle{AoS vs SoA}
|
||
|
||
\begin{verbatim}
|
||
[cacheline][cacheline][cacheline]
|
||
\end{verbatim}
|
||
|
||
\begin{verbatim}
|
||
[RGBRGBRG][BRGBRGBR][GBRGBRGB]
|
||
\end{verbatim}
|
||
|
||
\begin{verbatim}
|
||
[HSVHSVHS][VHSVHSVH][SVHSVHSV]
|
||
\end{verbatim}
|
||
|
||
\begin{verbatim}
|
||
[HHHHHHHH][SSSSSSSS][VVVVVVVV]
|
||
\end{verbatim}
|
||
|
||
\end{frame}
|
||
|
||
\begin{frame}{Example - Image Processing}
|
||
\framesubtitle{OpenGL Image Formats}
|
||
|
||
\begin{itemize}
|
||
\item \texttt{GL\_R3\_G3\_B2}
|
||
\item \texttt{GL\_RGB10\_A2}
|
||
\item \texttt{GL\_R11F\_G11F\_B10F}
|
||
\item \texttt{GL\_SRGB8\_ALPHA8}
|
||
\item \ldots
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[width=0.5\textwidth]{sea-of-types/target/sea-of-types-0-bytes.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[width=0.5\textwidth]{sea-of-types/target/sea-of-types-1-ieee754.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.5\textheight]{sea-of-types/target/sea-of-types-2-real.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.5\textheight]{sea-of-types/target/sea-of-types-3-real.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-4-degrees.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-5-turns.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-6-radians.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-7-angle.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-8-hue.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[height=0.8\textheight]{sea-of-types/target/sea-of-types-9-u8.png}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Sea of Types}
|
||
\centering
|
||
\includegraphics[width=\textwidth]{sea-of-types/target/sea-of-types-10-u8.png}
|
||
\end{frame}
|
||
|
||
|
||
|
||
|
||
\begin{frame}{Solutions (I): Traits / Typeclasses / Interfaces}
|
||
\begin{itemize}
|
||
\item todo
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Solutions (II): Wrapper structs / newtype}
|
||
\begin{itemize}
|
||
\item todo
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Coercions: (In-)Coherence with Transitivity}
|
||
\begin{itemize}
|
||
\item<1-> Common example: coerce \texttt{Int -> Real}
|
||
(subsumption \(\mathbb{N} \subset \mathbb{R}\))
|
||
|
||
\begin{itemize}
|
||
\item \texttt{Int -> Real}
|
||
\item \texttt{Int -> String}
|
||
\item \texttt{Real -> String}
|
||
\end{itemize}
|
||
|
||
\item<2-> transitivity creates two extensionally \emph{different} coercion paths:
|
||
\begin{itemize}
|
||
\item \texttt{Int -> String} (3 -> "3")
|
||
\item \texttt{Int -> Real -> String} (3 -> "3.0")
|
||
\end{itemize}
|
||
|
||
\item<3-> Subsumptive interpretation is misleading!
|
||
\item<3-> \texttt{Int -> Real} is not as unambiguous as it might seem.
|
||
\begin{itemize}
|
||
\item value ranges (e.g. map int to unit interval [0,1])
|
||
\item multiple quantization functions (linear, exponential, \dots)
|
||
\end{itemize}
|
||
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Related Work}
|
||
\begin{itemize}
|
||
\item TODO
|
||
\item cite
|
||
\item some
|
||
\item stuff
|
||
\end{itemize}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Ladder Types}
|
||
\begin{block}{Intuition}
|
||
Encode "represented-as" relation into type terms
|
||
\end{block}
|
||
|
||
\begin{block}{}
|
||
\( \tau_1 \sim \tau_2 \) reads "\(\tau_1\) represented as \(\tau_2\)"
|
||
\end{block}
|
||
|
||
\begin{example}\(
|
||
Color \sim sRGB
|
||
\sim HSV \sim \langle \text{Vec3} \quad \mathbb{R}_{[0,1]}
|
||
\sim \langle \text{QuantizeLinear} \quad 256 \rangle
|
||
\sim \mathbb{Z}_{256} \sim \text{machine.UInt8} \sim \text{Byte}
|
||
\rangle
|
||
\sim \text{[Byte; 3]}
|
||
\)\end{example}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Morphisms}
|
||
\begin{block}{Intuition}
|
||
Transform between semantically equivalent representations of the same abstract concept
|
||
\end{block}
|
||
|
||
\begin{block}{Type}
|
||
\( \tau \sim \tau_1 \rightarrow_\text{morph} \tau \sim \tau_2 \)
|
||
\end{block}
|
||
|
||
\begin{example}\(
|
||
Angle \sim Degrees \sim \mathbb{R}
|
||
\rightarrow_\text{morph}
|
||
Angle \sim Radians \sim \mathbb{R}
|
||
\)\end{example}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Morphisms}
|
||
\framesubtitle{Coherence}
|
||
\begin{block}{Morphism Condition}
|
||
Assume\\
|
||
\(\metavariable{m_\sigma} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow_\text{morph} \metavariable{\sigma} \sim \metavariable{\sigma_2}}\)\\
|
||
\(\metavariable{m_\tau} : \typeterminal{\metavariable{\tau} \sim \metavariable{\tau_1} \rightarrow_\text{morph} \metavariable{\tau} \sim \metavariable{\tau_2}}\)\\
|
||
\(\metavariable{f_1} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_1} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_1} }\)\\
|
||
\(\metavariable{f_2} : \typeterminal{\metavariable{\sigma} \sim \metavariable{\sigma_2} \rightarrow \metavariable{\tau} \sim \metavariable{\tau_2} }\)\\
|
||
then it holds that:\\
|
||
\(\forall x:\typeterminal{\metavariable{\sigma}\sim\metavariable{\sigma_1}},\quad
|
||
\metavariable{m_\tau}(\metavariable{f_1} x) = \metavariable{f_2} (\metavariable{m_\sigma} x) \)
|
||
\end{block}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Extending System F}
|
||
\small
|
||
\begin{grammar}
|
||
|
||
\firstcase{ T }{
|
||
\metavariable{\sigma}
|
||
}{Base Type}
|
||
|
||
\otherform{
|
||
\metavariable{\alpha}
|
||
}{Type Variable}
|
||
|
||
\otherform{
|
||
\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \nonterm{T}
|
||
}{Universal Type}
|
||
|
||
\otherform{
|
||
\typeterminal{<} \nonterm{T} \quad \nonterm{T} \typeterminal{>}
|
||
}{Specialized Type}
|
||
|
||
\otherform{
|
||
\nonterm{T} \quad \typeterminal{\rightarrow} \quad \nonterm{T}
|
||
}{Function Type}
|
||
|
||
\otherform{
|
||
\nonterm{T} \quad \typeterminal{\rightarrow_\text{morph}} \quad \nonterm{T}
|
||
}{Morphism Type}
|
||
|
||
\otherform{
|
||
\nonterm{T} \quad \typeterminal{\sim} \quad \nonterm{T}
|
||
}{Ladder Type}
|
||
|
||
$$\\$$
|
||
|
||
\firstcase{ E
|
||
% T_\selexpr
|
||
}
|
||
{ \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 $$
|
||
\nonterm{ E }
|
||
}{Type Abstraction}
|
||
|
||
\otherform{
|
||
$$ \exprterminal{\lambda} \metavariable{x} $$
|
||
\exprterminal{:} \nonterm{ T }
|
||
\quad $$\exprterminal{\mapsto}$$ \quad
|
||
\nonterm{ E }
|
||
}{Value Abstraction}
|
||
|
||
\otherform{
|
||
$$ \exprterminal{\lambda} \metavariable{x} $$
|
||
\exprterminal{:} \nonterm{ T }
|
||
\quad $$\exprterminal{\mapsto_\text{morph}}$$ \quad
|
||
\nonterm{ E }
|
||
}{Value Morphism}
|
||
|
||
\otherform{
|
||
\nonterm{ E }
|
||
\quad
|
||
\nonterm{ T }
|
||
}{Type Application}
|
||
|
||
\otherform{
|
||
\nonterm{ E }
|
||
\quad
|
||
\nonterm{ E }
|
||
}{Value Application}
|
||
|
||
\otherform{
|
||
\nonterm{ E }
|
||
\quad
|
||
\exprterminal{as}
|
||
\quad
|
||
\nonterm{ T }
|
||
}{Ascension}
|
||
|
||
\otherform{
|
||
\nonterm{ E }
|
||
\quad
|
||
\exprterminal{des}
|
||
\quad
|
||
\nonterm{ T }
|
||
}{Descension}
|
||
|
||
\end{grammar}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Morphism Graph}
|
||
|
||
\begin{definition}[Morphism Paths]
|
||
\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}
|
||
\end{definition}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Morphism Graph}
|
||
\begin{example}[Morphism Graph]
|
||
\begin{mathpar}
|
||
\small
|
||
\text{Assume }
|
||
\Gamma := \{\\
|
||
\exprterminal{\text{degrees-to-turns}} : \typeterminal{\text{Angle}\sim\text{Degrees}\sim\mathbb{R} \quad \rightarrow_\text{morph} \quad \text{Angle}\sim\text{Turns}\sim\mathbb{R}},\\
|
||
\exprterminal{\text{turns-to-radians}} : \typeterminal{\text{Angle}\sim\text{Turns}\sim\mathbb{R} \quad \rightarrow_\text{morph} \quad \text{Angle}\sim\text{Radians}\sim\mathbb{R}},\\
|
||
\}.
|
||
\end{mathpar}
|
||
\end{example}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Morphism Graph}
|
||
\begin{example}[Morphism Graph]
|
||
Then ..
|
||
\small
|
||
\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}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Translation}
|
||
\begin{definition}[Morphism Translation]
|
||
\begin{mathpar}
|
||
\small
|
||
|
||
\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[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
|
||
|
||
\end{mathpar}
|
||
\end{definition}
|
||
\end{frame}
|
||
|
||
\begin{frame}{Translation}
|
||
\begin{definition}[Morphism Translation (2)]
|
||
\begin{mathpar}
|
||
\small
|
||
\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}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Translation}
|
||
\begin{example}[Morphism Translation]
|
||
\begin{mathpar}
|
||
\small
|
||
\Big{\llbracket}
|
||
\inferrule[M-Chain]{
|
||
\ldots
|
||
}{
|
||
\Gamma \vdash \typeterminal{\langle\text{Seq}\quad\text{Angle}\sim\text{Degrees}\sim\mathbb{R}\rangle}\\
|
||
\leadsto \typeterminal{\langle\text{Seq}\quad\text{Angle}\sim\text{Radians}\sim\mathbb{R}\rangle}
|
||
}
|
||
\Big{\rrbracket} =
|
||
\exprterminal{\lambda \text{xs}:\typeterminal{\langle\text{Seq}\quad \text{Angle}\sim\text{Degrees}\sim\mathbb{R} \rangle}}
|
||
\newline
|
||
\exprterminal{\mapsto (map \text{ }(\lambda \text{x}:\metavariable{\tau} \mapsto \text{turns-to-radians } (\text{degrees-to-turns } x)) \text{ } xs) }
|
||
\end{mathpar}
|
||
\end{example}
|
||
\end{frame}
|
||
|
||
|
||
|
||
|
||
\begin{frame}{Typing}
|
||
\begin{definition}[Typing Relation]
|
||
\begin{mathpar}
|
||
\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}
|
||
}
|
||
\end{mathpar}
|
||
\end{definition}
|
||
\end{frame}
|
||
|
||
|
||
|
||
\begin{frame}{Translation}
|
||
\begin{definition}[Expression Translation]
|
||
Translates a type-derivation tree into a fully expanded expression
|
||
|
||
\begin{mathpar}
|
||
\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{)}
|
||
\end{mathpar}
|
||
\end{definition}
|
||
\end{frame}
|
||
|
||
|
||
\begin{frame}{Soundness}
|
||
|
||
\begin{lemma}[Morphism generation has correct type]
|
||
\begin{mathpar}
|
||
C :: \Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\\
|
||
\Rightarrow \Gamma \vdash \llbracket C \rrbracket : \metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}
|
||
\end{mathpar}
|
||
\end{lemma}
|
||
|
||
\begin{lemma}[Expression Translation preserves typing]
|
||
\begin{mathpar}
|
||
D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
|
||
\Rightarrow \Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau}
|
||
\end{mathpar}
|
||
\end{lemma}
|
||
\end{frame}
|
||
|
||
|
||
|
||
|
||
\begin{frame}{Soundness}
|
||
\begin{theorem}[Preservation]
|
||
\begin{mathpar} \forall \Gamma, \metavariable{e}, \metavariable{\tau},\\
|
||
D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
|
||
\Rightarrow \llbracket D \rrbracket \rightarrow_{eval} \metavariable{e'} \\
|
||
\Rightarrow \Gamma \vdash \metavariable{e'} : \metavariable{\tau}
|
||
\end{mathpar}
|
||
\end{theorem}
|
||
\end{frame}
|
||
|
||
|
||
|
||
|
||
\begin{frame}{Soundness}
|
||
\begin{theorem}[Progress]
|
||
\begin{mathpar} \forall \Gamma, \metavariable{e}, \metavariable{\tau},\\
|
||
D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
|
||
\Rightarrow \llbracket D \rrbracket \text{ is a value} \\ \vee
|
||
\exists \metavariable{e'} . \llbracket D \rrbracket \rightarrow_{eval} \metavariable{e'} \\
|
||
\end{mathpar}
|
||
\end{theorem}
|
||
\end{frame}
|
||
|
||
|
||
|
||
|
||
\begin{frame}[t, fragile]{Summary}
|
||
|
||
%\begin{tabular*}[h]{p{0.5\textwidth}|p{0.5\textwidth}}
|
||
%\end{tabular*}
|
||
|
||
\end{frame}
|
||
|
||
|
||
|
||
\end{document}
|
||
|