# Typsysteme Prüfungsvorbereitung

## Was versteht man unter einem Typ?

Benutzer der Sprache

1. Werkzeuge zur Klassifizierung aufgrund Eigenschaften, Verhalten, Verwendung
2. Schutzschilder gegen unbeabsichtigte/falsche Interpretation von Rohdaten 
3. Werkzeuge zur Programmerstellung, Weiterentwicklung, Wartung

Compilerentwickler

4. schränken Aussagen syntaktisch ein für Kompatibilität von Operationen
5. bestimmen Speicherauslegungen für Werte

Theoretiker

6. legen Verhaltensinvarianten für Instanzen des Typs fest

Ganz allgemein:  
*Eine Menge von Instanzen*

## Was versteht man unter einem Typsystem?

Ein Typsystem ist eine Menge von Regeln um Ausdrücken einen eindeutigen allgemeinsten Typ zuzuordnen.

## Was sind Kriterien nach denen man Typsysteme einteilen kann?

Kriterien:
* Definierbarkeit (vordefiniert, definierbar)
* Art der Definition (extensional, intensional)
  * extensional: alle Instanzen des Typs
  * intensional: Eigenschaften relativ zu anderen Typen
* Typfestlegung (statisch, stark, schwach)
* Mächtigkeit (flexibel, sicher einfach)
* Typzwang (konservativ, optimistisch)
* Durchlässigkeit (dicht, löchrig)
* Typäquivalenz (struktur, name)
* Abstraktionsgrad (abstrakt, konkret)
* Ausdrücklichkeit (implizit, explizit)
* Überschneidungen (monomorph, polymorph)

Typisierungsmengen:
Sprachen > typisierte Sprachen > vollständig typisierte Sprachen > stark typisierte Sprachen > statisch typisierte Sprachen

## Welche Arten von polymorphen Typsystemen gibt es?

Polymorphe Typsysteme haben Variablen mit mehreren Typen:

* Deklarierter Typ ist jener, mit dem Variable deklariert wurde
* Statischer Typ ist jener, der vom Compiler ermittelt wird.
* Dynamischer Typ ist der speziellste Typ, den der in der Variable gerade gespeicherte Wert hat

Aufteilung in:

* universell quantifiziert
  * parametrisch (aka Generics)
  * Subtyping
* ad-hoc polymorph
  * überladen
  * umwandelnd

## Was sind Unterbereichstypen in Ada?

Von jedem Typ kann ein Unterbereichstyp erstellt werden, und ist eigentlich kein neuer Typ. Hat zusätzliche Einschränkungen, wie z.B range und precision. 
Können nur dynamisch geprüft werden im Gegensatz zu abgeleiteten Typen welche auch statisch geprüft werden können.

## Was sind abgeleitete Typen in Ada? Wie funktioniert Ableitung in Ada? Ersetzbarkeitsprinzip?

Sind tatsächlich eigenständige Typen. Compiler prüft auf Namensgleichheit. Alle Operationen vom Obertyp sind auf den Untertyp anwendbar. Die Schnittstellenbeschreibungen von Routinen werden so angepasst dass alle Obertypvorkommen durch Untertypvorkommen ersetzt werden. Dadurch sind alle Parameter in Ada kovariant, was das Ersetzbarkeitsprinzip verletzt, weil dieses besagt dass Eingangsparameter kontravariant sein müssen.

## Was sind Verbunde mit Diskriminanten bzw. Varianten in Ada?

Diskriminanten sind spezielle Komponenten in Verbundtypen, die die Struktur bestimmen. Sie können zB Bereichsgrenzen für Typen definieren. 

Varainten werden mittels case Anweisungen auf Diskriminanten festgelegt. 

## Was sind Tagged Records in Ada?

Das sind Verbunde, welche erweitert werden können. D.h. sie verwenden das Konzept der Composition, statt der Vererbung. Man kann dadurch neue Komponenten hinzufügen um neue Typen zu erstellen. (z.B. Mann ist Person mit Bart)

## Was sind Klassenweite Typen in Ada?

Zu jedem Verbundtyp t gibt es einen klassenweiten typ t'Class. Diese "Klasse" umfasst t und alle davon abgeleiteten Typen. Jede Instanz der Klasse enthält einen tag, der den spezifischen Typ angibt. Wenn man diese Typen in Parametern verwendet sind sie unterschiedlich vom spezifischen Typ und bleiben bei ableitung gleich -> invariant -> erfüllt Ersetzbarkeitsprinzip. 

## Wann braucht man in Ada dynamisches Binden?

Wenn spezifische Typen von Argumenten dem Compiler bekannt sind dann reicht statisches Binden, d.h. eine überladene Funktion kann statisch festgelegt werden. Wenn man aber klassenweite Typen als Argument verwendet, kann man die Operation erst mit dem tag ermitteln -> dynamisch. 

## Unterschied Single- und Multiple-Dispatching

Bei Eingangsargumenten kann es dynamische Typen geben, weswegen man erst zur Laufzeit Einzelroutinen aussuchen kann, was auch als dynamisches Binden bekannt ist.

Wenn man nur über ein einzelnes Argument verwendet um die Routine auszuwählen hat man single dispatching, wenn man mehrere beliebige Argumente verwendet hat man multiple dispatching.

## Warum reicht in Ada Single Dispatching aus?

Multiple dispatching ist um einiges komplexer. deswegen wird immer nur anhand des ersten Parameters entschieden in Ada. Außerdem bietet Ada schon Möglichkeiten für kovariantes Subtyping an.

## Typinferenzalgorithmus erklären mit jedem Fall von PT. Was ist in den Gamma Umgebungen drinnen? Worst Case Laufzeit? Warum occurs so teuer?

