diff --git a/beamer/lc-beamer/example.tex b/beamer/lc-beamer/example.tex index f1dfc9c..463277e 100644 --- a/beamer/lc-beamer/example.tex +++ b/beamer/lc-beamer/example.tex @@ -255,19 +255,41 @@ image-write "out.png" im3 \begin{frame}{Solutions (I): Traits / Typeclasses / Interfaces} +\centering + \includegraphics[width=0.5\textwidth]{solution-traits.png} + \vskip1cm \begin{itemize} - \item todo + \item \texttt{impl Angle for Degrees \{ \dots \}} + \item \texttt{impl Angle for Turns \{ \dots \}} + \item \texttt{impl Angle for Radians \{ \dots \}} \end{itemize} \end{frame} \begin{frame}{Solutions (II): Wrapper structs / newtype} +\centering + \includegraphics[width=0.5\textwidth]{solution-wrappers.png} + + \vskip1cm \begin{itemize} - \item todo + \item \texttt{struct Degrees\{ value: f32 \}} + \item \texttt{struct Turns\{ value: f32 \}} + \item \texttt{struct Radians\{ value: f32 \}} \end{itemize} \end{frame} +\begin{frame}{Solutions (II): Wrapper structs / newtype} +\centering + \includegraphics[width=0.5\textwidth]{solution-wrappers.png} + + \vskip1cm + \begin{itemize} + \item \texttt{struct Degrees\{ value: T \}} + \item \texttt{struct Turns\{ value: T \}} + \item \texttt{struct Radians\{ value: T \}} + \end{itemize} +\end{frame} \begin{frame}{Coercions: (In-)Coherence with Transitivity} \begin{itemize} @@ -461,6 +483,22 @@ $$\\$$ + +\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}{Morphism Graph} \begin{definition}[Morphism Paths] @@ -607,24 +645,6 @@ Then .. \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 @@ -693,13 +713,52 @@ D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\\ \end{frame} - - \begin{frame}[t, fragile]{Summary} -%\begin{tabular*}[h]{p{0.5\textwidth}|p{0.5\textwidth}} -%\end{tabular*} +\begin{tabular*}{\textwidth}{p{0.5\textwidth}|p{0.5\textwidth}} + \textbf{Problem} + \small + \begin{itemize} + \item fixed memory representation derived from type + (loss of low level control) + + \item weak type interpretations + (loss of safety) + \end{itemize} + + & + + \textbf{Goal} + \small + \begin{itemize} + \item handle data transformations in type-safe way + \item allow low-level optimizations + with strong, unambiguous types + \end{itemize} + + \\ + + \hline + + \textbf{Ladder-Types} + \small + \begin{itemize} + \item connect low-level representation \& + high-level concept via structure of type terms + \end{itemize} + + & + + \textbf{Result} + \small + \begin{itemize} + \item extended SystemF with ladder types \& morphisms + \item formalized in Coq + \item proved basic lemmas about correctness of translation + \end{itemize} + +\end{tabular*} \end{frame} diff --git a/beamer/lc-beamer/solution-traits.dot b/beamer/lc-beamer/solution-traits.dot new file mode 100644 index 0000000..34e9b8d --- /dev/null +++ b/beamer/lc-beamer/solution-traits.dot @@ -0,0 +1,15 @@ + +digraph SeaOfTypes { + + Degrees [label="Degrees", fontsize=20, shape=plaintext]; + Turns [label="Turns", fontsize=20, shape=plaintext]; + Radians [label="Radians", fontsize=20, shape=plaintext]; + + Angle [label="Angle", fontsize=24, shape=plaintext, color=brown]; + + Angle -> Degrees + Angle -> Turns + Angle -> Radians +} + + diff --git a/beamer/lc-beamer/solution-traits.png b/beamer/lc-beamer/solution-traits.png new file mode 100644 index 0000000..42d6483 Binary files /dev/null and b/beamer/lc-beamer/solution-traits.png differ diff --git a/beamer/lc-beamer/solution-wrappers.dot b/beamer/lc-beamer/solution-wrappers.dot new file mode 100644 index 0000000..877c372 --- /dev/null +++ b/beamer/lc-beamer/solution-wrappers.dot @@ -0,0 +1,15 @@ + +digraph SeaOfTypes { + + Real [label="ℝ", fontsize=24, shape=plaintext]; + + Degrees [label="Degrees", fontsize=20, shape=plaintext]; + Turns [label="Turns", fontsize=20, shape=plaintext]; + Radians [label="Radians", fontsize=20, shape=plaintext]; + + Degrees -> Real + Turns -> Real + Radians -> Real +} + + diff --git a/beamer/lc-beamer/solution-wrappers.png b/beamer/lc-beamer/solution-wrappers.png new file mode 100644 index 0000000..08103dc Binary files /dev/null and b/beamer/lc-beamer/solution-wrappers.png differ