Typsysteme (5. 1.)

Typ-Prüfungen

$$Id: typ.tex,v 1.1 2004/01/05 14:12:41 joe Exp $$

Typ: eine Menge von Daten und zugeörigen Operationen.

Typ-Prüfung: Test, ob gegebenes Datum zu gewünschter Menge gehört.

• Typ-Deklarationen sind hervorragende Dokumenationen (warum?)

Typfehler sind Vorboten von Laufzeitfehlern.

Statische Typ-Prüfung: jedes Objekt, jeder Bezeichner hat genau einen Typ. Dieser ist bereits zur Kompile-Zeit bekannt.

Vorteile:

• frühestmögliche Fehlererkennung
• keine Laufzeit-Typtests/information nötig

Arten von Typen

Einfache Typen:

• Aufzählungstypen (Boolean, Char, Int, selbst definierte)
• andere Zahltypen (Float, Double)

Zusammengesetze Typen:

• Produkte,
• Summen,
• Exponentiale.

zusammengesetzte Typen: Produkte

• unbenannt: Tupel type T = ( T1, T2 )

  entspricht $T = T_1 \times T_2$

• benannt: Records, Structs, Objekte, ... data T = C { f1 :: T1, f2 :: T2 }

  ist isomorph zu $T = T_1 \times T_2$

  Konstruktor: $C :: (T_1 \times T_2) \to T$

  Destruktoren: $f_i :: T \to T_i$

zusammengesetzte Typen: Summen

• unbenannt (z. B. union in C) $T = T_1 \cup T_2$ (gefährlich)
• benannt (z. B. record .. case .. of .. in Pascal)

  (Aufzählungstypen sind Spezialfall!)

  data T = C1 { ... } | C2 { ... }

  ermöglicht Fallunterscheidungen:

  case (x :: T) of C1 {} -> ... ; C2 {} -> ...
  

  (enthält if/then/else als Spezialfall!)

Aufgabe: warum gibt es keine Summen in Java? Was soll stattdessen benutzt werden?

zusammengesetzte Typen: Exponentiale type T = T1 -> T2

entspricht $T = T_2^{T_1} = \{ f \mid f : T_1 \to T_2 \}$.

Wesentliche Regel:

wenn $f :: T_1 \to T_2$ und $x :: T_1$, dann $f(x):: T_2$.

(vergleiche Aussagenlogik: aus $p_1 \to p_2$ und $p_1$ folgt $p_2$.)

In vielen Sprachen gibt es Exponential-Typen nur versteckt in Funktionsdeklarationen, d. h. statt

(T1 -> T2) f; // Deklaration,
f = \ x -> { return 2 * x + 7; } // Zuweisung, anonyme Funktion

schreibt man

T2 f (T1 x) { return 2 * x + 7; }

Ganz ganz einfaches Typprüfen

$$Id: simpel.tex,v 1.1 2004/01/05 14:12:41 joe Exp $$

Wenn die Sprache nur wenige Typen hat (Beispiel: int und boolean), dann kann man die Typprüfung in die Grammatik verlegen:

statt Ausdruck -> ... benutze

Int_Ausdruck -> ...
Bool_Ausdruck -> ...

Verzweigung -> if Bool_Ausdruck then Anweisung

Zeiger-Typen

$$Id: zeiger.tex,v 1.1 2004/01/14 10:48:34 joe Exp $$

in einigen Sprachen gibt es den Typ-Konstruktor ,,Zeiger auf``

(in C und Pascal. In Java nicht, bzw. Objekt-Zeiger sind implizit.)

• Programierung: Zeiger erlauben Sharing von Speicherbereichen
• Implementierung: Zeiger brauchen (viel) weniger Platz als das Objekt, auf das sie verweisen

Mengentheoretisch: Zeigertyp ^t ist benannte Vereinigung von null (,,leerer Zeiger``) und t.

Typ-Ausdrücke, Abstrakte Interpretation

$$Id: abstrakt.tex,v 1.1 2004/01/14 10:48:34 joe Exp $$

Typen werden im Compiler durch Typ-Ausdrücke (Bäume) repräsentiert. (Beispiele.)

Bei der Kompilation von Ausdrücken der Quellsprache wird für jeden Teilausdruck sein Typ(-Ausdruck) berechnet.

