TaPL Notizen

Notizen.tex

\documentclass[a4paper,10pt]{article}

% IMPORTS
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{titlesec}
\usepackage{wrapfig}
\usepackage[ngerman]{babel}
\usepackage[utf8x]{inputenc}
\usepackage{pdfpages}
\usepackage{placeins}
\usepackage{color}
\usepackage{eurosym}
\usepackage{xargs}
\usepackage{xcolor}
\usepackage{subcaption}
\usepackage{hyperref}
\usepackage[margin=2cm]{geometry}
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}

% CONFIG
\clubpenalty = 9000
\widowpenalty = 9000
\displaywidowpenalty = 9000
\titlespacing\section{0pt}{14pt plus 4pt minus 2pt}{2pt plus 2pt minus 1pt}
\titlespacing\subsection{0pt}{10pt plus 4pt minus 2pt}{2pt plus 2pt minus 1pt}
\setlength{\parindent}{0pt}
\setcounter{tocdepth}{2}

% -----------------------------------------------------------------------------
\begin{document}

\begin{titlepage}
	\begin{center}
		\huge Notizen zur Vorlesung \\
		\Huge \textbf{Typen und Programmiersprachen} \\
		\huge gehalten von Prof. Dr.-Ing. Sven Apel \\ im WS 2017/18
		\normalsize

		\vspace{1cm}
		\begin{tabular}[b]{l|l}
			\textbf{author} & Niko Fink \texttt{<finksim@fim.uni-passau.de>} \\
			\textbf{last change} & \today
		\end{tabular}

		\vspace{1cm}
		\tableofcontents
	\end{center}
\end{titlepage}

\section{Knowledge-Base}

\paragraph{formale Systeme und notwendige Eigenschaften}
Formale Sprache + Regeln/Axiome: Programmiersprachen, Kalküle, Scriptsprachen, UML\\
Eigenschaften: Einfachheit (zur Untersuchung und Beweisführung), Aussagekraft (relevante Eigenschaften der Realität exakt widerspiegeln)\\
keine formalen Systeme: natürliche Sprachen, z.B. Deutsch

\paragraph{Vorteile eines Typsystems}
Ein Typsystem ist eine syntaktische Methode zur automatischen Überprüfung von Programmen mit dem Ziel fehlerhaftes Programmverhalten auszuschließen.
\begin{itemize}
\item Fehlererkennung u.U bereits zur Kompilierzeit
\item Effizienz, z.B. durch besser Optimierungsmöglichkeiten
\item Dokumentation, Verbesserung der Code-Lesbarkeit
\item Sicherheitsgarantien
\item Erhöhung des Abstraktionsniveaus
\end{itemize}
$\Rightarrow$ ``Syntaktische Methode zu automatischen Überprüfung von Programmen mit dem Ziel, fehlerhaftes Verhalten auszuschließen ''

\paragraph{statische und dynamische Typprüfung}\mbox{}\\
\begin{tabular}{l|ccc}
 & Eigenschaft & $\oplus$ & $\ominus$ \\ \hline
statisch & Fehlerprüfung zur Übersetzungszeit & Fehler früh erkannt & längere Übersetzung \\
dynamisch & Fehlerprüfung zur Laufzeit & Mehr Fehler zu erkennen & Fehler spät erkannt \\
&&& längere Laufzeit
\end{tabular}

\paragraph{Konservative Typprüfung vs. Ausdruckskraft}
Es kann nur Abwesenheit von Fehlern sichergestellt werden, die Anwesenheit von Fehlern kann nicht bewiesen werden.
Konservative Typprüfung muss so teilweise korrektes Verhalten wie \texttt{if true then 1 else <type error>} als inkorrekt getypt zurückweisen.
Ausdruckstärkere Typsysteme würden in obiger Situation keinen Fehler liefern.

\paragraph{Low-Level vs. High-Level Typprüfung}\mbox{}\\
\begin{minipage}{.5\linewidth}
Low-Level Typfehler
\begin{itemize}
\item Methode nicht vorhanden
\item Operator nicht definiert für einen Typ
\item Typkonvertierung nicht möglich
\end{itemize}
\end{minipage}
\begin{minipage}{.5\linewidth}
High-Level Typfehler
\begin{itemize}
\item Zugriff auf Feld nicht gestattet (z. B. private)
\item Klasse/Methode ist abstrakt
\end{itemize}
\end{minipage}

\paragraph{Typinferenz vs. Typannotation}
\begin{description}
\item[Typinferenz] Typ einer Variablen oder eines gesamten Ausdruckes wird hergeleitet, ohne explizit angegeben werden zu müssen
\item[Typannotation] Programmierer legt den Typ einer Variable oder eines Ausdrucks explizit fest
\end{description}

\paragraph{Java Laufzeit Typfehler}
Division durch 0, ClassCastException, da Belegung von Variablen erst zur Laufzeit bekannt

