christiaan/structure.lhs

   1 \subsection{Structure}
   2 %include talk.fmt
   3 \frame{
   4 \frametitle{Structure}
   5 \begin{code}
   6 fir (State pxs) x = (pxs**hs, State (pxs<++x))
   7    where hs = $(vectorTH [2::Int16,3,-2,4])
   8 \end{code}
   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 \note[itemize]{
  15 \item Wat bepaald nu precies de grootte van het circuit? het aantal optellers en het aantal vermenigvuldigers.
  16 \item De grootte van de vectoren is van een groot belang voor het bepalen van de grootte en aantal elementen in een circuit.
  17 \item Next sheet: hoe bepalen we grootte vectors?
  18 }
  19
  20 \frame{
  21 \frametitle{Structure}
  22 \begin{itemize}
  23   \item The size of the vectors determines the size of the circuit.
  24   \item How do we know the size of the vectors?
  25   \begin{itemize}
  26     \item We infer the size
  27     \item We specify the size
  28   \end{itemize}
  29 \end{itemize}
  30 }
  31 \note[itemize]{
  32 \item Hoe bepalen we nu de lengte van de vectoren?
  33 \item We kunnen proberen af te leiden of een ontwerper ze laten opgeven
  34 \item Next sheet: grootte  afleiden
  35 }
  36
  37 \subsubsection{Size Inference}
  38 \frame{
  39 \frametitle{Infer Size}
  40 \begin{itemize}
  41   \item Determine the size by counting the elements inside, at compile-time.
  42   \item Base size of new vectors based on size of other vectors of which you already know the size.
  43   \item Requires a lot of bookkeeping.
  44 \end{itemize}
  45 }
  46 \note[itemize]{
  47 \item We kunnen het aantal elementen tellen van lijsten waarvan de elementen expliciet zijn opgegeven. Zoals de coefficenten in het FIR filter.
  48 \item Proberen om andere vectoren van deze vectoren af te leiden.
  49 \item Veel boekhoudwerk, we moeten alle afgeleide lengten opslaan, en daarbij vectoren uniek kunnen bepalen: Van welke vector willen we afleiden?
  50 \item Next sheet: problemen grootte afleiden
  51 }
  52
  53 \frame{
  54 \frametitle{Infer Size}
  55 \begin{itemize}
  56   \item Might not be possible in the general case?
  57   \item What is the size of the combinatorial circuit seen below? Infinite? Zero?
  58 \end{itemize}
  59 \begin{code}
  60      xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
  61 \end{code}
  62 }
  63 \note[itemize]{
  64 \item Kunnen we wel voor elke vector de lengte afleiden?
  65 \item Er vanuitgaande dat xs en hs van buiten de chip komen, wat zijn dan de lengten van xs en hs? Hoe moeten die worden afgeleid?
  66 \item Next sheet: grootte specificeren
  67 }
  68
  69 \subsubsection{Size Specification}
  70 \frame{
  71 \frametitle{Specify Size}
  72 \begin{itemize}
  73   \item Have the designer specify the size of a vector.
  74   \item Two ways to specify
  75   \begin{itemize}
  76     \item As part of each specific instance / term
  77     \item As part of the type
  78   \end{itemize}
  79 \end{itemize}
  80 }
  81 \note[itemize]{
  82 \item Om (tijdelijk) deze problemen te voorkomen laten we de hardware ontwerper de lengte van de vector opgeven.
  83 \item Hier hebben we ook weer twee mogelijkheden:
  84 \item Bij elke instantie de lengte opgeven
  85 \item Een instantie van een voorafgedefineerd type laten zijn, waarbij het type de lengte informatie bevat.
  86 \item Next sheet: Basisconcepten programmeren
  87 }
  88
  89 \frame{
  90 \frametitle{Some basic concepts}
  91 \begin{itemize}
  92   \item Programming languages express computations
  93   \item Computations manipulate values
  94   \item Types = Set of values
  95   \item Computations can be assigned types to indicate what kind of values to produce or manipulate
  96 \end{itemize}
  97 }
  98 \note[itemize]{
  99 \item Even, helaas, een paar defenities
 100 \item Met programmeertalen druk je dus berekeningen uit
 101 \item Berekening bewerken waarden
 102 \item Types worden gebruikt om sets van waarden aan te geven. Bijvoorbeeld het Integer type omvat alle waarden die behoren tot gehele getalen.
 103 \item Berekeningen kunnen we types toekennen, om aan te geven wat voor waarden ze op moeten leveren, en wat voor waarden ze bewerken
 104 \item Types geven dus extra informatie over een programma, en helpen bij het detecteren van fouten van de programmeur
 105 \item Next sheet: Specificeren term level
 106 }
 107
 108 \frame{
 109 \frametitle{Specify Size (term-level)}
 110 \begin{code}
 111 data Vector a = Vec Int a
 112 \end{code}
 113 \begin{itemize}
 114   \item Size specification at the instance / term level suffers from the same problems as size inference:
 115   \begin{itemize}
 116     \item Extensive bookkeeping
 117     \item Compile Time-Evaluation
 118     \item Generality of the solution
 119   \end{itemize}
 120 \end{itemize}
 121 }
 122 \note[itemize]{
 123 \item Als we per vector gaan specificeren wat de lengte is krijgen we weer dezelfde soort problemen als we hadden met het afleiden van lengten.
 124 \item We moeten weer vanalles bijhouden
 125 \item Ook is er weer het probleem dat we niet kunnen vastleggen wat lengte is van vectoren die van buiten komen.
 126 \item Next sheet: specificeren type-level
 127 }
 128
 129 \frame{
 130 \frametitle{Specify Size (type-level)}
 131 \begin{itemize}
 132   \item The size of the vector becomes part of the type:
 133   \begin{itemize}
 134     \item Unconstrained Vectors:
 135     \begin{code}
 136 Nat n => Vector n a
 137     \end{code}
 138     \item Constrained Vectors:
 139     \begin{code}
 140 Vector 4 Integer
 141     \end{code}
 142   \end{itemize}
 143 \end{itemize}
 144 }
 145 \note[itemize]{
 146 \item Daarom leggen we de lengte vast in het type van de vector
 147 \item Nat n geeft aan dat n een natuurlijk getal moet zijn
 148 \item Nu kunnen we dus bijvoorbeeld aangeven, dat er een vector type moet zijn die aangeeft dat er het 4 element heeft, en dat deze elementen van het type Integer zijn
 149 \item Next sheet: we willen meer dan lengte specificeren
 150 }
 151
 152 \frame{
 153 \frametitle{Specify Size (type-level)}
 154 \begin{itemize}
 155   \item Not only do we want to indicate the size of vectors
 156   \item We also want to manipulate or query the size of a vector
 157 \end{itemize}
 158 }
 159 \note[itemize]{
 160 \item Maar we willen niet alleen de lengte vastleggen
 161 \item We willen ook dingen over de lengte kunnen vragen, of de lengte kunnen veranderen
 162 \item Next sheet: informatie over size opvragen
 163 }
 164
 165 \frame{
 166 \frametitle{Size Query}
 167 \begin{itemize}
 168   \item Sometimes we want to know something about the size of the vector
 169   \item Get the first element of the vector
 170   \begin{code}
 171 first :: Positive n => Vector n a -> a
 172   \end{code}
 173   \item Only works for vectors that are not empty
 174 \end{itemize}
 175 }
 176 \note[itemize]{
 177 \item Soms willen we dus iets weten over de lengte van de vector
 178 \item Voor de functie first, die het eerste element uit een vector haalt, moeten we dus wel zeker weten dat de vector minimaal een element heeft.
 179 \item Daarom willen we weten of de lengte, n, Positief is
 180 \item Next sheet: lengtes afleiden van anderen, en manipuleren
 181 }
 182
 183 \frame{
 184 \frametitle{Size Manipulation}
 185 \begin{itemize}
 186   \item Sometimes we want to relate the size of one or more vectors to the size of one or more other vectors
 187   \item Combine 2 vectors into 1 large vector
 188   \begin{code}
 189 combine :: Vector n1 a -> Vector n2 a ->
 190            Vector (n1 + n2) a
 191   \end{code}
 192 \end{itemize}
 193 }
 194 \note[itemize]{
 195 \item En we willen lengten ook wel eens aanpassen of construeren
 196 \item Zoals in de functie combine, die 2 vectoren aan elkaar plakt.
 197 \item We willen aangeven dat de lengte van de resulterende vector, de lengte van de andere twee vectoren bij elkaar opgeteld is.
 198 \item Next sheet: type-niveau getallen
 199 }
 200
 201 \frame{
 202 \frametitle{Type-level numbers}
 203 \begin{itemize}
 204   \item Number literals, e.g. 1, 4 , 17, etc. are not allowed in the type signature.
 205   \item We must resort to so-called type-level numbers
 206   \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.
 207 \end{itemize}
 208 }
 209 \note[itemize]{
 210 \item Eigenaardigheden in Haskell: de normale getalen mogen niet onderdeel zijn van een type, omdat het waarden zijn.
 211 \item Daarom moeten we speciale getallen gebruiken, zogeheette type-level nummers
 212 \item Deze type-level nummers stellen dus het getal 3 voor! maar hebben niet de waarde 3! Het is nu een type op zichzelf.
 213 \item Next sheet: problemen met type-niveau getallen
 214 }
 215
 216 \frame{
 217 \frametitle{Type-level problems}
 218 \begin{itemize}
 219   \item Type systems demand proofs! Otherwise they are of no use to us!
 220   \item When dealing with type-level numbers we suddenly have to proof invariants that we normally take for granted.
 221   \item For example, commutativity of addition:\\    a + b = b + a
 222 \end{itemize}
 223 }
 224 \note[itemize]{
 225 \item Wij interpreteren bepaalde types als getallen, maar het blijven types, en daarom moeten ze blijven voldoen aan de eisen van het type systeem.
 226 \item Omdat het type systeem garanties moet geven over de correctheid vereist het bewijzen. Als ze zomaar alles zouden accepteren heb je er niks aan.
 227 \item Als gevolg moeten we dus opeens invarianten bewijzen die voor ons heel natuurlijk zijn. Die iedereen eigenlijk voor lief neemt. Zoals de communicativiteit van het optellen.
 228 \item Next sheet: Geen proofs, daarom geen eigen transformaties
 229 }
 230
 231 \frame{
 232 \frametitle{Consequences}
 233 \begin{itemize}
 234   \item Currently such proofs have to specified as part of the programs, and in a very cumbersome way!
 235   \item We chose not to expose this need for proofs to the developer.
 236   \item Result: a (limited) set of vector transformations is exposed to a developer.
 237 \end{itemize}
 238 }
 239 \note[itemize]{
 240 \item Er is binnen Haskell niet echt goede ondersteuning om dit soort invarianten op te schrijven. Op dit moment moet je bewijsopbouwers aanroepen in de functie zelf.
 241 \item Wij hebben er voor gekozen om de gebruiker niet aan dit soort manier van bewijzen op te bouwen en te gebruiken binnen functies.
 242 \item Dit betekent dus ook dat gebruikers niet zelf functies kunnen schrijven die de lengte van de vector aanpassen.
 243 \item Als gevolg is er een aantal vooraf gedefineerde vector transformatie functies gemaakt en samengevoegd in een library. Een gebruiker kan geen nieuwe transformaties maken.
 244 \item Next sheet: geen eigen transformaties, daarom geen eigen recursieve functies
 245 }
 246
 247 \frame{
 248 \frametitle{Consequences}
 249 \begin{itemize}
 250   \item The largest consequence of not allowing any type of vector transforming functions is that a developer can no longer specify recursive functions!
 251 \end{itemize}
 252 }
 253 \note[itemize]{
 254 \item Het grootste gevolg is dat gebruikers nu helaas geen eigen recursieve functies mogen maken. Omdat  ze de structuur van een vector niet mogen aanpassen.
 255 \item Next sheet: is \clash{} te beperkt?
 256 }