Main 8
Main 8
Main 8
• Induktionsschritt: x == h : t . . .
test1 = smallCheckI
(associative (append::[Int]->[Int]->[Int]))
Übung: Kommutativität (formulieren und testen)
– Typeset by FoilTEX – 4 – Typeset by FoilTEX – 5
Literatur Übungen
• Skripte: • im Pool Z430, vgl. http://www.imn.htwk-leipzig.
– aktuelles Semester http: de/˜waldmann/etc/pool/
//www.imn.htwk-leipzig.de/˜waldmann/lehre.html
• Beispiele f. deklarative Programmierung
– vorige Semester http://www.imn.htwk-leipzig.de/
– funktional: Haskell mit ghci,
˜waldmann/lehre-alt.html
– logisch: Prolog mit swipl,
• Entwurfsmuster: http://www.imn.htwk-leipzig. – constraint: mit mathsat, z3
de/˜waldmann/draft/pub/hal4/emu/ • Haskell-Entwicklungswerkzeuge
• Maurice Naftalin und Phil Wadler: Java Generics and – (eclipsefp, leksah, . . . , http://xkcd.org/378/)
Collections, O’Reilly 2006 – API-Suchmaschine http://www.haskell.org/hoogle/
• Commercial Uses of Functional Programming
• http://haskell.org/ (Sprache, Werkzeuge,
http://www.syslog.cl.cam.ac.uk/2013/09/22/
Tutorials), http://book.realworldhaskell.org/
liveblogging-cufp-2013/
Vervollständigen Sie die Definition der Tiefe von Termen: Abkürzung für Anwendung von 0-stelligen Symbolen:
anstatt Z() schreibe Z.
• für S = {A(A(D, x), y) → A(x, A(x, y))} bestimme Normalform von Ak (B(E))
... -> ... data List = Nil | Cons Bool List deriving Prelude.S
• beweise:
forall xs . reverse (reverse xs) == xs
• der Typ Pair a b hat Konstruktor Pair a b. • bestimme Anzahl und Typ seiner Argumente
die Substitution für diese Typvariablen ist • wähle Werte für diese Argumente nach diesem
a = Bool, b = (). Vorgehen.
– Typeset by FoilTEX – 54 – Typeset by FoilTEX – 55
Kochrezept: Typ-Bestimmung Lösung: ist gleich dem Typ der zugehörigen
Diskriminante p
Aufgabe (Bsp.) bestimme Typ von x (erstes Arg. von get):
• bestimme das Muster, durch das p deklariert wird
at :: Position -> Tree a -> Maybe a
at p t = case t of Lösung: at p t =
Node f ts -> case p of • bestimme den Typ von p
Nil -> Just f Lösung: durch Vergleich mit Typdeklaration von at (p ist
Cons x p’ -> case get x ts of das erste Argument) p :: Position, also
Nothing -> Nothing Cons x p’ :: Position = List N, also x :: N.
Just t’ -> at p’ t’ Vorgehen zur Typbestimmung eines Namens:
Lösung:
• finde die Deklaration (Muster einer Fallunterscheidung
oder einer Funktionsdefinition)
• bestimme das Muster, durch welches x deklariert wird.
Lösung: Cons x p’ -> • bestimme den Typ des Musters (Fallunterscheidung: Typ
• bestimme den Typ diese Musters der Diskriminante, Funktion: deklarierter Typ)
– Typeset by FoilTEX – 56 – Typeset by FoilTEX – 57
Statische Typisierung und Polymorphie Bsp. für Programm ohne statischen Typ (Javascript)
Def: dynamische Typisierung: function f (x) {
if (x>0) { return function () { return 42; } }
• die Daten (zur Laufzeit des Programms, im
else { return "foobar"; } }
Hauptspeicher) haben einen Typ
Dann: Auswertung von f(1)() ergibt 42, Auswertung von
Def: statische Typisierung: f(0)() ergibt Laufzeit-Typfehler.
• Bezeichner, Ausdrücke (im Quelltext) haben einen Type entsprechendes Haskell-Programm ist statisch fehlerhaft
(zur Übersetzungszeit bestimmt). f x = case x > 0 of
True -> \ () -> 42
• für jede Ausführung des Programms gilt: der statische False -> "foobar"
Typ eines Ausdrucks ist gleich dem dynamischen Typ
seines Wertes
Nutzen der statischen Typisierung: Von der Spezifikation zur Implementierung (I)
• beim Programmieren: Entwurfsfehler werden zu Bsp: Addition von Peano-Zahlen data N = Z | S N
Typfehlern, diese werden zur Entwurfszeit automatisch plus :: N -> N -> N
erkannt ⇒ früher erkannte Fehler lassen sich leichter aus der Typdeklaration wird abgeleitet:
beheben plus x y = case x of
Z ->
• beim Ausführen: es gibt keine Lauzeit-Typfehler ⇒ keine
S x’ ->
Typprüfung zur Laufzeit nötig, effiziente Ausführung
erster Zweig: plus Z y = 0 + y = y
Nutzen der Polymorphie: zweiter Zweig : plus (S x’) y = (1 + x’) + y =
• Flexibilität, nachnutzbarer Code, z.B. Anwender einer mit Assoziativität von + gilt
Collection-Bibliothek legt Element-Typ fest (Entwickler ... = 1 + (x’ + y) = S (plus x’ y)
der Bibliothek kennt den Element-Typ nicht) Bsp. (Ü): Multiplikation. Hinweis: benutze Distributivgesetz.
Von der Spezifikation zur Implementierung (II) • substitutiere xs = Cons x1 Nil, erhalte
Bsp: homogene Listen
maximum (append (Cons x1 Nil) ys)
data List a = Nil | Cons a (List a)
= maximum (Cons x1 ys)
Aufgabe: implementiere maximum :: List N -> N
= max (maximum (Cons x1 Nil)) (maximum ys)
Spezifikation: = max x1 (maximum ys)
maximum (Cons x1 Nil) = x1
maximum (append xs ys) = max (maximum xs) (maximum Damit kann
ys) der aus dem Typ abgeleitete Quelltext
maximum :: List N -> N
• substitutiere xs = Nil, erhalte
maximum xs = case xs of
maximum (append Nil ys) = maximum ys Nil ->
= max (maximum Nil) (maximum ys) Cons x xs’ ->
ergänzt werden.
d.h. maximum Nil sollte das neutrale Element für max Vorsicht: für min, minimum funktioniert das nicht so, denn
(auf natürlichen Zahlen) sein, also 0 (geschrieben Z). min hat für N kein neutrales Element.
– Typeset by FoilTEX – 62 – Typeset by FoilTEX – 63
Unveränderliche Objekte Beispiel: Einfügen in Baum
• destruktiv:
Überblick
interface Tree<K> { void insert (K key); }
• alle Attribute aller Objekte sind unveränderlich (final)
Tree<String> t = ... ;
• anstatt Objekt zu ändern, konstruiert man ein neues
t.insert ("foo");
Eigenschaften des Programmierstils:
• persistent (Java):
• vereinfacht Formulierung und Beweis von
Objekteigenschaften interface Tree<K> { Tree<K> insert (K key); }
• parallelisierbar (keine updates, keine data races) Tree<String> t = ... ;
Tree<String> u = t.insert ("foo");
http://fpcomplete.com/
the-downfall-of-imperative-programming/ • persistent (Haskell):
• Persistenz (Verfügbarkeit früherer Versionen)
insert :: Tree k -> k -> Tree k
• Belastung des Garbage Collectors (. . . dafür ist er da)
– Typeset by FoilTEX – 64 – Typeset by FoilTEX – 65
https://www.stackage.org/lts-5.17/hoogle
– Typeset by FoilTEX – 98