\documentclass[a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{fancyhdr}
\usepackage{listings}

% Margin Config
\usepackage[top=1in, bottom=1in, left=1in, right=1in]{geometry}

% Header / Footer Config
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\rhead{VO Typsysteme}
\chead{Zusammenfassung bekannter Prüfungsfragen}
\lhead{185.206}
\renewcommand{\footrulewidth}{0.4pt}
\lfoot{\today}
\rfoot{Seite \thepage}

% Listing Config
\lstset
{
	frame=single,
	basicstyle=\ttfamily,
    numberblanklines=false,
    tabsize=4,
    breaklines=true,
    postbreak=\mbox{{$\hookrightarrow$}\space},
}

\begin{document}

\section{Allgemeines}
\subsection{Kovarianz, Kontravarianz, Invarianz}
\begin{itemize}
\item \emph{Kovarianz} bedeutet, dass Parametertypen durch Vererbung gleich bleiben oder spezieller werden (''in Vererbungsrichtung'').
\item \emph{Kontravarianz} bedeutet, dass Parametertypen von Routinen durch Vererbung (bzw. Subtyping) gleich bleiben oder allgemeiner werden (''gegen die Vererbungsrichtung'').
\item \emph{Invarianz} bedeutet, dass Parametertypen durch Vererbung nicht verändert werden.
\end{itemize}

\subsection{Ersetzbarkeitsprinzip}
Ein Typ \emph{s} ist ein Untertyp eines Typs \emph{t} wenn eine Instanz von \emph{s} überall verwendet werden kann wo eine Instanz von \emph{t} erwartet wird. D.h. Eingangsparameter müssen kontravariant sein, Ergebnistypen müssen kovariant sein.

\section{Definitionen von Typen / Sichten auf Typen}
\begin{itemize}
\item Typen sind Werkzeuge zur Klassifikation von Werten aufgrund ihrer Eigenschaften, ihres Verhaltens oder ihrer Verwendungsmöglichkeiten. (Programmierer)

\item Typen sind Schutzschilder gegen unbeabsichtigte bzw. falsche Interpretation roher Daten. (Programmierer)

\item Typen sind Werkzeuge des Softwareentwicklers zur Unterstützung der Programmerstellung, Weiterentwicklung und Wartung. (Programmierer)

\item Typen schränken Ausdrücke syntaktisch ein, so dass Kompatibilität zwischen Operatoren und Operanden zugesichert wird. (Compilerbauer)

\item Typen bestimmen Speicherauslegungen für Werte. (Compilerbauer)

\item Typen legen Verhaltens-Invarianten fest, die alle Instanzen der Typen erfüllen müssen. (CompLang Theoretiker)

\item Ein Typsystem ist eine Menge von Regeln, die jedem Ausdruck einen eindeutigen Typ zuordnet. Dieser Typ beschreibt die Menge aller Umgebungen, in denen der Ausdruck vorkommen kann und eine Bedeutung hat. (CompLang Theoretiker)

\item \emph{Ein Typ beschreibt eine Menge von Instanzen. (Allgemeinste Definition, beinhaltet alle oberen)}
\end{itemize}

\section{Ada}
\subsection{Unterbereichstypen}
Von jedem Typ können verschiedene Unterbereichstypen erzeugt werden. Ein Unterbereichstyp enthält zusätzliche Einschränkungen. Sie stellen keine neuen Typen im eigentlichen Sinn dar. Sie legen nur Einschränkungen fest die zur \emph{Laufzeit} überprüft werden. Unterbereichstypen sind wie Untertypen verwendbar (welche jedoch meist statisch prüfbar sind).
\begin{lstlisting}[language=Ada]
subtype WERKTAG is TAG'(MO)...TAG'(SA);
subtype SMALL is INTEGER range -100..100;
\end{lstlisting}

\subsection{Subtyping}

\subsubsection{Abgeleitete Typen}
Im Gegensatz zu Unterbereichstypen sind abgeleitete Typen tatsächlich eigenständige Typen. Der Compiler prüft auf Namensgleichheit. Auf jedem abgeleiteten Typ sind dieselben Operationen anwendbar, die auf dem Typ, aus dem er abgeleitet wurde, anwendbar sind (= Überladen).
\begin{lstlisting}[language=Ada]
type APFEL is new INTEGER range 0..100;
\end{lstlisting}

\subsubsection{Tagged Records}
Unter \emph{Typerweiterung} versteht man in Ada das \emph{hinzufügen neuer Komponenten} zu abgeleiteten Verbundtypen. Solche erweiterbaren Verbunde müssen mit dem Wort \emph{tagged} gekennzeichnet werden.
\begin{lstlisting}[language=Ada]
type Person is tagged record
	Vorname: String (1..20);
end record;
type Mann is new Person with record
	Barttraeger: Boolean;
end record;
\end{lstlisting}

\subsubsection{Wie funktioniert Subtyping?}
Die Schnittstellenbeschreibungen von Routinen auf einem abgeleiteten Typ unterscheiden sich von den Schnittstellenbeschreibungen der entsprechenden Routinen auf dem ursprünglichen Typ genau dadurch, dass \emph{alle Vorkommen des ursprünglichen Typbezeichners durch den Bezeichner des abgeleiteten Typs ersetzt werden}. Alle anderen Typbezeichner bleiben gleich. Abgeleitete Typen sind Untertypen des ursprünglichen Typs. In Ada sind daher sowohl Eingangs- als auch Ausgangsparameter kovariant (oder invariant). Routinen auf abgeleiteten Typen \emph{widersprechen daher dem Ersetzbarkeitsprinzip}.

\subsubsection{Klassenweite und spezifische Typen}
Zu jedem erweiterbaren Verbundtyp \emph{t} ist implizit ein sogenannter \emph{klassenweiter Typ t'Class} definiert. Die durch \emph{t} definierte Klasse (in Ada-Terminologie) umfasst \emph{t} und alle von \emph{t} abgeleiteten Typen (z.B. gehört zu \emph{Person'Class} \emph{Person} und \emph{Mann}, und zu \emph{Mann'Class} gehört nur \emph{Mann}).

Jede Instanz eines klassenweiten Typs enthält eine unsichtbare Komponente, ein \emph{''tag''}, das den \emph{spezifischen} (= nicht klassenweiten) Typ der Instanz angibt.

Ein klassenweiter Typ gilt als vom entsprechenden spezifischen Typ verschieden. Daher bleiben bei einer Typableitung klassenweite Parametertypen stets unverändert. Alle klassenweiten Parametertypen sind daher invariant und \emph{entsprechen dem Ersetzbarkeitsprinzip}.

\subsection{Statisches- und dynamisches Binden}
Wenn die spezifischen Typen von Argumenten dem Compiler bekannt sind, kann die auszuführende überladene Operation statisch festgelegt werden (\emph{statisches Binden}). Bei Verwendung klassenweiter Typen als Argumenttypen kann die auszuführende Operation jedoch erst zur Laufzeit anhand der \emph{''tag''}-Komponente bestimmt werden (\emph{dynamisches Binden}).

\subsection{Single- / Multiple-Dispatching}
Wenn die Auswahl der Einzelroutine nur über ein einziges Eingangsargument erfolgt, spricht man von \emph{Einfach-Binden} (engl. \emph{''single dispatching''}). Einfach-Binden liegt (wie in Ada) auch vor wenn in jeder Einzelroutine mehrere gekennzeichnete Eingangsparameter einen gemeinsamen Typ haben und die entsprechenden Parameter der Gesamtroutine einen entsprechenden gemeinsamen Obertyp haben. Es muss dynamisch (zur Laufzeit) überprüft werden ob tatsächlich alle Argumente denselben dynamischen Typ haben. Die Auswahl erfolgt dann über den gemeinsamen dynamischen Typ dieser Eingangsargumente. Im allgemeinen Fall, wenn die Auswahl der Einzelroutine über die dynamischen Typen mehrerer beliebiger Argumente erfolgen kann, spricht man von \emph{Mehrfach-Binden} (engl. \emph{''multiple dispatching''}).

\section{Typinferenz}
Es wird versucht die Typen der Lambda-Ausdrücke aus untypisierten Ausdrücken zu berechnen.

\small
\begin{align*}
PT(c) =& \emptyset \triangleright c:t\\
& \text{(Ordnet einer Konstante einen Typ zu, f.e. } c=3 \Rightarrow 3:Int\text{)}\\
PT(x) =& \{x:v\} \triangleright x:v\\
& \text{(Ordnet einem Parameternamen einen neuen Typparameter als Typ zu.}\\
& \text{''Unter der Annahme dass x den Typ v hat, hat x den Typ v'')}\\
PT(e \ e') =	
&\begin{aligned}\text{let } &\Gamma \triangleright f:t = PT(e);  \text{   (Rekursive Berechnung des Typs der Funktion)}\\
						 	&\Gamma' \triangleright f':t' = PT(e');  \text{   (Rekursive Berechnung des Typs des Arguments)}\\
						 	&\theta = unify(\{s = s' | x:s \in \Gamma; x:s' \in \Gamma'\} \cup \{t = t' \rightarrow v\});\\
& \text{(Typparameter aneinander und an Typen binden - x hat den selben Typ in }\Gamma \text{ und }\Gamma'\text{)}
 \end{aligned}\\
& \text{in }\theta\Gamma \cup \theta\Gamma' \triangleright \theta(f \ f'):\theta v\\
PT(\lambda x.e) = & \text{let } \Gamma \triangleright f:t = PT(e);\text{ in } \\
				  & \text{if } x:s \in \Gamma \text{ für ein beliebiges } s \text{ then } \Gamma \setminus \{x:s\} \triangleright (\lambda x:s.f):s\rightarrow t\\
				  & \text{else } \Gamma \triangleright (\lambda x:v.f):v \rightarrow t\\
				  & \text{(Falls Typ noch nicht in Annahme, füge neuen Typ v hinzu. Falls schon, lösche Typvariable}\\
				  & \text{aus } \Gamma \text{, da Typvariable nicht mehr frei ist - zur Vermeidung von Namenskonflikten.)}
\end{align*}
\begin{align*}
unify(\emptyset) =& \emptyset\\
				 & \text{(Die leere Menge ist unifiziert.)}\\
unify(E \cup \{b = b'\}) =& \text{if } b \neq b' \text{ then fail}\\
						  & \text{else } unify(E)\\
				 & \text{(Fehler falls die Gleichung keine Typvariable beinhaltet und Typen ungl. sind.)}\\
unify(E \cup \{v = t\}) =& \text{if } v = t \text{ then } unify(E)\\
						  & \text{else if } v \text{ occurs in } t \text{ then fail}\\
						  & \text{else } unify([t/v]E) \circ [t/v]\\
				 & \text{(Falls v=t ist die Annahme trivial. Falls die Annahme v unter }\\
				 & \text{dem Namen t beinhaltet, ersetze v durch t.}\\
				 & \text{Falls v in t vorkommt wird abgebrochen - ''unendlicher Term''.)}\\
unify(E \cup \{s \rightarrow s' = t \rightarrow t'\}) =& unify(E \cup \{s = t, s' = t'\})\\
				 & \text{(Falls der Funktionstyp gleich ist, setze}\\
				 & \text{Eingangs- und Ausgangsparametertypen gleich.)}\\
\end{align*}
\normalsize
Das Ergebnis der unify-Funktion ist entweder eine Liste an Typparameterersetzungen $[t_1/v_1] \circ ... \circ [t_n/v_n]$ oder ''fail''.
Der \emph{occurs}-Check dient dazu unendliche Terme (rekursive Typen) zu vermeiden.
Der Algorithmus ist im Allgemeinen unentscheidbar. Es gibt jedoch ein eingeschränktes, dafür aber entscheidbares polymorphes Typsystem. Die Einschränkung dieses Typsystems ist, dass rekursive Funktionen innerhalb des Rumpfes der Funktionsdefinition nur monomorph verwendet werden dürfen. Das heißt alle direkt rekursiven Aufrufe müssen dieselben Argumenttypen haben.
Die Komplexität des Algorithmus zur Berechnung des allgemeinsten Typs kann aber auch ohne polymorph rekursive Funktionsaufrufe exponentiell sein, da der \emph{occurs}-Check die Typen die ein Typ beinhaltet rekursiv überprüfen muss.
\begin{lstlisting}[language=Java]
import java.util.AbstractList;
import java.util.List;
public class ExponentialTypeInference {
    List<Integer> xs =
     new Cons<> (1, // 0.5 seconds
      new Cons<> (2, // 0.5 seconds
       new Cons<> (3, // 0.5 seconds
        new Cons<> (4, // 0.6 seconds
         new Cons<> (5, // 0.7 seconds
          new Cons<> (6, // 0.9 seconds
           new Cons<> (7, // 1.4 seconds
            new Cons<> (8, // 6.0 seconds
             new Cons<> (9, // 6.5 seconds
              new Cons<> (10, // 10.5 seconds
               new Cons<> (11, // 26 seconds
                new Cons<> (12, // 76 seconds
                 null))))))))))));
}
class Cons<E> extends AbstractList<E> {
    private final E first;
    private final List<E> rest;

    Cons(E first, List<E> rest) {
        this.first = first;
        this.rest = rest;
    }
    public E get(int i) { return (i == 0) ? first : rest.get(i-1); }
	public int size() { return rest.size()+1; }
}
\end{lstlisting}


\section{Subtyping-Regeln}
\paragraph{Regel für Funktionstypen:}\label{funktionstypen}
$$\frac{\Gamma \vdash s' \leq s \ \ \ \Gamma \vdash t' \leq t}{\Gamma \vdash s \rightarrow t \leq s' \rightarrow t'}$$
Die Formel beschreibt das Ersetzbarkeitsprinzip: Kontravariante (''weniger strenge'') Eingangstypen und kovariante (''strengere'') Ergebnistypen.

\section{Rekursive Typen}

\paragraph{$\boldsymbol\alpha$-Konversionsregel (Umbenennungen):}
\begin{align*}
\mu v.t = \mu u.[u/v]t && (u \not \in free(\mu v.t))
\end{align*}

\paragraph{Faltungsregel:}
\begin{align*}
\mu v.t = [\mu v.t/v]t
\end{align*}
\begin{itemize}
\item Wenn der Typparameter $v$ in $t$ nicht vorkommt, ist $\mu v.t$ äquivalent zu $t$.
\item Sonst ($v$ kommt in $t$ vor) können alle Vorkommen von $v$ in $t$ beliebig durch den Typ selbst ($\mu v.t$) ersetzt werden (Typ wird aufgefaltet).
\end{itemize}

\paragraph{Subtyping-Regel:}
\begin{align*}
\frac{\Gamma \cup \{u \leq v\} \vdash s \leq t}{\Gamma \vdash \mu u.s \leq \mu v.t} && (u \not \in free(t); v \not \in free(s); u,v \not \in free(\Gamma))
\end{align*}
''$\Gamma$ leitet $\mu u.s \leq \mu v.t$ ab wenn es einen Typ $t$ gibt, so dass $\Gamma \cup \{u \leq v\}$ auch $s \leq t$ ableitet.''\\
Die Untertypbeziehung zwischen zwei rekursiven Typen ist also genau dann gegeben, wenn die rekursionsfreien Variablen dieser Typen (mit freien Typparametern statt der gebundenen Typparameter) zueinander in einer Untertypbeziehung stehen, wobei Subtyping-Annahmen für die Typparameter gelten.

Beispiel:
$$\mu u.\{f:u \rightarrow u; x:u\} \not \leq \mu v.\{f:v \rightarrow v\}$$
Es existiert kein Typ $u$, so dass (unter der Subtyping-Annahme $u \leq v$) $\{f:u \rightarrow u; x:u\} \leq \{f:v \rightarrow v\}$ gilt, da dies der Kontravarianz von Eingangsparametern widersprechen würde (kann also durch die Subtyping-Regel für Funktionstypen nicht hergeleitet werden - siehe \ref{funktionstypen}).

\section{F-gebundene Generizität}
Angenommen $T$ bezeichnet einen generischen Typ und $T[S]$ einen Typ, der durch Ersetzung eines Typparameters in $T$ durch den Typ $S$ aus $T$ abgeleitet wird. Im \emph{F-gebundenen Polymorphismus} gilt die Beziehung $S \leq T[S]$, der Untertyp kann also den Typparameter des (generischen) Obertyps ersetzen. Einige aktuelle Sprachen mit Generizität verwenden F-gebundene Generizität und ermöglichen damit rekursive Definitionen wie $S \leq T[S]$.
\begin{lstlisting}[language=Java]
interface Comparable<T> {
	int compareTo(T that);
}
class Integer implements Comparable<Integer> {
	public int compareTo(Integer that) {...}
}
\end{lstlisting}
Der Typ des formalen Parameters \emph{that} wird durch den Typparameter bestimmt, nicht durch Subtyping. Damit werden Einschränkungen beim Subtyping (kovariante bzw. binäre Routinen) vermieden und es trotzdem sichergestellt, dass \emph{this} in \emph{compareTo} denselben Typ wie \emph{that} hat. Wenn $S \leq T[S]$ gilt und ein Untertyp $U \leq S$ existiert, kann $U \leq T[U]$ nicht mehr gelten, sondern nur $U \leq T[S]$ (wie aus $S$ übernommen). Hier hilft der Einsatz von Wildcard-Typen ($S \leq T[?\ extends/super\ S]$) manchmal weiter, schränkt aber die Art der Zugriffe stark ein (extends nur lesend, super nur schreibend).
\begin{lstlisting}[language=Java]
class MyInteger extends Integer {
	// int compareTo(Integer that) - Integer anstatt MyInteger!
}
\end{lstlisting}
Mittels Wildcard-Typen kann das Ersetzbarkeitsprinzip verletzt werden:
\begin{lstlisting}[language=Java]
class SuperC<T extends SuperC> implements Comparable<T> {
    public int compareTo(T that) {...}
}

class SubC extends SuperC<SubC> {
    public int compareTo(SubC that) {...}
}

public class BinaryFunctions {
    public static void main(String... args) {
        SuperC superC = new SuperC();
        SuperC subC = new SubC();
        subC.compareTo(superC); // kann kompiliert werden, wirft aber ClassCastException zur Laufzeit!
    }
}
\end{lstlisting}

\section{Higher Order Subtyping}
Zwei generische Typen $S$ und $T$ sind in einer Untertypbeziehung höherer Ordnung, wenn $S[U] \leq T[U]$ für alle Typen $U$ gilt (wird z.B. in Haskell und C++ verwendet). Nicht-generische Typen werden einfach als Spezialfall generischer Typen gesehen (mit der leeren Menge von Typparametern). Als Grundlage für die Vererbung kann man dann \textless\# (''Matching''), definiert durch $ S \text{\textless}\# T$ wenn $S[U] \leq T[U]$ für alle Typen $U$, anstatt der Untertypbeziehung verwenden. Higher Order Subtyping \emph{erfüllt das Ersetzbarkeitsprinzip nicht}, da gebundene Typparameter in rekursiven Typen kovariant als Eingangsparametertypen verwendet werden dürfen.

Es gilt also folgende Beziehung: $\{i:int, f:u \rightarrow u, next:u \} \text{\textless}\# \{i:int, f:v \rightarrow v \}$

\end{document}