### PT

funktioniert nur für monomorphe Typsysteme, für polymorphe Typsysteme bräuchte man den Semiunifikator welcher unentscheidbar ist. 

c Konstante, x Parametername, v Typparameter, s&t Typen, e untypisierter Lambdaausdruck, f typisierter Lambdaausdruck, G ist eine Umgebung mit Typzuweisungen and Parameternamen.

PT(c) = {} |> c:t
*Konstanten erhalten ihren Typ, z.B. 1 ist ein int*

PT(x) = {x:v} |> x:v
*Ein Parametername erhält einen neuen Typparameter*

PT(e e') = let G  |> f :t = PT(e);
               G' |> f':t' = PT(e');
*Funktion und Argument werden rekursiv typisiert und die verwendeten Typzuweisungen in Umgebungen geschrieben.*
               theta = unify({s = s' | x:s \in G; x:s' \in G'} U
                             {t = t' -> v})
           in thetaG U thetaG' |> theta(f f'): thetav
*Typparameter werden aneinander gebunden und an die Typen welche sie erhalten haben.Ebenso wird der typ von der Funktion definiert (als (t' -> v)). Siehe auch 'unify'*

PT(lx.e) = let G |> f:t = PT(e)
*Ausdruck wird rekursiv typisiert*
           in if x:s \in G für beliebiges s
*Wenn Lambdaparameter im Body der Abstraktion typisiert wurde.*
              then G \ {x : s} |> (lx:s.f):s->t
*Lösche Typisierung da x gebunden wird und außerhalb der Abstraktion anders verwendet wird.*
              else G |> (lx:v.f):v -> t
*Wenn nicht, dann ist der Typ beliebig und wir setzen einen neuen Parameter ein*

### Unify

unify({}) = {}
*Leere Mengen sind trivialerweise unifiziert*

unify(E U {b = b'}) = if b != b' then fail
                      else unify(E)
*Wenn spezifische Typen ungleich sind, aber gleich sein müssen, dann schlägt die Unifizierung fehl*

unify(E U {v = t}) = if v = t then unify(E)
*Wenn v ident zu t dann können wir es weglassen, weil schon spezifisch*
                     else if v occurs in t then fail
*Wenn v in t ist dann kann es zu einer unendlichen Rekursion kommen, weswegen wir es abbrechen*
                     else unify([t/v]E) + [t/v]
*Wenn v t beinhaltet, dann kann es durch t ersetzt werden*

unify(E U {s -> s' = t -> t'}) = unify(E U { s = t, s' = t'})
*Zum Aufschlüsseln von Funktionen. Ausgangs, Eingangsparameter werden gleichgesetzt wenn Funktionen gleich sind.*

Das Ergebnis ist demnach ein fail wenn es Konflikte mit Typen gab oder wenn es zu einer Verschachtelung von Typparametern kommt. Zweiteres wird vom occurs gecheckt. Dieser check kann uU exponentiell sein. Ansonsten ist der Algorithmus linear.

Wenn es nicht failed, dann beinhaltet das Ergebnis eine Reihe an Typzuweisungen für Typparameter.

## Formel für Subtyping von Verbunden, rekursiven Typen

Rekursiver Typ:
baum = {i:int, l:baum, r:baum}

Alpharegel:

mv.t = mu.[u/v]t (u not in free(mv.t))

Faltungsregel:

mv.t = [mv.t/v]t

* Wenn kein v in t dann sind mv.t und t äquivalent, also t ist ein Fixpunkt
* sonst kann man den Typen selber in v einsetzen, also auffalten. Kann uU unendlich passieren. 

Subtyping-Regel:

G U {u <= v} |- s <= t 
---------------------- (u not free in t, v not free in s, u&v not free in G)
G |- mu.s <= mv.t

G leitet genau dann mu.s <= mv.t ab, wenn G U {u <= v} s<=t ableitet
d.h wenn die rekursionsfreien Typen Untertypen sind, sind es auch die mit Rekursion unter Annahme dass u <= v.

### Beispiel 

mu.{f: u -> u; x:u} !<= mv.{f:v->v}

Wir haben die Annahme u <= v. Durch das Ersetzungsprinzip von Funktionen sind die beiden Typen in keiner Untertypbeziehung, weil u -> u kein Untertyp von v -> v ist gegeben der Annahme. 

## Higher-Order Subtyping

Ist ein wenig anders als bei normaler Subtypbeziehung rekursiver Typen. Hier gilt S <# T wenn S[U] <# T[U] für alle Typen gilt. 

### Beispiel

{f: u -> u; x:u} <# {f: v -> v}

Das hier gilt, weil wir nicht die komplette Regel von vorhin mit u <= v annehmen sondern nur u == v. 

## F-gebundene Generizität + Vererbung, binäre Methoden, Ersetzbarkeit

Bei F-gebundener Generizität gilt S <= T[S]

Ein Beispiel damit ist in Java der Einsatz des generischen Comparable Typs:

```java
interface Comparable<T> {
  int compareTo(T that);
}

class Integer implements Comparable<Integer> {
  int compareTo(Integer that);
}
```

Dadurch setzt man den Eingangsparameter von compareTo mittels Typparametern und nicht mittels Subtyping. 
Achtung gilt hier bei Subtypen, weil wenn S <= T[S] gilt und U <= S gilt nicht U <= T[U] sondern U <= T[S]
Mit wildcards kann man dem entgegenwirken, aber die Zugriffe werden eingeschränkt => extends nur lesend, super nur schreibend. 

Binäre Methode ist eine wo der Typ als Eingangsparameter doppelt vorkommt wie bei compareTo (Objekttyp + nochmal in der Methode)