%include talk.fmt
\frame{
\frametitle{Structure}
-\begin{verbatim}
+\begin{code}
fir (State pxs) x = (pxs**hs, State (pxs<++x))
where hs = $(vectorTH [2::Int16,3,-2,4])
-\end{verbatim}
+\end{code}
\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}
}
+\note[itemize]{
+\item Wat bepaald nu precies de grootte van het circuit? het aantal optellers en het aantal vermenigvuldigers.
+\item De grootte van de vectoren is van een groot belang voor het bepalen van de grootte en aantal elementen in een circuit.
+\item Next sheet: hoe bepalen we grootte vectors?
+}
\frame{
\frametitle{Structure}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Hoe bepalen we nu de lengte van de vectoren?
+\item We kunnen proberen af te leiden of een ontwerper ze laten opgeven
+\item Next sheet: grootte afleiden
+}
\subsubsection{Size Inference}
\frame{
\item Requires a lot of bookkeeping.
\end{itemize}
}
+\note[itemize]{
+\item We kunnen het aantal elementen tellen van lijsten waarvan de elementen expliciet zijn opgegeven. Zoals de coefficenten in het FIR filter.
+\item Proberen om andere vectoren van deze vectoren af te leiden.
+\item Veel boekhoudwerk, we moeten alle afgeleide lengten opslaan, en daarbij vectoren uniek kunnen bepalen: Van welke vector willen we afleiden?
+\item Next sheet: problemen grootte afleiden
+}
\frame{
\frametitle{Infer Size}
\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}
+\begin{code}
+ xs ** hs = foldl (+) 0 (zipWith (*) xs hs)
+\end{code}
+}
+\note[itemize]{
+\item Kunnen we wel voor elke vector de lengte afleiden?
+\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?
+\item Next sheet: grootte specificeren
}
\subsubsection{Size Specification}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Om (tijdelijk) deze problemen te voorkomen laten we de hardware ontwerper de lengte van de vector opgeven.
+\item Hier hebben we ook weer twee mogelijkheden:
+\item Bij elke instantie de lengte opgeven
+\item Een instantie van een voorafgedefineerd type laten zijn, waarbij het type de lengte informatie bevat.
+\item Next sheet: Basisconcepten programmeren
+}
\frame{
\frametitle{Some basic concepts}
\item Computations can be assigned types to indicate what kind of values to produce or manipulate
\end{itemize}
}
+\note[itemize]{
+\item Even, helaas, een paar defenities
+\item Met programmeertalen druk je dus berekeningen uit
+\item Berekening bewerken waarden
+\item Types worden gebruikt om sets van waarden aan te geven. Bijvoorbeeld het Integer type omvat alle waarden die behoren tot gehele getalen.
+\item Berekeningen kunnen we types toekennen, om aan te geven wat voor waarden ze op moeten leveren, en wat voor waarden ze bewerken
+\item Types geven dus extra informatie over een programma, en helpen bij het detecteren van fouten van de programmeur
+\item Next sheet: Specificeren term level
+}
\frame{
\frametitle{Specify Size (term-level)}
+\begin{code}
+data Vector a = Vec Int a
+\end{code}
\begin{itemize}
\item Size specification at the instance / term level suffers from the same problems as size inference:
\begin{itemize}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\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.
+\item We moeten weer vanalles bijhouden
+\item Ook is er weer het probleem dat we niet kunnen vastleggen wat lengte is van vectoren die van buiten komen.
+\item Next sheet: specificeren type-level
+}
\frame{
\frametitle{Specify Size (type-level)}
\item The size of the vector becomes part of the type:
\begin{itemize}
\item Unconstrained Vectors:
- \begin{verbatim}
+ \begin{code}
Nat n => Vector n a
- \end{verbatim}
+ \end{code}
\item Constrained Vectors:
- \begin{verbatim}
-Vector 4 a
- \end{verbatim}
+ \begin{code}
+Vector 4 Integer
+ \end{code}
\end{itemize}
\end{itemize}
}
+\note[itemize]{
+\item Daarom leggen we de lengte vast in het type van de vector
+\item Nat n geeft aan dat n een natuurlijk getal moet zijn
+\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
+\item Next sheet: we willen meer dan lengte specificeren
+}
\frame{
\frametitle{Specify Size (type-level)}
\item We also want to manipulate or query the size of a vector
\end{itemize}
}
+\note[itemize]{
+\item Maar we willen niet alleen de lengte vastleggen
+\item We willen ook dingen over de lengte kunnen vragen, of de lengte kunnen veranderen
+\item Next sheet: informatie over size opvragen
+}
\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}
+ \begin{code}
first :: Positive n => Vector n a -> a
- \end{verbatim}
+ \end{code}
\item Only works for vectors that are not empty
\end{itemize}
}
+\note[itemize]{
+\item Soms willen we dus iets weten over de lengte van de vector
+\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.
+\item Daarom willen we weten of de lengte, n, Positief is
+\item Next sheet: lengtes afleiden van anderen, en manipuleren
+}
\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}
+ \begin{code}
combine :: Vector n1 a -> Vector n2 a ->
Vector (n1 + n2) a
- \end{verbatim}
+ \end{code}
\end{itemize}
}
+\note[itemize]{
+\item En we willen lengten ook wel eens aanpassen of construeren
+\item Zoals in de functie combine, die 2 vectoren aan elkaar plakt.
+\item We willen aangeven dat de lengte van de resulterende vector, de lengte van de andere twee vectoren bij elkaar opgeteld is.
+\item Next sheet: type-niveau getallen
+}
\frame{
\frametitle{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}
}
+\note[itemize]{
+\item Eigenaardigheden in Haskell: de normale getalen mogen niet onderdeel zijn van een type, omdat het waarden zijn.
+\item Daarom moeten we speciale getallen gebruiken, zogeheette type-level nummers
+\item Deze type-level nummers stellen dus het getal 3 voor! maar hebben niet de waarde 3! Het is nu een type op zichzelf.
+\item Next sheet: problemen met type-niveau getallen
+}
\frame{
\frametitle{Type-level problems}
\item For example, commutativity of addition:\\ a + b = b + a
\end{itemize}
}
+\note[itemize]{
+\item Wij interpreteren bepaalde types als getallen, maar het blijven types, en daarom moeten ze blijven voldoen aan de eisen van het type systeem.
+\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.
+\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.
+\item Next sheet: Geen proofs, daarom geen eigen transformaties
+}
\frame{
\frametitle{Consequences}
\item Result: a (limited) set of vector transformations is exposed to a developer.
\end{itemize}
}
+\note[itemize]{
+\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.
+\item Wij hebben er voor gekozen om de gebruiker niet aan dit soort manier van bewijzen op te bouwen en te gebruiken binnen functies.
+\item Dit betekent dus ook dat gebruikers niet zelf functies kunnen schrijven die de lengte van de vector aanpassen.
+\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.
+\item Next sheet: geen eigen transformaties, daarom geen eigen recursieve functies
+}
\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}
+}
+\note[itemize]{
+\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.
+\item Next sheet: is \clash{} te beperkt?
}
\ No newline at end of file
projects / matthijs / master-project / final-presentation.git / blobdiff