Typsysteme

Hauptstudium Informatik und Mathematik
SS 2007
Vorlesung: Mi 14-16 Uhr, Oettingenstr. 67, Oe 1.15, Do 12-14 Uhr, Oe 0.33, Prof. Martin Hofmann, Dr. Andreas Abel
Übung: Fr 12-14 Uhr, Oettingenstr. 67, Oe 0.37, Dr. Andreas Abel
Schein: ja (50% Übungspunkte)
SWS: 4 Vorlesung + 2 Übung

Aktuelles

  • Die Vorlesung ist beendet.

Zeitplan

Datum Dozent Stoff Material
18.04. VL H,A Einleitung; λ-Kalkül Pierce 5.1+3
Der λ-Kalkül ist der Kern funktionaler Programmiersprachen (Scheme, ML, Haskell), auch imperative und objektorientierte Sprachen können in ihm simuliert werden. Typsysteme werden gewöhnlicherweise für idealisierte Programmiersprachen, Erweiterungen des λ-Kalküls, entworfen und studiert, da eine in die Tiefe gehende, systematische Behandlung nur für eine Sprache mit einer kleinen Zahl von Konstrukten sinnvoll erfolgen kann. Ist ein Typsystem für den (oder eine Erweiterung des) λ-Kalkül(s) verstanden und verifiziert, kann es auf reichere Sprachen übertragen werden.

Stoff: Syntax des λ-Kalküls, freie und gebundene Variablen und α-Äquivalenz, β-Gleichheit, Substitution.

19.04. VL A Einfach getypter λ-Kalkül (STL) Pierce 9.1+2
Typen dienen u.a. dazu, bestimmte Laufzeitfehler, wie z.B. Addition einer Zahl zu einer Funktion, auszuschliessen. Ein Typsystem ist korrekt, falls die Auswertung eines wohlgetypten Programmes zu keinem Fehler führt. Vorbereitung auf den Beweis dieses Theorems: Grammatik für einfache Typen, Typisierungskontexte als endliche Abbildungen, induktive Definition der Typisierungsrelation, Überblick Auswertungsstrategien, induktive Definition der Call-By-Value(CBV)-Ein-Schritt-Reduktion.
20.04. Ü A Induktion, Big-Step-Semantik, De Bruijn Repräsentation Übungsblatt 1 Teillösung: stl.sml
25.04. VL A Typsicherheit
Typinferenz an Beispielen 		Pierce 8.3,9.3; Wright & Felleisen, A syntactical approach to type soundness
Ein wohlgetypes Programm (geschlossener Term) ist entweder ein Wert (also schon fertig ausgewertet) oder er lässt sich reduzieren (Fortschritts/progress-Theorem). Reduktion verändert den Typen nicht (Typerhaltungs/preservation/subject reduction-Theorem). Zusammen ergibt sich (mit Koinduktion), dass ein wohlgetyptes Programm fehlerfrei auswertet, d.h. entweder ergibt sich ein Wert nach endlich vielen Reduktionsschritten, oder das Programm divergiert.

Typinferenz für den STL wurde an Beispielen erläutert. Definition von Substitution, Komposition von Substitutionen, Instantiierungs-Quasi-Ordnung auf Substitutionen.

