christiaan/structure.lhs

   1 \subsection{Structure}
   2 %include talk.fmt
   3 \frame{
   4 \frametitle{Structure}
   5 \begin{verbatim}
   6 fir (State pxs) x = (pxs**hs, State (pxs<++x))
   7    where hs = $(vectorTH [2::Int16,3,-2,4])
   8 \end{verbatim}
   9 \begin{itemize}
  10   \item How did we know how big the circuit would have to be? e.g. How many multipliers?
  11   \item The size of the circuit is determined by the size of the vectors!
  12 \end{itemize}
  13 }
  14
  15 \frame{
  16 \frametitle{Structure}
  17 \begin{itemize}
  18   \item The size of the vectors determines the size of the circuit.
  19   \item How do we know the size of the vectors?
  20   \begin{itemize}
  21     \item We infer the size
  22     \item We specify the size
  23   \end{itemize}
  24 \end{itemize}
  25 }
  26
  27 \subsubsection{Size Inference}
  28 \frame{
  29 \frametitle{Infer Size}
  30 \begin{itemize}
  31   \item Determine the size by counting the elements inside, at compile-time.
  32   \item Base size of new vectors based on size of other vectors of which you already know the size.
  33   \item Requires a lot of bookkeeping.
  34 \end{itemize}
  35 }
  36
  37 \frame{
  38 \frametitle{Infer Size}
  39 \begin{itemize}
  40   \item Might not be possible in the general case?
  41   \item What is the size of the combinatorial circuit seen below? Infinite? Zero?
  42 \end{itemize}
  43 \begin{verbatim}
  44     xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
  45 \end{verbatim}
  46 }
  47
  48 \subsubsection{Size Specification}
  49 \frame{
  50 \frametitle{Specify Size}
  51 \begin{itemize}
  52   \item Have the designer specify the size of a vector.
  53   \item Two ways to specify
  54   \begin{itemize}
  55     \item As part of each specific instance / term
  56     \item As part of the type
  57   \end{itemize}
  58 \end{itemize}
  59 }
  60
  61 \frame{
  62 \frametitle{Some basic concepts}
  63 \begin{itemize}
  64   \item Programming languages express computations
  65   \item Computations manipulate values
  66   \item Types = Set of values
  67   \item Computations can be assigned types to indicate what kind of values to produce or manipulate
  68 \end{itemize}
  69 }
  70
  71 \frame{
  72 \frametitle{Specify Size (term-level)}
  73 \begin{itemize}
  74   \item Size specification at the instance / term level suffers from the same problems as size inference:
  75   \begin{itemize}
  76     \item Extensive bookkeeping
  77     \item Compile Time-Evaluation
  78     \item Generality of the solution
  79   \end{itemize}
  80 \end{itemize}
  81 }
  82
  83 \frame{
  84 \frametitle{Specify Size (type-level)}
  85 \begin{itemize}
  86   \item The size of the vector becomes part of the type:
  87   \begin{itemize}
  88     \item Unconstrained Vectors:
  89     \begin{verbatim}
  90 Nat n => Vector n a
  91     \end{verbatim}
  92     \item Constrained Vectors:
  93     \begin{verbatim}
  94 Vector 4 a
  95     \end{verbatim}
  96   \end{itemize}
  97 \end{itemize}
  98 }
  99
 100 \frame{
 101 \frametitle{Specify Size (type-level)}
 102 \begin{itemize}
 103   \item Not only do we want to indicate the size of vectors
 104   \item We also want to manipulate or query the size of a vector
 105 \end{itemize}
 106 }
 107
 108 \frame{
 109 \frametitle{Size Query}
 110 \begin{itemize}
 111   \item Sometimes we want to know something about the size of the vector
 112   \item Get the first element of the vector
 113   \begin{verbatim}
 114 first :: Positive n => Vector n a -> a
 115   \end{verbatim}
 116   \item Only works for vectors that are not empty
 117 \end{itemize}
 118 }
 119
 120 \frame{
 121 \frametitle{Size Manipulation}
 122 \begin{itemize}
 123   \item Sometimes we want to relate the size of one or more vectors to the size of one or more other vectors
 124   \item Combine 2 vectors into 1 large vector
 125   \begin{verbatim}
 126 combine :: Vector n1 a -> Vector n2 a ->
 127            Vector (n1 + n2) a
 128   \end{verbatim}
 129 \end{itemize}
 130 }
 131
 132 \frame{
 133 \frametitle{Type-level numbers}
 134 \begin{itemize}
 135   \item Number literals, e.g. 1, 4 , 17, etc. are not allowed in the type signature.
 136   \item We must resort to so-called type-level numbers
 137   \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.
 138 \end{itemize}
 139 }
 140
 141 \frame{
 142 \frametitle{Type-level problems}
 143 \begin{itemize}
 144   \item Type systems demand proofs! Otherwise they are of no use to us!
 145   \item When dealing with type-level numbers we suddenly have to proof invariants that we normally take for granted.
 146   \item For example, commutativity of addition:\\    a + b = b + a
 147 \end{itemize}
 148 }
 149
 150 \frame{
 151 \frametitle{Consequences}
 152 \begin{itemize}
 153   \item Currently such proofs have to specified as part of the programs, and in a very cumbersome way!
 154   \item We chose not to expose this need for proofs to the developer.
 155   \item Result: a (limited) set of vector transformations is exposed to a developer.
 156 \end{itemize}
 157 }
 158
 159 \frame{
 160 \frametitle{Consequences}
 161 \begin{itemize}
 162   \item The largest consequence of not allowing any type of vector transforming functions is that a developer can no longer specify recursive functions!
 163 \end{itemize}
 164 }