\paragraph{Effizientere Array-Zugriffe in Java}
Verbot der Zuweisung eines Array-Typen an ein Array eines Subtypen.

\paragraph{Ungeschützte Abstraktionsmechanismen}
\begin{description}
\item[Java] durch die Reflections API
\item[C++] durch Pointerarithmetik
\end{description}

\paragraph{Definition Normalform} als Term, der nicht weiter ausgewertet werden kann
\begin{description}
\item[Sind alle Normalformen Werte?] Je nach Sprachdefinition, ein Term kann auch \emph{stuck} (= Normalform, aber kein Wert) sein
\item[Sind alle Werte Normalformen?] Ja
\end{description}

\paragraph{Fortschritt+Erhaltung}
Fortschritt: Ein wohlgeformter Term ist nicht festgefahren, kann also weiter evaluiert werden\\
Erhaltung: Wenn ein wohlgeformter Term einen Schritt evaluiert wird, entsteht wieder ein wohlgeformter Term


\paragraph{Terme, Werte,...}
Alle Worte einer Sprache werden als Terme bezeichnet\\
Resultat einer Evaluierung ist immer eine Konstante $\rightarrow$ Wert

\paragraph{Semantische Stile}
\begin{description}
\item[Operationale Semantik] abstrakten Maschine
\item[Denotationelle Semantik] mathematische Objekte
\item[Axiomatische Semantik] beweisbare Eigenschaften des Terms
\end{description}

\paragraph{Problem bei Funktionstypen}
keine Typinformation über freie Variablen im Funktionsrumpf, deswegen Einführung des Kontexts $\Gamma$.

\paragraph{Nominelle vs. Strukturelle Subtyprelation}\mbox{}\\
\begin{tabular}{l|l}
\textbf{Strukturell} & \textbf{Nominell} \\
$+$ Rein auf Struktur der Terme & $+$ Dient der Dokumentation/Semantik \\
$+$ keine explizite Angabe nötig & $+$ explizite Angabe \\
$-$ ungewollte Subtyprelation & $-$ keine strukturellen Garantien, wenn es keine Vererbung gibt \\
$\pm$ Mehrfachvererbung (Diamant) & $+$ Typnamen beim Typcheck nutzbar (Reflection, instanceof,...) \\
$+$ statisch &
\end{tabular}

\paragraph{Kovarianz vs. Kontravarianz vs. Invarianz}\mbox{} \\
\begin{minipage}[t]{.3\linewidth}
\textbf{Kovarianz}
\begin{itemize}
\item Relation in gleiche Richtung
\item Rückgabewerte-/typen
\end{itemize}
\end{minipage}
\begin{minipage}[t]{.3\linewidth}
\textbf{Kontravarianz}
\begin{itemize}
\item Relation in entgegengesetzte Richtung
\item Parameterwerte-/typen
\end{itemize}
\end{minipage}
\begin{minipage}[t]{.3\linewidth}
\textbf{Invarianz}
\begin{itemize}
\item Keine Änderung an Parameter und Rückgabetypen erlaubt
\end{itemize}
\end{minipage}

\paragraph{Elemente aus der Objektorientierung}
\begin{itemize}
\item Mehrfachrepräsentation (multiple representation)
\item Dynamische Methodenauswahl (dynamic dispatch)
\item Kapselung (encapsulation)
\item Subtypenbeziehung (subtyping)
\item Vererbung (inheritance)
\item Offene Rekursion (open recursion)
\item Späte Bindung (late binding)
\end{itemize}


\section{Fragen}

\begin{itemize}
\item UE3-2-d warum inneres pair vor äußerem? `pair v (fst ...)' erlaubt kein E-APP2
\item UE4-3-b Wie weiß man bei T-App den T11
\item Wann darf man $\Gamma$ abkürzen?
\item UE5-1+2 Sinn?
\item Sequentielle Komposition / Typaskription / Disjunkte Summen / Varianten / fix / letrec auf Angabenblatt
\item Beispiel Verwendung Varianten
\item UE6-4-b Wie kann man (noch) unbekannte Typen im Ableitungsbaum repräsentieren?; Annahmen für $\epsilon$

\end{itemize}


\section{TODO}

\begin{itemize}
\item Quizzez
\item Knowledge-Base aus Folien und Übungen erweitern
\item Altklausuren
\end{itemize}

\section{Klausurthemen}

\begin{itemize}
\item Featherweight Java: Evaluierung, aber keine Typprüfung + Wissensfragen
\item Ungetypter Lambda-Kalkül
\item Getypter Lambda-Kalkül + Erweiterungen (Referenzen, seq. Komposition,...)
\item Subtypen nur mit Handout-Regeln (Subtypbeziehung + Typüberprüfung)
\item Wissensfragen\\
	$\rightarrow$ Was ist eine Normalform?..\\
	Fortschritt+Erhaltung: Beweisideen, aber keine Durchführung
\item Evaluierung
\item Typableitung
\item Objektorientierung
\end{itemize}

\end{document}