X-Git-Url: https://git.stderr.nl/gitweb?a=blobdiff_plain;f=christiaan%2Fstructure.lhs;fp=christiaan%2Fstructure.lhs;h=2c813972d9235f317e1cb8996cb2aed742ac762d;hb=68dfe53b5995913363ac3fa0240e789e6774cf8a;hp=0000000000000000000000000000000000000000;hpb=a6db20a6d9cfe457b5deb643932813b921a04d47;p=matthijs%2Fmaster-project%2Ffinal-presentation.git

diff --git a/christiaan/structure.lhs b/christiaan/structure.lhs
new file mode 100644
index 0000000..2c81397
--- /dev/null
+++ b/christiaan/structure.lhs
@@ -0,0 +1,164 @@
+\section{Structure}
+%include talk.fmt
+\frame{
+\frametitle{Structure}
+\begin{verbatim}
+fir (State pxs) x = (pxs**hs, State (pxs<++x))
+   where hs = $(vectorTH [2::Int16,3,-2,4])
+\end{verbatim}
+\begin{itemize}
+  \item How did we know how big the circuit would have to be? e.g. How many multipliers?
+  \item The size of the circuit is determined by the size of the vectors!
+\end{itemize}
+}
+
+\frame{
+\frametitle{Structure}
+\begin{itemize}
+  \item The size of the vectors determines the size of the circuit.
+  \item How do we know the size of the vectors?
+  \begin{itemize}
+    \item We infer the size
+    \item We specify the size
+  \end{itemize}
+\end{itemize}
+}
+
+\subsection{Size Inference}
+\frame{
+\frametitle{Infer Size}
+\begin{itemize}
+  \item Determine the size by counting the elements inside, at compile-time.
+  \item Base size of new vectors based on size of other vectors of which you already know the size.
+  \item Requires a lot of bookkeeping.
+\end{itemize}
+}
+
+\frame{
+\frametitle{Infer Size}
+\begin{itemize}
+  \item Might not be possible in the general case?
+  \item What is the size of the combinatorial circuit seen below? Infinite? Zero?
+\end{itemize}
+\begin{verbatim}
+    xs ** hs = foldl (+) 0 (zipWith (*) xs hs)  
+\end{verbatim}
+}
+
+\subsection{Size Specification}
+\frame{
+\frametitle{Specify Size}
+\begin{itemize}
+  \item Have the designer specify the size of a vector.
+  \item Two ways to specify
+  \begin{itemize}
+    \item As part of each specific instance / term
+    \item As part of the type
+  \end{itemize}
+\end{itemize}
+}
+
+\frame{
+\frametitle{Some basic concepts}
+\begin{itemize}
+  \item Programming languages express computations
+  \item Computations manipulate values
+  \item Types = Set of values
+  \item Computations can be assigned types to indicate what kind of values to produce or manipulate
+\end{itemize}
+}
+
+\frame{
+\frametitle{Specify Size (term-level)}
+\begin{itemize}
+  \item Size specification at the instance / term level suffers from the same problems as size inference:
+  \begin{itemize}
+    \item Extensive bookkeeping
+    \item Compile Time-Evaluation
+    \item Generality of the solution
+  \end{itemize}
+\end{itemize}
+}
+
+\frame{
+\frametitle{Specify Size (type-level)}
+\begin{itemize}
+  \item The size of the vector becomes part of the type:
+  \begin{itemize}
+    \item Unconstrained Vectors:
+    \begin{verbatim}
+Nat n => Vector n a  
+    \end{verbatim}
+    \item Constrained Vectors:
+    \begin{verbatim}
+Vector 4 a  
+    \end{verbatim}
+  \end{itemize}
+\end{itemize}
+}
+
+\frame{
+\frametitle{Specify Size (type-level)}
+\begin{itemize}
+  \item Not only do we want to indicate the size of vectors
+  \item We also want to manipulate or query the size of a vector
+\end{itemize}
+}
+
+\frame{
+\frametitle{Size Query}
+\begin{itemize}
+  \item Sometimes we want to know something about the size of the vector
+  \item Get the first element of the vector
+  \begin{verbatim}
+first :: Positive n => Vector n a -> a
+  \end{verbatim}
+  \item Only works for vectors that are not empty
+\end{itemize}
+}
+
+\frame{
+\frametitle{Size Manipulation}
+\begin{itemize}
+  \item Sometimes we want to relate the size of one or more vectors to the size of one or more other vectors
+  \item Combine 2 vectors into 1 large vector
+  \begin{verbatim}
+combine :: Vector n1 a -> Vector n2 a -> 
+           Vector (n1 + n2) a    
+  \end{verbatim}
+\end{itemize}
+}
+
+\frame{
+\frametitle{Type-level numbers}
+\begin{itemize}
+  \item Number literals, e.g. 1, 4 , 17, etc. are not allowed in the type signature.
+  \item We must resort to so-called type-level numbers
+  \item When dealing with type-level number,s each instance is a type in it’s own right! e.g. the type-level equivalent of 3 is D3.
+\end{itemize}
+}
+
+\frame{
+\frametitle{Type-level problems}
+\begin{itemize}
+  \item Type systems demand proofs! Otherwise they are of no use to us!
+  \item When dealing with type-level numbers we suddenly have to proof invariants that we normally take for granted.
+  \item For example, commutativity of addition:\\    a + b = b + a
+\end{itemize}
+}
+
+\frame{
+\frametitle{Consequences}
+\begin{itemize}
+  \item Currently such proofs have to specified as part of the programs, and in a very cumbersome way!
+  \item We chose not to expose this need for proofs to the developer.
+  \item Result: a (limited) set of vector transformations is exposed to a developer.
+\end{itemize}
+}
+
+\frame{
+\frametitle{Consequences}
+\begin{itemize}
+  \item The largest consequence of not allowing any type of vector transforming functions is that a developer can no longer specify recursive functions!
+\end{itemize}
+}
\ No newline at end of file