TU Wien:Typsysteme VO (Puntigam)/Output einer Lerngruppe

Warnung: Der folgende Text ist ein verlustbehafteter Mitschnitt unserer Lerngruppe. Teilweise werden Fragen gestellt, manchmal diese beantwortet oder einfach nur Anregungen zu Diskussionen gebracht.

Warnung': Da wir morgen Prüfung haben ist der Text keineswegs konvergiert - (\x . x x) (\x . x x)!

1) Was ist ein Typ?

2) Motivation aus Sicht vom

Programmierer: Klassifikation von Werten, Schutzschilder gegen unbeabsichtigte Interpretation, Unterstützung bei der Programmerstellung Compilerbauer: Typen schränken Ausdrücke syntaktisch ein, Speicherauslegung für Werte, Sprachdesigner: Verhaltinsvarianten, Regeln um jedem Ausdruck einen allgemeinsten Typ zuzuordnen,

Sicherheit, Flexibilität, Einfachheit

==> ein Typ beschreibt eine Menge von Instanzen

3) Passive Objekte/Aktive Objekte.

4) Typspezifikation: Extensional - Intensional

5) Einteilung von Typstemen

Vollständig Typisiert: Alle Ausdrücke Typkonsistent (wird überprüft - spätestens zur Laufzeit) - zB.: C - Arraygrenzen (C hat löcher) Stark: Alle Typfehler werden zur Übersetzungszeit erkannt (aber nicht jeder Ausdruck hat einen Eindeutigen Typ) Statisch: Der eindeutige Typ jedes Ausdrucks ist statisch festgelegt. (Stark/Statisch gilt nur für Typisierten Teil)

Typkonsistent: wenn die Operanden den vom Operator erwarteten Typ haben (Typkonsistenz nicht gleichbedeutend mit "Qualität" des Typsystems)

Optimisitisch (oft interpretierte Sprachen, bricht nicht ab wenn Typkonsistenz nicht garantiert ist) vs Konservative Übersetzung

Durchlässigkeit - ob Löcher vorhanden sind. Löcher sind Konstrukte, die verbotene Dinge nicht entdecken (zB.: aus Performancegründen)

Typäquivalenz

a) Strukturgleicheit (zB.: typedef in C)
b) Namensgleichheit (zB.: struct in C)

6) ADTs: verstecken interne Implementierung und von außen kann nur auf exportierte Operationen zugegriffen werden.

7) Abstrakte Typen: nicht vollständig spezifizierter Typ (generische Typen)

8) Polymorphie

9) Typumwandlung: im Gegensatz zu Overloading eine semantische Operation

Theoretische Konzepte

---

1) Lambda Kalkül (Syntax & Semantik) 2) Experimente

--fix :: (a -> a) -> a

fix f = f (fix f)

--fac':: (Int -> Int) -> Int -> Int

fac' f n = if n<=1 then 1 else n * (f (n-1) )

fac n = if n<=1 then 1 else n * (fac (n-1))

fac = fix fac'

type Church a = (a -> a) -> (a -> a)

church :: Integer -> Church Integer

church 0 = \f -> \x -> x

church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer

unchurch n = n (\x -> x + 1) 0

plus = \m -> \n -> \f -> \x -> m f (n f x)

Für strict Evaluation:

module Fix

//let rec fix f = f (fix f) // THIS ONE FAILS

let rec fix f x = f (fix f) x

let fac' f n = if n<=1 then 1 else n * (f (n-1) )

let rec fac n = if n<=1 then 1 else n * (fac (n-1))

//let fac = fix fac'

3) (Simply)Typed Lambda Calculus

Y-Combinator lässt sich mit den Typ-Regeln nicht anschreiben

Deswegen Delta-Regel, welche den Y-Combinator quasi in die Sprache nehmen.

4) PER Modell

bietet das theoretische MOdell um Subtyping nicht nur auf die Werteteilmenge zu definieren sondern auch dass untertypen (bei verbunden) mehr elemente enthalten als der obertyp.

5) Logische Sprachen

Verfahren zur Auswertung: Bottom Up: alle Fakten in Working Set, all Ableitebaren Regeln in Working, ... bis fipunkt. Die enstehende (im allgemeinen unendlich Große) Menge beschreibt alle Abfragen - Ziel element dieser Menge -> Bewiesen/Top Down: Backward Reasoning ausgehend vom Ziel aus - In jedem Schritt wird Unifikation angewandt.

6) Typisierte Logische Programme

Externes Typsystem (selbe funktionaität wie sprache) oder Typ-Checking über Sprachfeatures (prädikate für typen). Nachteil - man sieht nicht ob Typfehler oder nicht Beweisbar (was ist der unterscheid ;-)). Nachteil - Typfehler brauchen länger, weil Backtracking eventuell ausgeführt wird.

7)

- Universelle Algebren $(A,\Omega )$ [Trägermenge + Operationen]

- Varietät $V(\Omega ,\Delta )$ [Operationen + Gesetzte]

- Signatur: Ist die Menge der Operationen und deren Stelligkeit (entspricht Schnittstellenbeschreibung eines ADT oder vgl. ML signatur)

- Freie Algebren: $V(\Omega ,\Delta )$ - Algebren in denen keine Gesetze gelten, die nicht aus Delta ableitbar sind

- Heterogene Algebren (Many-Sorted): Mehrere Trägermengen - Jede Menge hat einen namen (Sort(Sorte)).

Sorten werden ein Teil er heterogenen Algebren - also kann man Operationen nicht mehr unabhängig von der Trägermenge definieren - Die Sorten sind durch Operationen aneinander gebunden, und deswegen nicht Unabhängig. Dadurch müsste man sinnvolle Programme (durch diese Abhängigkeiten) in einer Algebra darstellen. Die Lösung für dieses Problem sind Generische Sorten - "Mit parametrischen Typen sind heterogene Algebren tats ̈chlich mähtige Werkzeuge zur Spezifiakation von Programmen im Allgemeinen und von abstrakten Datentypen im Besonderen."

8) Prozessalgebren: Dienen zur Spezifikation von nebenläufigen Prozessen

9) Was ist cool an ADAs Typsystem?

10) Order-Sorted Algebras - Auf die Sorten (Namen der Trägermengen) definiert man eine Halbordnung

11) Verbände über Sortenmengen - Infimum Supremum,....

12) Polymorphe Operationen: Eingangsparameter können ein Untertyp des parameters sein. Ausgangsparameter können Obertyp vom formalen Parametertyp sein