Das ist eine Art von abstrakter Interpretation.

• konkrete Interpretation (auf Daten): berechne Wert.

  4 + strlen ("foo") -> 4 + 3 -> 7
  

• abstrakte Interpretation (auf Typen): berechne Typ

  4 + strlen ("foo") -> int + strlen (char *) 
       -> int + int -> int
  

Typ-Regeln

• Typen von Literalen sind bekannt
• Typen für Bezeichner ((lokale) Variablen, formale Parameter) sind vom Programmierer deklariert
• für zusammengesetzte Ausdrücke der Form $A = f(A_1, \ldots, A_n)$
  • die Typen der Argument-Ausdrücke sind schon (rekursiv) berechnet: $A_1 :: T_1, \ldots, A_n :: T_n$
  • der Typ der Funktion ist bekannt: $f :: ( S_1 \times \ldots \times S_n ) \to S$
  • die Argument-Typen müssen passen: $T_1 = S_1, \ldots$
  • dann ist Typ des Ausdrucks $A :: S$.
  entspr. für Operator-Ausdr. sowie Array- und Zeiger-Zugriffe.

Vergleich von Typ-Ausdrücken

$$Id: gleich.tex,v 1.1 2004/01/14 10:48:34 joe Exp $$

oft gibt es Namen für Typen:

typedef int * T1;
T1 x1;
typedef int * T2;
T2 x2;

sind jetzt $T_1$ und $T_2$ gleich?

• strukturelle Gleichheit: ja
• Namesgleichheit: nein

strukturelle Gleichheit erlaubt (ein wenig) Polymorphie

Namensgleichheit erlaubt stärkere Kontrolle (bessere Fehlererkennung)

Rekursive Datentypen

$$Id: rekurs.tex,v 1.2 2004/01/14 11:47:14 joe Exp $$

struct T {
    int contents;
    struct T * next;
}

entspricht Gleichung

$T = \verb*\vert int\vert \times (\verb*\vert null\vert \cup T)$

vergleiche diese Gleichungen für Funktionen:

int f (int x) {
 if ( x < 100 ) 
  return x - 10;
 else 
  return 
   f (f (x + 11));}

int t (int x, int y, int z) {
  if (x <= y) { return y; }
  else return 
    t ( t ( x-1, y, z)
      , t ( y-1, z, x)
      , t ( z-1, x, y) ); }

Gleichungen für Zahlen:

int y = y + 4;    double x = 2 + 3 * x / 4;

eine (rekursive) Gleichung (für Typen, Funktionen, Zahlen) kann keine, eine oder mehrere Lösungen haben.

Repräsentation rekursiver Typen

struct T {
    int contents;
    struct T * next;
}

$T = \verb*\vert int\vert \times (\verb*\vert null\vert \cup T)$

kann im Kompiler so dargestellt werden:

• strukturell: (Rückwärts-)Zeiger im Typ-Ausdruck

  (Vorsicht: Typvergleich muß trotzdem immer terminieren)

• benannt: (eigener) Typname im Typ-Ausdruck

Sprache C benutzt (u. a. deswegen)

• Namensgleichheit für structs,
• und strukturelle Gleichheit sonst.

Typprüfung bei Zuweisungen

$$Id: zuweis.tex,v 1.1 2004/01/14 10:48:34 joe Exp $$

Die übliche Notation a := b; ist irreführend, denn in Zuweisung $l := r$ bezeichnet:

• $r$ einen Ausdruck mit Typ $T$
• $l$ eine Adresse (einen Zeiger) auf $T$

es ist üblich, auch $l$ als Ausdruck vom Typ $T$ zu schreiben.

Bei Ausführung der Zuweisung (im kompilierten Code) wird von $l$

• nicht der Wert (rvalue),
• sondern der Adress-Wert (lvalue) bestimmt.

Nicht jeder Ausdruck $l :: T$ besitzt einen Adress-Wert.

Implizite Typumwandlungen (Erweiterungen)

Für einen (Teil-Ausdruck) $A$ wurde Typ $T$ berechnet,
aber Typ $S \neq T$ ist verlangt:

kann gestattet werden, falls $T \subseteq S$,

oder falls es eine (durch Sprachdefinition festgelegte) Abbildung (Einbettung) $T \to S$ gibt
(Code dafür wird dann vom Kompiler eingebaut)

