add summary & traits/wrappers

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<T: \(\mathbb{R}\)>\{ value: T \}}
+	\item \texttt{struct Turns<T: \(\mathbb{R}\)>\{ value: T \}}
+	\item \texttt{struct Radians<T: \(\mathbb{R}\)>\{ 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}
 
 

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
+}
+
+

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
+}
+
+