26.04. VL A Typinferenz für einfache Typen und let Mitchell 11 (Pierce 22)
Definition Unifikationsproblem und Algorithmus für den allgemeinsten Unifikator (most general unifier, mgu). Typinferenz-Algorithmus für den STL als induktive Relation; Eingabe: ein Term; Ausgabe: eine Typisierung, d.h., ein allgemeinster Typ des Termes und ein Typisierungskontext mit den Typen der freien Variablen des Terms. Typsubstitutions- und Abschwächungslemma (Weakening) für den STL, Korrektheit und Vollständigkeit der Typinferenz. Erweiterung auf let mit der naiven Typregel: let x=s in t ist wohlgetypt, wenn s und t[s/x] wohlgetypt sind. Typinferenz für let nach Mitchell, mit einer endlichen Abbildung von let-gebundenen Variablen auf Typisierungen.
27.04. Ü A Unifikation und Typinferenz Übungsblatt 2 Teillösung: unify.sml inferSTL.sml
02.05.-10.05. VL H Relationale Semantik von Seiteneffekten ASCII Skript
11.05. Ü A Effekttypisierung Übungsblatt 4
16.05. VL A Polymorphismus: ML
17.05. Christi Himmelfahrt
18.05. Ü A Algorithmus W Übungsblatt 5 aux.sml unify.sml ml_stub.sml
23.05. VL A System F
24.05. VL H Fsub: System F mit Subtyping ASCII Skript
25.05. Ü Beringer Übungsblatt 6
30.05. VL H Unentscheidbarkeit von Fsub ASCII Skript. Siehe auch Originalarbeit von Pierce . In der VL wurde allerdings ein neuer Beweis gegeben.
31.05. VL H On Decidability of Nomial Subtyping with Variance von Kennedy und Pierce.
01.06. Ü A Objektkodierungen in Fsub Übungsblatt 7
06.06. VL A entfällt
07.06. Fronleichnam
08.06. Ü A entfällt
13.06. VL A System Fω
Beispiele für Typkonstruktoren: List, Produkttypkonstruktor, Monade. 3 Ebenen von Fω: Arten (kinds), Typ(konstruktor)en, und Terme/Programme. Wohlgeformtheit von Typkonstruktoren (kinding), deklarative βη-Gleichheit von Typkonstruktoren, Typisierung von Termen im Curry-Stil und im Church-Stil.
14.06. VL A System Fω: Bidirektionale Konstruktorgleichheit
Bidirektionales Kind-Checking für Typkonstruktoren in β-Normalform. Bidirektionale algorithmische βη-Gleichheit von Typkonstruktoren.

Einführung in abhängige Typen anhand bekannter Beispiele: Vektoren und Matrizen in der Mathematik, Quantifikation in der Logik, die sprintf-Funktion, bekannt aus der Programmiersprache C, in Cayenne/Agda.

15.06. Ü A System Fω Übungsblatt 8 state-stub.sml
20.06. VL A Abhängige Typen: LF und Twelf LF-Dateien: vec.tgz
Das Logische Rahmenwerk (engl. logical framework) ist der λ-Kalkül, abhängig typisiert. Man spricht von abhängigen Typen, falls ein Typ von einem Term abhängen kann. Twelf ist eine Implementation von LF, in der man Signaturen von Typfamilien und Termkonstanten und -definitionen Typ-Checken kann. Die Typfamilien koennen als Logikprogramme ausgefuehrt werden (Beweissuche). Die Traces der Logikprogramme werden selbst wieder as LF-Terme gespeichert.
Twelf Homepage
21.06. VL A Abhängige Typen: Definition von LF LF-Dateien: hoas.tgz
Beispiel: Repraesentation von ungetypten Lambda-termen in Higher-Order Abstract Syntax (HOAS). Einmal als starke HOAS, andermal as schwache. Typregeln fuer LF. Variante von LF: Canonical LF. Hier werden alle Terme in langer Normalform gehalten, Typ-Checking ist bidirektional.
Literatur: Bob Harper, Dan Licata, Mechanizing Metatheory in a Logical Framework.
22.06. Ü A LF und Twelf Übungsblatt 9 slist.cfg slist.elf
Praesenzuebung: Aussagenlogik in LF. logic.cfg logic.elf
27.06. VL H Parametrizitaet I
Theorems for free (P Wadler) . Bis einschl.\ 3.7, ausserdem gezeigt, dass die einzigen parametrischen Elemente der Codierung von Bool in System F gerade die beiden Wahrheitswerte sind. Satz von Loader (Definierbarkeit im einfach typ Lambdakalkuel ist unentscheidbar) und Zshg mit Parametrizitaet erwaehnt.
Hintergrund: Types, Abstraction, and Parametric Polymorphism (John C Reynolds) .
28.06. VL H Parametrizitaet II
Theorems for Free zuende. PER Modell als Instanz eines Frame Modells. Abadi-Plotkins logic for parameteric polymorphism .
29.06. Ü ? entfällt
04.07. VL A Martin-Löf Typentheorie I
Martin-Löf beschreibt eine offene Typentheorie in der neue Typen nach dem Schema Formation-Einführung-Beseitigung-Berechnung hinzugefügt werden können.
  • Formations-Regel: Bildungsgesetz eines neuen Typs, z.B.: Ist A ein Typ, dann auch List A.
  • Einführungs(introduction)regeln: Bildungsgesetze für die kanonischen Bewohner des Typs, z.B. nil ist ein Bewohner von List A, und falls a ein Bewohner von A und as ein Bewohner von List A ist, so bildet cons a as einen Bewohner von List A.
  • Beseitigungs-/Eliminationsregel: Regeln, die erlauben, die durch die Einführungsregeln hineingesteckte Information eines Bewohners vollständig zu verwenden. Für Listen ist der Listen-Rekursor das gültige Eliminationsprinzip.
  • Berechnungsregel: Ein β-Redex ensteht durch Anwendung einer Beseitigung auf eine Einführung. β-Redexe werden gemäß den Berechnungsregeln aufgelöst.