C: int $\to$ long, int $\to$ float, char $\leftrightarrow$ int

Java: von Object $\to$ String

ist Fehlerquelle (versteckter Code)

Aufgabe (Wdhlg): an welchen Stellen können solche Umwandlungen vorkommen? (D. h.: wann wird Gleichheit von Typen geprüft?)

Explizite Typumwandlungen (Zuschnitte)

C, Java: casts, coercions, z. B. von Typ Object nach eigener Klasse

durch T x; S y = (S)x; behauptet der Programmierer: Wertebereich von $x \subseteq S$,
und der Kompiler muß es glauben.

ist Fehlerquelle (Behauptung wird nicht geprüft).

Typischer Fall: Collections in Java.

nur notwendig, wenn das Typsystem der Sprache
nicht in der Lage ist, das Wissen/die Absicht der Programmierers auszudrücken.

(D. h. Sprache ist für Programmierung ungeeignet. :-)

Statische Polymorphie (Überladung)

$$Id: over.tex,v 1.2 2004/01/14 10:48:34 joe Exp $$

Polymorphie (wörtlich): Viel-Förmigkeit

(in Programmiersprachen): der gleiche Bezeichner steht für verschiedene Dinge.

statisches Überladen:

es gibt $f_1 :: T_1$ und $f_2 :: T_2$, aber beide $f_i$ heißen nur $f$. Bei jeder Benutzung von $f$ ist zu entscheiden, welches $f_i$ gemeint ist.

in Java ist Überladen von Bezeichnern $f_1, f_2, \ldots$ nur erlaubt, wenn alle $f_i$ Unterprogramme sind, die sich in den Argumentlisten (Länge und Typen) unterscheiden.

Damit wird erreicht, daß der Kompiler alle Typen bottom-up (ohne Backtracking) bestimmen kann.

Typkonstruktoren

$$Id: constructor.tex,v 1.1 2004/01/14 11:47:14 joe Exp $$

Ein Typkonstruktor (z. B. ,,Liste von``) bildet zu einem Argumenttyp einen Ergebnistyp (z. B. String = List Char)

in Haskell (generisch mit Typ-Parameter elt)

data List elt
  = Nil 
  | Cons { head :: elt, tail :: List elt }

vgl. in C (nicht generisch):

typedef struct list 
  { elt head; struct list * tail; }

Der Listen-Konstruktor

Tatsächliche Notation in Haskell benutzt eckige Klammern:

• Typname: nicht List elt, sondern [ elt ]
• Konstruktoren:
  • nicht Nil, sondern [],
  • nicht Cons {head = x, tail = ys}, sondern x : ys
• Literale: [ "foo", "bar" ], [ 1 .. 100 ]

Welche Typen haben die Funktionen head, tail, Cons (:) ?

welchen Type hat die Funktion f x = head ( head x ) ?

Polymorphe (generische) Programme

Ein Unterprogramm ist generisch, wenn es (bei gleichem Code) auf verschiedenen Argumenttypen operieren kann

length :: [ a ] -> Int
length l = case l of
    []     -> 0
    x : xs -> 1 + length xs

append :: [a] -> [a] -> [a]
append l r = case l of
    []     -> r
    x : xs -> x : append xs r

Typprüfung von polymorphen Ausdrücken

Die Typ-Ausdrücke können Variablen enthalten.

Beim Vergleich von Typen muß der tatsächliche Typ $T$ auf den geforderten Typ $S$ passen:

d. h. es muß möglich sein, die Typ-Variablen aus $S$ so durch Typ-Ausdrücke zu ersetzen, daß $T$ entsteht.

length [ ["foo", "bar" ], [ "frob" ], [] ]
  [ ["foo", "bar" ], [ "frob" ], [] ] 
    :: [[String]]
  length 
    :: [a] -> Int
Ersetzung mit  a = [String]

Generische Programmierung

polymorphe (Container-Typen) $+$ polymorphe Funktionen höherer Ordnung $\Rightarrow$ sehr praktisch.

map :: (a -> b) -> [a] -> [b]
map f l = case l of
    []     -> []
    x : xs -> f x : map f xs

Aufgabe: welchen Typ muß $f$ haben, damit das korrekt ist:

x :: [ Int ]
x = map f "foobar"

Welchen Typ hat

g = map map