Zusätzlich gibt es noch Extensionalitätsprinzipien (η) für einige Typen: η-Redexe entstehen durch eine Einführung, die unmittelbar auf eine Beseitigung folgt.
05.07. VL A Martin-Löf Typentheorie II
Besprochene Typen: Sigma, Booleans, disjunkte Summe, Natürliche Zahlen, Listen, Gleichheitstyp.
06.07. Ü A Typentheorie Übungsblatt 10
11.07. VL H Amortisierte Heap-Analyse I Pr"asentation der Arbeit .
12.07. VL H Fortsetzung der Praesentation . Vorfuehrung der .
13.07.. Ü ? entfällt
18.07. VL H Typen für Daten-Sicherheit
19.07. VL A Typ-basierte Termination
Versieht man Typen mit einer Größenangabe, die Baumho¨he der sie bewohnenen Datenstrukturen begrenzt, kann man die Verwendung von Rekursion so beschräken, dass ein Typchecker die Terminierung der Rekursion überprüfen kann. (Die Menge der typkorrekten Programme ist damit natürlich nicht mehr Turing-vollständig!) Literatur:
  • Hughes, Pareto, and Sabry: Proving the Correctness of Reactive Systems using Sized Types (POPL 2007)
  • Abel, Type-Based Termination (2007, Buchfassung meinerer Doktorarbeit)

Inhalt

Typen dienen in Programmiersprachen dazu, überladene Operationen zu übersetzen, gewisse Fehler schon bei der Übersetzung eines Programms abzufangen, die Lesbarkeit des Programmcodes zu erhöhen und bei der Suche einer gewünschten Funktion in einer Bibliothek zu helfen. Fortgeschrittene Typsysteme werden für die statische Analyse von Programmen verwendet, z.B. in Übersetzern, und um gewisse Programmeigenschaften zu spezifizieren und automatisch zu überprüfen.

In der Vorlesung werden allgemeine Methoden für Typinferenz und Typüberprüfung behandelt und verschiedene Typsysteme vorgestellt, unter anderem: die neuesten Typsysteme für JAVA und C#; Typsysteme für Polymorphismus; abhängige Typen, mit denen sich vollständige Spezifikationen notieren lassen; Typsysteme, die Termination garantieren; Security-Typsysteme, die Daten vor unbefugtem Zugriff schützen; und Ressourcen-Typen, die die Einhaltung von Speicherplatzschranken sicherstellen.

Literatur

  • "Pierce": Types and Programming Languages, Benjamin C. Pierce, MIT Press, 2002
  • "Mitchell": Foundations for Programming Languages, John C. Mitchell, MIT Press, 1996. Lambda Calculi with Types, Henk Barendregt, im Handbook of Logic in Computer Science, Band 2, Oxford University Press, 1993

WWW-Ressourcen

Valid HTML 4.01!
Andreas Abel
Last modified: Tue Jul 24 18:08:06 CEST 2007 		Valid CSS!