Einleitung

Programmierung im Studium bisher

Worin besteht jetzt der Fortschritt?

Formen der deklarativen Programmierung

Definition: Funktionale Programmierung

Softwaretechnische Vorteile

…der funktionalen Programmierung

Beispiel Spezifikation/Test

import Test.LeanCheck

append :: forall t . [t] -> [t] -> [t]
append [] y = y
append (h : t) y = h : (append t y)

associative f = 
   \ x y z -> f x (f y z) == f (f x y) z
commutative f = \ x y -> ...

test = check
  (associative (append::[Bool]->[Bool]->[Bool]))

Übung: Kommutativität (formulieren und testen)

Beispiel Verifikation

app :: forall t . [t] -> [t] -> [t]
app [] y = y
app (h : t) y = h : (app t y)

Lemma: app x (app y z) .=. app (app x y) z

Proof by induction on List x
  Case []
    To show: app [] (app y z) .=. app (app [] y) z
  Case h:t
    To show: app (h:t) (app y z) .=. app (app (h:t) y) z
    IH: app t (app y z) .=. app (app t y) z

CYP https://github.com/noschinl/cyp,

ist vereinfachte Version
von Isabelle https://isabelle.in.tum.de/

Beispiel Parallelisierung (Haskell)

Klassische Implementierung von Mergesort

sort :: Ord a => [a] -> [a]
sort [] = [] ; sort [x] = [x]
sort xs =  let ( left,right ) = split xs
               sleft  = sort left  
               sright = sort right 
           in  merge sleft sright

wird parallelisiert durch Annotationen:

  sleft  = sort left  
              `using` rpar `dot` spineList
  sright = sort right `using` spineList

vgl. http://thread.gmane.org/gmane.comp.lang.haskell.parallel/181/focus=202

Beispiel Parallelisierung (C#, PLINQ)

vgl. Introduction to PLINQ https://msdn.microsoft.com/en-us/library/dd997425(v=vs.110).aspx

Softwaretechnische Vorteile

…der statischen Typisierung

The language in which you write profoundly affects the design of programs written in that language.

For example, in the OO world, many people use UML to sketch a design. In Haskell or ML, one writes type signatures instead. Much of the initial design phase of a functional program consists of writing type definitions.

Unlike UML, though, all this design is incorporated in the final product, and is machine-checked throughout.

Simon Peyton Jones, in: Masterminds of Programing, 2009;

http://shop.oreilly.com/product/9780596515171.do

Deklarative Programmierung in der Lehre

Beziehungen zu weiteren LV: Voraussetzungen

Anwendungen:

Konzepte und Sprachen

Funktionale Programmierung ist ein Konzept. Realisierungen:

Die Erkenntnisse sind sprachunabhängig.

Gliederung der Vorlesung

Softwaretechnische Aspekte

Organisation der LV

Literatur

Alternative Quellen

Übungen KW15

Aufgaben (Auswertung in KW 16)

  1. zu: E. W. Dijkstra: Answers to Questions from Students of Software Engineering (Austin, 2000) (EWD 1035)

    • putting the cart before the horse

      • übersetzen Sie wörtlich ins Deutsche,

      • geben Sie eine entsprechende idiomatische Redewendung in Ihrer Muttersprache an,

      • wofür stehen cart und horse hier konkret?

  2. sind die empfohlenen exakten Techniken der Programmierung für große Systeme anwendbar?

    Erklären Sie lengths of …grow not much more than linear with the lengths of ….

    • Welche Längen werden hier verglichen?

    Modellieren Sie das System als Graph, die Knoten sind die Komponenten, die Kanten sind deren Beziehungen (direkte Abhängigkeiten).

    • Welches asymptotische Wachstum ist bei undisziplinierter Entwicklung des Systems zu befürchten?

    • Welche Graph-Eigenschaft impliziert den linearen Zusammenhang?

    • Wie gestaltet man den System-Entwurf, so daß diese Eigenschaft tatsächlich gilt? Welchen Nutzen hat das für Entwicklung und Wartung?

  3. Über ein Monoid \((M,\circ, 1)\) mit Elementen \(a, b\in M\) (sowie eventuell weiteren) ist bekannt: \(a^2= b^2 = (ab)^2 = 1\).

    Dabei ist \(ab\) eine Abkürzung für \(a\circ b\) und \(a^2\) für \(aa\), usw.

    • Geben Sie ein Modell mit \(1\neq a\neq b\neq 1\) an.

    • Überprüfen Sie \(ab = ba\) in Ihrem Modell.

    • Leiten Sie \(ab=ba\) aus den Monoid-Axiomen und gegebenen Gleichungen ab.

    Das ist eine Übung zur Wiederholung der Konzepte abstrakter und konkreter Datentyp sowie Spezifikation.

  4. im Rechnerpool live vorführen:

    • ein Terminal öffnen

    • ghci starten (in der aktuellen Version), Fakultät von 100 ausrechnen

    • Datei F.hs mit Texteditor anlegen und öffnen, Quelltext f = ... (Ausdruck mit Wert 100!) schreiben, diese Datei in ghci laden, f auswerten

    Dabei wg. Projektion an die Wand:

    Schrift 1. groß genug und 2. schwarz auf weiß.

    Vorher Bildschirm(hintergrund) aufräumen, so daß bei Projektion keine personenbezogenen Daten sichtbar werden. Beispiel: export PS1="$ " ändert den Shell-Prompt (versteckt den Benutzernamen).

    Wer (unsinnigerweise) eigenen Rechner im Pool benutzt:

    • Aufgaben wie oben und

    • ssh-Login auf einen Rechner des Pools

      (damit wird die Ausrede GHC (usw.) geht auf meinem Rechner nicht hinfällig)

    • ssh-Login oder remote-Desktop-Zugriff von einem Rechner des Pools auf Ihren Rechner (damit das projiziert werden kann, ohne den Beamer umzustöpseln)

    (falls das alles zu umständlich ist, dann eben doch einen Pool-Rechner benutzen)

  5. welcher Typ ist zu erwarten für die Funktion,

    • (wurde bereits in der Übung behandlelt) die das Spiegelbild einer Zeichenkette berechnet?

    • die die Liste aller (durch Leerzeichen getrennten) Wörter einer Zeichenkette berechnet?

      f "foo bar" = [ "foo", "bar" ]

    Suchen Sie nach Funktionen dieses Typs mit https://www.haskell.org/hoogle/, erklären Sie einige der Resultate, welches davon ist das passende, rufen Sie diese Funktion auf (in ghci).

Daten

Wiederholung: Terme

Beispiele: Signatur, Terme

Algebraische Datentypen

data Foo = Foo { bar :: Int, baz :: String } 
    deriving Show

Bezeichnungen (benannte Notation)

x :: Foo
x = Foo { bar = 3, baz = "hal" }

Bezeichnungen (positionelle Notation)

data Foo = Foo Int String  
y = Foo 3 "bar"

Datentyp mit mehreren Konstruktoren

Beispiel (selbst definiert)

data T = A { foo :: Int } 
       | B { bar :: String, baz :: Bool } 
    deriving Show

Bespiele (in Prelude vordefiniert)

data Bool = False | True
data Ordering = LT | EQ | GT

Mehrsortige Signaturen

Bsp.: \(S=\{Z,B\}, \Sigma=\{0 \mapsto ([],Z), p \mapsto ([Z,Z],Z),\) \(e\mapsto ([Z,Z],B), a\mapsto([B,B],B)\}\).

Rekursive Datentypen

data Tree = Leaf {}
    | Branch { left :: Tree
             , right :: Tree }

Übung: Objekte dieses Typs erzeugen

(benannte und positionelle Notation der Konstruktoren)

Daten mit Baum-Struktur

Bezeichnungen für Teilterme

dabei bezeichnen:

Operationen mit (Teil)Termen

Operationen mit Variablen in Termen

Termersetzungssysteme

Termersetzungssysteme als Programme

dieses Berechnungsmodell ist im allgemeinen

Konstruktor-Systeme

Für TRS \(R\) über Signatur \(\Sigma\): Symbol \(s\in\Sigma\) heißt

Das TRS \(R\) heißt Konstruktor-TRS, falls:

Übung: diese Eigenschaft formal spezifizieren

Beispiele: \(R_1=\{a(b(x)) \to b(a(x))\}\) über \(\Sigma_1=\{a/1,b/1\}\),

\(R_2=\{f(f(x,y),z) \to f(x,f(y,z))\) über \(\Sigma_2=\{f/2\}\):

definierte Symbole? Konstruktoren? Konstruktor-System?

Funktionale Programme sind ähnlich zu Konstruktor-TRS.

Übung Terme, TRS

mit ghci:

Die Größe eines Terms \(t\) ist definiert durch

\(|f(t_0,\ldots,t_{k-1})| = 1 + \sum_{i=0}^{k-1} |t_i|\).

Für die Signatur \(\Sigma=\{Z/0, S/1, f/2\}\):

Notation für Termersetzungsregeln: anstatt \((l,r)\) schreibe \(l\to r\).

Abkürzung für Anwendung von 0-stelligen Symbolen: anstatt \(Z()\) schreibe \(Z\). (Vorsicht: dann kann man Variablen nicht mehr von 0-stelligen Symbolen unterscheiden. Man muß dann immer die Signatur explizit angeben oder auf andere Weise vereinbaren, wie man Variablen erkennt, z.B. Buchstaben am Ende das Alphabetes (\(\dots,x,y,\dots\)) sind Variablen, das ist aber riskant)

Abkürzung für mehrfache Anwendung eines einstelligen Symbols: \(A(A(A(A(x)))) = A^4(x)\)

Hausaufgaben (Diskussion in KW18)

  1. autotool-Aufgabe Data-1

    Allgemeine Hinweise zur Bearbeitung von Haskell-Lückentext-Aufgaben:

    • Schreiben Sie den angezeigten Quelltext (vollständig! ohne zusätzliche Leerzeichen am Zeilenanfang!) in eine Datei mit Endung .hs, starten Sie ghci mit diesem Dateinamen als Argument

    • ändern Sie den Quelltext: ersetzen Sie undefined durch einen geeigneten Ausdruck, hier z.B.

      solution = S.fromList [ False, G ]

      im Editor speichern, in ghci neu laden (:r)

    • reparieren Sie Typfehler, werten Sie geeignete Terme aus, hier z.B. S.size solution

    • werten Sie test aus, wenn test den Wert True ergibt, dann tragen Sie die Lösung in autotool ein.

  2. Geben Sie einen Typ (eine data-Deklaration) mit genau 100 Elementen an. Sie können andere Data-Deklarationen benutzen (wie in autotool-Aufgabe). Minimieren Sie die Gesamtzahl aller deklarierten Konstruktoren.

  3. Vervollständigen Sie die Definition der Tiefe von Termen:

    \[\begin{aligned} && \operatorname{depth}( f() ) = 0 \\ k>0 &\Rightarrow& \operatorname{depth}(f(t_0,\ldots,t_{k-1})) = \dots\end{aligned}\]

    • Bestimmen Sie \(\operatorname{depth}(\sqrt{a\cdot a + b\cdot b})\)

    • Beweisen Sie \(\forall \Sigma: \forall t\in\operatorname{Term}(\Sigma): \operatorname{depth}(t) \le |t|-1\).

    • Für welche Terme gilt hier die Gleichheit?

  4. autotool-Aufgabe TRS-1

  5. (Zusatz-Aufgabe) für die Signatur \(\{A/2, D/0\}\):

    • definiere Terme \(t_0=D, t_{i+1} = A(t_i, D)\).

      Zeichne \(t_3\). Bestimme \(|t_i|,\operatorname{depth}(t_i)\) .

    • für \(S=\{ A(A(D,x),y)\to A(x,A(x,y)) \}\)

      bestimme \(S\)-Normalform(en), soweit existieren, der Terme \(t_2, t_3, t_4\).

      Geben Sie für \(t_2\) die ersten Ersetzungs-Schritte explizit an.

    • Normalform von \(t_i\) allgemein.

Programme

Funktionale Programme (Bsp.)

Signatur: \(\{(S,1),(Z,0),(f,2)\}\), Variablenmenge \(\{x',y\}\)

Ersetzungssystem \(\{ f(Z,y) \to y, f(S(x'),y) \to S(f(x',y)) \}\).

Konstruktor-System mit definiertem Symbol \(\{f\}\), Konstruktoren \(\{S,Z\}\), data N = Z | S N

Startterm \(f(S(S(Z)),S(Z))\).funktionales Programm:

f :: N -> N -> N  -- Typdeklaration
-- Gleichungssystem:
f Z y = y ; f (S x') y = S (f x' y)

Aufruf: f (S (S Z)) (S Z)

alternativ: eine Gleichung, mit Pattern Match

f x y = case x of
    { Z   -> y  ;  S x' -> S (f x' y) }

Pattern Matching

data Tree = Leaf | Branch Tree Tree
size :: Tree -> Int
size t = case t of { ... ; Branch l r -> ... }

Eigenschaften von Case-Ausdrücken

ein case-Ausdruck heißt

Bespiele (für data N = F N N | S N | Z)

-- nicht disjunkt:
case t of { F (S x) y -> .. ; F x (S y) -> .. }
-- nicht vollständig:
case t of { F x y -> .. ; Z -> .. }

data und case

typisches Vorgehen beim Verarbeiten algebraischer Daten vom Typ T:

Pattern Matching in versch. Sprachen

Nicht verwechseln mit regular expression matching zur String-Verarbeitung. Es geht um algebraische (d.h. baum-artige) Daten!

Peano-Zahlen

data N = Z | S N

plus :: N -> N -> N
plus x y = case x of
    Z -> y
    S x' -> S (plus x' y)

Aufgaben:

Spezifikation und Test

Bsp: Addition von Peano-Zahlen

Spezifikation und Verifikation

Beweis für: Addition von Peano-Zahlen ist assoziativ

Übung Pattern Matching, Programme

Hausaufgaben (für KW 19)

  1. Für die Deklarationen

    -- data Bool = False | True   (aus Prelude)
data S = A Bool | B | C S S

    entscheide/bestimme für jeden der folgenden Ausdrücke:

    • syntaktisch korrekt?

    • Resultat-Typ (statische Semantik)

    • Resultat-Wert (dynamische Semantik)

    • Menge der Muster ist: disjunkt? vollständig?

    1. case False of { True -> B }
2. case False of { B -> True }
3. case C B B of { A x -> x }
4. case A True of { A x -> False }

5. case A True of { A x -> False ; True -> False }
6. case True of { False -> A ; True -> A False }
7. case True of { False -> B ; False -> A False }
8. case B of { C x y -> False; A x -> x; B -> True }

  2. für selbst definierte Wahrheitswerte (vgl. Übungsaufgabe): deklarieren, implementieren und testen Sie eine zweistellige Funktion exclusiv-oder (mit Namen xor)

  3. für binäre Bäume ohne Schlüssel (vgl. Übungsaufgabe): deklarieren, implementieren und testen Sie ein einstelliges Prädikat über solchen Bäumen, das genau dann wahr ist, wenn das Argument eine gerade Anzahl von Blättern enthält.

  4. Peano-Zahlen: siehe autotool und:

    Beweisen Sie, daß unsere Implementierung der Addition kommutativ ist. Hinweis: dazu ist ein Hilfssatz nötig, in dessen Behauptung Z vorkommt.

bg

Polymorphie

Definition, Motivation

Beispiele f. Typkonstruktoren (I)

Beispiele f. Typkonstruktoren (II)

Polymorphe Funktionen

Beispiele:

Def: der Typ einer polymorphen Funktion beginnt mit All-Quantoren für Typvariablen.

Bsp: Datenkonstruktoren polymorpher Typen.

Bezeichnungen f. Polymorphie

data List e = Nil | Cons e (List e)

Operationen auf Listen (I)

data List a = Nil | Cons a (List a)

Von der Spezifikation zur Implementierung (II)

Bsp: homogene Listen data List a = Nil | Cons a (List a)

Aufgabe: implementiere maximum :: List N -> N

Spezifikation:

maximum (Cons x1 Nil) = x1
maximum (append xs ys) = max (maximum xs) (maximum ys)

Damit kann der aus dem Typ abgeleitete Quelltext

maximum :: List N -> N
maximum xs = case xs of
  Nil        -> 
  Cons x xs' ->

ergänzt werden.

Vorsicht: für min, minimum funktioniert das nicht so, denn min hat für N kein neutrales Element.

Operationen auf Listen (II)

Operationen auf Bäumen

data List e = Nil | Cons e (List e)
data Bin e = Leaf | Branch (Bin e) e (Bin e)

Knotenreihenfolgen

Adressierug von Knoten (False \(=\) links, True \(=\) rechts)

Statische Typisierung und Polymorphie

Bsp. für Programm ohne statischen Typ

Nutzen der stat. Typisierung und Polymorphie

Konstruktion von Objekten eines Typs

Aufgabe (Bsp): x :: Either (Maybe ()) (Pair Bool ())

Lösung (Bsp):

Insgesamt x = Right y = Right (Pair False ())

Vorgehen (allgemein)

Bestimmung des Typs eines Bezeichners

Aufgabe (Bsp.) bestimme Typ von x (erstes Arg. von get):

at :: Position -> Tree a -> Maybe a
at p t = case t of
  Node f ts -> case p of
    Nil -> Just f
    Cons x p' -> case get x ts of
      Nothing -> Nothing
      Just t' -> at p' t'

Lösung:

Vorgehen zur Typbestimmung eines Namens:

Übung Polymorphie

Geben Sie alle Elemente dieser Datentypen an:

Operationen auf Listen:

Operationen auf Bäumen:

Quelltexte aus Vorlesung: https://gitlab.imn.htwk-leipzig.de/waldmann/fop-ss18

Hausaufgaben (für KW 20)

  1. für die folgenden Datentypen: geben Sie einige Elemente an (ghci), geben Sie die Anzahl aller Elemente an (siehe auch autotool-Aufgabe)

    1. Maybe (Maybe Bool)

    2. Either (Bool, ()) (Maybe ())

    3. Foo (Maybe (Foo Bool)) mit data Foo a = C a | D

    4. (Zusatz) T () mit data T a = L a | B (T (a,a))

  2. Implementieren Sie die Post-Order Durchquerung von Binärbäumen.

    (Zusatz: Level-Order. Das ist schwieriger.)

  3. Beweisen Sie

    forall xs . reverse (reverse xs) == xs

    Sie dürfen

       reverse (append xs ys) 
== append (reverse ys) (reverse xs)

    ohne Beweis verwenden.

Funktionen

Funktionen als Daten

Der Lambda-Kalkül

Freie und gebundene Variablen(vorkommen)

Bsp: \(\operatorname{fvar}(x (\lambda x.\lambda y.x)) =\{x\}\), \(\operatorname{bvar}(x (\lambda x. \lambda y.x)) =\{x,y\}\),

Semantik des Lambda-Kalküls: Reduktion \(\to_\beta\)

Relation \(\to_\beta\) auf \(\Lambda\) (ein Reduktionsschritt)

Es gilt \(t \to_\beta t'\), falls

Ein (Teil-)Ausdruck der Form \((\lambda x.B)A\) heißt Redex.
(Dort kann weitergerechnet werden.)

Ein Term ohne Redex heißt Normalform.
(Normalformen sind Resultate von Rechnungen.)

Falsches Binden lokaler Variablen

Semantik …: gebundene Umbenennung \(\to_\alpha\)

Umbenennung von lokalen Variablen

Lambda-Terme: verkürzte Notation

Ein- und mehrstellige Funktionen

eine einstellige Funktion zweiter Ordnung:

f = \ x -> ( \ y -> ( x*x + y*y ) )

Anwendung dieser Funktion:

(f 3) 4 = ...

Kurzschreibweisen (Klammern weglassen):

f = \ x y -> x * x + y * y ; f 3 4

Übung:

gegeben t = \ f x -> f (f x)

bestimme t succ 0, t t succ 0, t t t succ 0, t t t t succ 0, ...

Typen

für nicht polymorphe Typen: tatsächlicher Argumenttyp muß mit deklariertem Argumenttyp übereinstimmen:

wenn \(f :: A \to B\) und \(x :: A\), dann \((f x) :: B\).

bei polymorphen Typen können der Typ von \(f :: A \to B\) und der Typ von \(x :: A'\) Typvariablen enthalten.

Beispiel: \(\lambda x.x :: \forall t.t\to t\).

Dann müssen \(A\) und \(A'\) nicht übereinstimmen, sondern nur unifizierbar sein (eine gemeinsame Instanz besitzen).

Beispiel: \((\lambda x.x)\text{True}\)

benutze Typ-Substitution \(\sigma=\{(t,\text{Bool})\}\).

Bestimme allgemeinsten Typ von \(t = \lambda f x . f(f x))\), von \((t t)\).

Beispiel für Typ-Bestimmung

Aufgabe: bestimme den allgemeinsten Typ von \(\lambda f x. f(f x)\)

Verkürzte Notation für Typen

Lambda-Ausdrücke in C#

Lambda-Ausdrücke in Java

Lambda-Ausdrücke in Javascript

$ node

> let f = function (x){return x+3;}
undefined

> f(4)
7

> ((x) => (y) => x+y) (3) (4)
7

> ((f) => (x) => f(f(x))) ((x) => x+1) (0)
2

Beispiele Fkt. höherer Ord.

Fkt. höherer Ord. für Folgen

Fkt. höherer Ord. für Mengen

Nützliche Funktionen höherer Ordnung

Stelligkeit von Funktionen

Übung Lambda-Kalkül

Hausaufgaben für KW 21

  1. (autotool) Reduktion im Lambda-Kalkül

  2. fvar implementieren (vgl. Übungsaufgabe)

  3. Normalform eines Lambda-Ausdrucks berechnen (an der Tafel, der Ausdruck wird erst dann gegeben)

  4. den allgemeinsten Typ eines Lambda-Ausdrucks bestimmen (an der Tafel, der Ausdruck wird erst dann gegeben)

  5. (autotool) Implementierung von dropWhile o.ä.

  6. Beweisen Sie für diese Implementierung

    xs=append (takeWhile p xs) (dropWhile p xs)

Rekursionsmuster

Rekursion über Bäume (Beispiele)

data Tree a = Leaf
            | Branch (Tree a) a (Tree a)
summe :: Tree Int -> Int
summe t = case t of
  Leaf -> 0 
  Branch l k r -> summe l + k + summe r
preorder :: Tree a -> List a
preorder t = case t of
  Leaf -> Nil 
  Branch l k r -> 
    Cons k (append (preorder l) (preorder r))

Rekursion über Bäume (Schema)

f :: Tree a -> b
f t = case t of
  Leaf -> ...
  Branch l k r -> ... (f l) k (f r)

dieses Schema ist eine Funktion höherer Ordnung:

fold :: ( ... ) -> ( ... ) -> ( Tree a -> b )
fold leaf branch = \ t -> case t of
  Leaf -> leaf
  Branch l k r -> 
     branch (fold leaf branch l) 
       k (fold leaf branch r)
summe = fold 0 ( \ l k r -> l + k + r )

Rekursion über Listen

and :: List Bool -> Bool
and xs = case xs of 
  Nil -> True ; Cons x xs' -> x && and xs'
length :: List a -> N
length xs = case xs of
  Nil -> Z ; Cons x xs' ->  S (length xs')

fold :: b -> ( a -> b -> b ) -> List a -> b
fold nil cons xs = case xs of
    Nil -> nil
    Cons x xs' -> cons x ( fold nil cons xs' )
and = fold True (&&) 
length = fold Z ( \ x y ->  S y)

Rekursionsmuster (Prinzip)

data List a = Nil | Cons a (List a) 
fold ( nil :: b ) ( cons :: a -> b -> b ) 
   :: List a -> b

Rekursionsmuster anwenden

\(=\) jeden Konstruktor durch eine passende Funktion ersetzen

\(=\) (Konstruktor-)Symbole interpretieren (durch Funktionen)

\(=\) eine Algebra angeben.

length  = fold Z  ( \ _ l -> S l ) 
reverse = fold Nil ( \ x ys ->      )

Rekursionsmuster (Merksätze)

aus dem Prinzip ein Rekursionsmuster anwenden \(=\) jeden Konstruktor durch eine passende Funktion ersetzen folgt:

Rekursion über Listen (Übung)

das vordefinierte Rekursionsschema über Listen ist:

foldr :: (a -> b -> b) -> b -> ([a] -> b)

length = foldr ( \ x y -> 1 + y ) 0

Beachte:

Aufgaben:

Weitere Beispiele für Folds

data Tree a 
  = Leaf a | Branch (Tree a) (Tree a)

fold :: ...

Rekursionsmuster (Peano-Zahlen)

data N = Z | S N

fold :: ...
fold z s n = case n of
    Z    -> 
    S n' -> 

plus  = fold ...
times = fold ...

Spezialfälle des Fold

Argumente für Rekursionsmuster finden

Vorgehen zur Lösung der Aufgabe:

Schreiben Sie Funktion \(f:T \to R\) als fold

Beispiel: data N = Z | S N,

\(f:\verb|N|\to\verb|Bool|\), \(f(x)=\) \(x\) ist ungerade

Nicht durch Rekursionmuster darstellbare Fkt.

Darstellung als fold mit Hilfswerten

Weitere Übungsaufgaben zu Fold

Übung Rekursionsmuster

Hausaufgaben für KW 22

  1. (autotool) Rekursionsmuster auf Listen (inits, tails, …)

  2. Rekursionsmuster auf Bäumen

    • Beweisen Sie, daß is_search_tree :: Tree Int -> Bool kein fold ist.

    • (autotool) diese Funktion kann jedoch als Projektion einer Hilfsfunktion h :: Tree Int -> (Bool, Maybe (Int,Int)) erhalten werden, die für nichtleere Bäume auch noch das kleinste und größte Element bestimmt. Stellen Sie h als fold dar.

  3. Rekursionsmuster auf Peano-Zahlen

    • führen Sie Addition, Multiplikation und Potenzierung (jeweils realisiert als fold) vor

    • Beweisen Sie, daß die modifizierte Vorgängerfunktion

      pre :: N -> N; pre Z = Z; pre (S x) = x

      kein fold ist.

    • (autotool) Diese Funktion pre kann jedoch als Projektion einer geeigneten Hilfsfunktion h :: N -> (N,N) realisiert werden. Spezifizieren Sie h und geben Sie eine Darstellung von h als fold an.

    • (autotool) Implementieren Sie die Subtraktion.

  4. Wenden Sie die Vorschrift zur Konstruktion des Rekursionsmusters an auf den Typ

    • Bool

    • Maybe a

    Jeweils:

    • Typ und Implementierung (vorbereiteten Quelltext zeigen)

    • Testfälle (in ghci vorführen)

    • gibt es diese Funktion bereits? Suchen Sie nach dem Typ mit https://www.haskell.org/hoogle/

Algebraische Datentypen in OOP

Kompositum: Motivation

Kompositum: Beispiel

public class Composite  {
  public static void main(String[] args) {
    JFrame f = new JFrame ("Composite");
    f.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE);
    Container c = new JPanel (new BorderLayout());
    c.add (new JButton ("foo"), BorderLayout.CENTER);
    f.getContentPane().add(c);
    f.pack(); f.setVisible(true);
  } 
}

Übung: geschachtelte Layouts bauen, vgl. http://www.imn.htwk-leipzig.de/~waldmann/edu/ws06/informatik/manage/

Kompositum: Definition

(Vorsicht: Begriff und Abkürzung nicht verwechseln mit abstrakter Datentyp \(=\) ein Typ, dessen Datenkonstruktoren wir nicht sehen)

Binäre Bäume als Komposita

der entsprechende algebraische Datentyp ist:

data Tree k = Leaf { ... }
  | Branch { left :: Tree k , ... 
           , right :: Tree k }

Übung: Anzahl aller Blätter, Summe aller Schlüssel (Typ?), der größte Schlüssel (Typ?)

Kompositum-Vermeidung

Wenn Blätter keine Schlüssel haben, geht es musterfrei?

class Tree<K> {
   Tree<K> left; K key; Tree<K> right;
}

Der entsprechende algebraische Datentyp ist

data Tree k =
     Tree { left :: Maybe (Tree k)
          , key :: k
          , right :: Maybe (Tree k)
          }

erzeugt in Java das Problem, daß …

Übung: betrachte Implementierung in java.util.Map<K,V>

Maybe \(=\) Nullable

Algebraischer Datentyp (Haskell):

data Maybe a = Nothing | Just a

http://hackage.haskell.org/packages/archive/base/latest/doc/html/Prelude.html#t:Maybe

In Sprachen mit Verweisen (auf Objekte vom Typ O) gibt es häufig auch Verweis auf kein Objekt— auch vom Typ O. Deswegen null pointer exceptions.

Ursache ist Verwechslung von Maybe a mit a.

Trennung in C#: Nullable<T> (für primitive Typen T)

http://msdn.microsoft.com/en-us/library/2cf62fcy.aspx

Alg. DT und Pattern Matching in Scala

http://scala-lang.org

algebraische Datentypen:

abstract class Tree[A]
case class Leaf[A](key: A) extends Tree[A]
case class Branch[A]
    (left: Tree[A], right: Tree[A]) 
        extends Tree[A]

pattern matching:

def size[A](t: Tree[A]): Int = t match {
    case Leaf(k) => 1
    case Branch(l, r) => size(l) + size(r)
  }

beachte: Typparameter in eckigen Klammern

Objektorientierte Rekursionsmuster

Plan

(Zum Vergleich von Java- und Haskell-Programmierung)

sagte bereits Albert Einstein: Das Holzhacken ist deswegen so beliebt, weil man den Erfolg sofort sieht.

Kompositum und Visitor

Definition eines Besucher-Objektes
(für Rekursionsmuster mit Resultattyp R über Tree<A>)
entspricht einem Tupel von Funktionen

interface Visitor<A,R> {
  R leaf(A k);
  R branch(R x, R y);  }

Empfangen eines Besuchers:
durch jeden Teilnehmer des Kompositums

interface Tree<A> { ..
  <R> R receive (Visitor<A,R> v);  }

Hausaufgaben für KW 23

  1. zur Folie Kompositum-Vermeidung:

    Das Problem bei null als Simulation für Leaf ist, daß man Blätter dann nicht richtig verarbeiten kann: Anstatt

    Tree<K> t = ... ; int s = t.size();

    muß man schreiben

    Tree<K> t = ... ; int s = (null == t) ? 0 : t.size();

    und das gilt für jede Methode.

    Wie wird das in der Implementierung von java.util.TreeMap<K,V> gelöst?

    Hinweis zu eclipse im Pool:

    • /usr/local/waldmann/opt/eclipse/latest (ohne /bin!) und /usr/local/waldmann/opt/java/latest/bin sollten im PATH sein

    • dann in Eclipse: Window \(\to\) Preferences \(\to\) Java \(\to\) Installed JREs \(\to\) Add eine neue JRE Version 12 (nicht 13!) hinzufügen

    • danach sind Bibliotheken mit der üblichen Navigation erreichbar (F4: Schnittstelle, F3: Quelltext)

  2. Implementieren und testen Sie die Funktion

    flip :: (a -> b -> c) -> (b -> a -> c)
flip f x y = _

    • (Zusatz) …in Javascript

      Bsp: Lambda-Ausdrücke in JS

      > (x => y => x-y) (5) (3)
2

      Hinweis zu node im Pool:

      export PATH=/usr/local/waldmann/opt/node/latest/bin:$PATH
export LD_LIBRARY_PATH=/usr/local/waldmann/opt/gcc/latest/lib64
node

    • …in Java (im Pool: ausführen mit jshell).

      Wie heißt der Typ für zweistellige Funktionen?

      Welches ist dann der Typ für flip?

    • Benutzen Sie Collections.sort, flip (vorige Teilaufgabe), Arrays.asList, Integer.compare, um eine Liste von Zahlen absteigend zu ordnen.

    Beispiel (vgl. Folie Strategie-Muster und folgende)

    jshell> List<Integer> xs = Arrays.asList(3,1,2,4)
xs ==> [3, 1, 2, 4]
jshell> Collections.sort(xs, Integer::compare)

jshell> xs
xs ==> [1, 2, 3, 4]

jshell> _ flip ( _ ) { _ }
jshell> <T>Comparator<T> asComp( _ f) { return (x,y)->f.apply(x,y);}
jshell> Collections.sort(xs,asComp(flip(Integer::compare))

  3. Java-Besucher für Listen. Schreibe das Kompositum für

    data List a = Nil | Cons a (List a)

    und den passenden Besucher. Benutze für

    • Summe, Produkt für List<Integer>

    • Und, Oder für List<Boolean>

    Ergänze Quelltexte (Eclipse-Projekt)

    Repository: https://gitlab.imn.htwk-leipzig.de/waldmann/fop-ss18, Pfad im Repository: eclipse/fop-ss18.

  4. Binärzahlen:

    • berechnen Sie den Wert einer Bitfolge als gespiegelte Binärzahl (LSB ist links), Bsp: [1,1,0,1] ==> 11

      • in Haskell (foldr)

      • in Java (Kompositum, Besucher wie vorige Teilaufgabe)

    • Beweisen Sie, daß die entsprechende Aufgabenstellung ohne Spiegelung (Bsp. [1,1,0,1] ==> 13) nicht lösbar ist

      (diese Funktion besitzt keine Darstellung als foldr)

Verzögerte Auswertung (lazy evaluation)

Motivation: Datenströme

Folge von Daten:

aus softwaretechnischen Gründen diese drei Aspekte im Programmtext trennen,

aus Effizienzgründen in der Ausführung verschränken (bedarfsgesteuerte Transformation/Erzeugung)

Bedarfs-Auswertung, Beispiele

Beispiel Bedarfsauswertung

data Stream a = Cons a (Stream a)
nats :: Stream Int ; nf :: Int -> Stream Int
nats = nf 0 ; nf n = Cons n (nf (n+1))
head (Cons x xs) = x ; tail (Cons x xs) = xs

Obwohl nats unendlich ist, kann Wert von head (tail (tail nats)) bestimmt werden:

   = head (tail (tail (nf 0)))
   = head (tail (tail (Cons 0 (nf 1))))
   = head (tail (nf 1))
   = head (tail (Cons 1 (nf 2)))
   = head (nf 2) = head (Cons 2 (nf 3)) = 2

es wird immer ein äußerer Redex reduziert

(Bsp: nf 3 ist ein innerer Redex)

Strictness

zu jedem Typ \(T\) betrachte \(T_\bot=\{\bot\}\cup T\)

dabei ist \(\bot\) ein Nicht-Resultat vom Typ \(T\)

Def.: Funktion \(f\) heißt strikt, wenn \(f(\bot)=\bot\).

Fkt. \(f\) mit \(n\) Arg. heißt strikt in \(i\),

falls \(\forall x_1 \dots x_n: (x_i=\bot) \Rightarrow f(x_1,\ldots,x_n)=\bot\)

verzögerte Auswertung eines Arguments
\(\Rightarrow\) Funktion ist dort nicht strikt

einfachste Beispiele in Haskell:

Beispiele Striktheit

Implementierung der verzögerten Auswertung

Begriffe:

bei jedem Konstruktor- und Funktionsaufruf:

Bedarfsauswertung in Scala

def F (x : Int) : Int = {
      println ("F", x) ; x*x
}        
lazy val a = F(3);
println (a);
println (a);

http://www.scala-lang.org/

Diskussion

Anwendg. Lazy Eval.: Ablaufsteuerung

Anwendg. Lazy Eval.: Modularität

Anwendg. Lazy Eval.: Streams

unendliche Datenstrukturen

Primzahlen

primes :: [ Int ]
primes = sieve ( enumFrom 2 )

enumFrom :: Int -> [ Int ]
enumFrom n = n : enumFrom ( n+1 )

sieve :: [ Int ] -> [ Int ]
sieve (x : xs) = x : sieve ys

wobei ys \(=\) die nicht durch x teilbaren Elemente von xs

(Das ist (sinngemäß) das Code-Beispiel auf https://www.haskell.org/)

Semantik von let-Bindungen

Beispiel für Lazy Semantik in Let

Übungsaufgaben zu Striktheit

Hausaufgaben für KW 25

  1. Aufgabe: strikt in welchen Argumenten?

    f x y z = case y || x of
  False -> y
  True -> case z && y  of
    False -> z
    True  -> False

    In der Übung dann ähnliche Aufgaben live.

  2. Bestimmen Sie jeweils die ersten Elemente dieser Folgen (1. auf Papier durch Umformen, 2. mit ghci).

    Für die Hilfsfunktionen (map, zipWith, concat):
    1. Typ feststellen, 2. Testfälle für endliche Listen

    1. f = 0 : 1 : f
    2. n = 0 : map (\ x -> 1 + x) n
    3. xs = 1 : map (\ x -> 2 * x) xs
    4. ys = False 
 : tail (concat (map (\y -> [y,not y]) ys))
    5. zs = 0 : 1 : zipWith (+) zs (tail zs)

    siehe auch https://www.imn.htwk-leipzig.de/~waldmann/etc/stream/

  3. (Zusatz) Algorithmus aus Appendix A aus Chris Okasaki: Breadth-First Numbering: Lessons from a Small Exercise in Algorithm Design (ICFP 2000) implementieren (von where auf let umschreiben), testen und erklären

OO-Simulation v. Bedarfsauswertung

Motivation (Wdhlg.)

Unix:

cat stream.tex | tr -c -d aeuio | wc -m

Haskell:

sum $ take 10 $ map ( \ x -> x^3 ) $ naturals

C#:

Enumerable.Range(0,10).Select(x=>x*x*x).Sum();

Iterator (Java)

interface Iterator<E> { 
  boolean hasNext(); // liefert Status
  E next(); // schaltet weiter
}
interface Iterable<E> { 
  Iterator<E> iterator(); 
}

typische Verwendung:

Iterator<E> it = c.iterator();
while (it.hasNext()) {
  E x = it.next (); ...
}

Abkürzung: for (E x : c) { ... }

Beispiel Iterator Java

Iterable<Integer> nats = new Iterable<Integer>() {
  public Iterator<Integer> iterator() {
    return new Iterator<Integer>() {
      private int state = 0;
      public Integer next() {
        int result = this.state; 
        this.state++; return result;
      }
      public boolean hasNext() { return true; }
    }; } };
for (int x : nats) { System.out.println(x); }

Aufgabe: implementiere eine Methode

static Iterable<Integer> range(int start, int count)

soll count Zahlen ab start liefern.

Testfälle dafür:

Weitere Beispiele Iterator

Enumerator (C#)

interface IEnumerator<E> {
  E Current; // Status
  bool MoveNext (); // Nebenwirkung
}
interface IEnumerable<E> { 
  IEnumerator<E> GetEnumerator();
}

Ü: typische Benutzung (schreibe die Schleife, vgl. mit Java-Programm)

Abkürzung: foreach (E x in c) { ... }

Zusammenfassung Iterator

Iteratoren mit yield

using System.Collections.Generic;
IEnumerable<int> Range (int lo, int hi) {
    for (int x = lo; x < hi ; x++)
       yield return x;
    yield break; }

Fkt. höherer Ord. für Streams

Motivation

Motivation: Parallel-Verarbeitung

geeignete Fkt. höherer Ordnung \(\Rightarrow\) triviale Parallelisierung:

var s = Enumerable.Range(1, 20000)
     .Select( f ).Sum() ;

var s = Enumerable.Range(1, 20000)
     .AsParallel()
     .Select( f ).Sum() ;

Dadurch werden

vgl. http://msdn.microsoft.com/en-us/library/dd460688.aspx

Strom-Operationen

Strom-Transformationen (1)

elementweise (unter Beibehaltung der Struktur)

Vorbild:

map :: (a -> b) -> [a] -> [b]

Realisierung in C#:

IEnumerable<B> Select<A,B> 
   (this IEnumerable <A> source,
    Func<A,B> selector);

Rechenregeln für map:

map f [] = ...
map f (x : xs) = ... 

map f (map g xs) = ...

Strom-Transformationen (2)

Änderung der Struktur, Beibehaltung der Elemente

Vorbild:

take :: Int -> [a] -> [a]
drop :: Int -> [a] -> [a]
filter :: (a -> Bool) -> [a] -> [a]

Realisierung: Take, Drop, Where

Übung: takeWhile, dropWhile, …

Strom-Transformationen (3)

neue Struktur, neue Elemente

Vorbild:

(>>=) :: [a] -> (a -> [b]) -> [b]

Realisierung:

SelectMany

Rechenregel (Beispiel):

map f xs = xs >>= ...

Übung:

Definition des Operators >=> durch

(s >=> t) = \ x -> (s x >>= t)

Typ von >=>? Assoziativität? neutrale Elemente?

Strom-Verbraucher

Vernichtung der Struktur

(d. h. kann danach zur Garbage Collection, wenn keine weiteren Verweise existieren)

Vorbild:

fold  :: r -> (e -> r -> r) -> [e] -> r

in der Version von links

foldl :: (r -> e -> r) -> r -> [e] -> r

Realisierung (Ü: ergänze die Typen)

R Aggregate<E,R> 
  (this IEnumerable<E> source, 
     ... seed, ... func)

(Beachte this. Das ist eine extension method)

Fold-Left: Eigenschaften

Fold-Left: Implementierung

Fold-Left: allgemeiner Typ

Zusammenfassung: Ströme

…und ihre Verarbeitung

C# (Linq) Haskell
IEnumerable<E> [e]
Select map
SelectMany >>= (bind)
Where filter
Aggregate foldl

Übung Stream-Operationen

Hinweise zur Arbeit mit C#:

Hausaufgaben für KW 26

  1. Übersetzen Sie dieses Programm (vollständiger Quelltext im git-repo)

    static IEnumerable<Tuple<int,int>> rectangle(int height,int width) {
  for (int x = 0; x<width; x++) {
    for (int y = 0; y<height; y++) {
      yield return new Tuple<int,int>(x,y);
    }
  }
  yield break;
}

    in einen expliziten Iterator (C# oder Java). Verallgemeinern Sie auf

    static IEnumerable<Tuple<A,B>> rectangle<A,B>(IEnumerable<A> xs,IEnumerable<B> ys)

  2. (Zusatz) implementieren Sie

    static IEnumerable<int> Merge(IEnumerable<int>xs, IEnumerable<int> ys)

    (Spezifikation: beide Eingaben sind (schwach) monoton steigend, Ausgabe auch und ist Multimengen-äquivalent zur Vereinigung der Eingaben).

    Verallgemeinern Sie von Element-Typ int auf einen Typparameter.

    Implementieren Sie Mergesort unter Verwendung dieses Merge

  3. Implementieren Sie map, filter und rectangle (siehe oben)

    • nur durch >>= (autotool)

    • Zusatz: durch SelectMany in C#

  4. In ghci vorführen und an der Tafel beweisen:

    für alle f,g,z,xs vom passenden Typ gilt:

    foldr f z (map g xs) == 
  foldr ( \ x y -> f (g x) y ) z xs

    Geben Sie eine ähnliche Beziehung für foldl und map an.

Eingeschränkte Polymorphie

Typklassen in Haskell: Überblick

Beispiel

sortBy :: (a -> a -> Ordering) -> [a] -> [a]
sortBy ( \ x y -> ... ) [False, True, False]

Kann mit Typklassen so formuliert werden:

class Ord a where 
    compare :: a -> a -> Ordering
sort :: Ord a => [a] -> [a]
instance Ord Bool where compare x y = ...
sort [False, True, False]

Grundwissen Typklassen

Unterschiede Typklasse/Interface (Bsp)

Unterschiede Typklasse/Interface (Impl.)

Typklassen/Interfaces: Vergleich

Generische Instanzen (I)

class Eq a where
    (==) :: a -> a -> Bool

Vergleichen von Listen (elementweise)

wenn a in Eq, dann [a] in Eq:

instance Eq a => Eq [a] where
  l == r = case l of
    [] -> case r of
      [] -> True ; y : ys -> False
    x : xs -> case r of
      [] -> False 
      y : ys -> (x == y) && ( xs == ys )

Übung: wie sieht instance Ord a => Ord [a] aus? (lexikografischer Vergleich)

Generische Instanzen (II)

class Show a where
  show ::  a -> String
instance Show Bool where
  show False = "False" ; show True = "True"
instance Show a => Show [a] where
  show xs = brackets 
          $ concat
          $ intersperse "," 
          $ map show xs
instance (Show a, Show b) => Show (a,b) where ...
show False = "False"
show ([True,False],True) 
  = "([True,False],True)"

Benutzung von Typklassen bei Leancheck

Test.LeanCheck—Beispiel

Testen für beliebige Stelligkeit

Überblick über Leancheck-Implementierung

Hausaufgaben für KW 27

bei beiden Aufgaben: vorbereitete Lösung in Editor/Eclipse zeigen, mit ghci/unit tests vorführen.

  1. für den Typ data T p = A Bool | B p deriving (Show, Eq) und mit import Test.LeanCheck:

    1. implementieren Sie

      instance Listable p => Listable (T p)

      unter Benutzung von cons* und \/

    2. die Eigenschaft die (abgeleitete) Gleichheit (==) auf T Int ist symmetrisch formulieren und testen

    3. zusätzlich Ord ableiten und testen, daß dann (<=) transitiv ist

    4. eine eigene instance Ord p => Ord (T p) schreiben, die verschieden ist von der abgeleiteten, aber trotzdem (<=) transitiv und antisymmetrisch (bzg. des abgeleiteten (==)). Eigenschaften durch Tests nachweisen.

  2. Übersetzen Sie nach Java

    data Pair a b = Pair { first :: a, second :: b }

    (in eine polymorphe Klasse, deren Komponenten final sind)

    1. Geben Sie Testfälle für Konstruktor-Aufruf und Zugriff auf Komponenten an, Bsp assertEquals(false,new Pair<Integer,Boolean>(42,false).second)

    2. implementiere equals als die mathematische Gleichheit von Paaaren, geben Sie Testfälle an

    3. implementieren Sie eine Methode äquivalent zu

      swap :: Pair a b -> Pair b a

      Testfälle: z.B.

      Pair<Integer,Boolean> p 
  = new Pair<>(42,false);
assertEquals (p,p.swap().swap());

    4. implementieren Sie für diese Klasse Comparable<Pair<A,B>> als die lexikografische Ordnung auf Paaren, mit Testfällen

Auswertung der Umfrage zur Vorlesung: https://www.imn.htwk-leipzig.de/~waldmann/edu/umf/

Bachelorarbeit zur Funktionalen Programmierung (Leistungsmessung einer Bibliothek mit Graphenalgorithmen): https://mail.haskell.org/pipermail/libraries/2019-June/029691.html

Bind (SelectMany, flatmap) und Verallgemeinerung

Linq (Language integrated query) in C#

IEnumerable<int> stream = from c in cars 
   where c.colour == Colour.Red
   select c.wheels;

wird vom Compiler übersetzt in

IEnumerable<int> stream = cars
   .Where (c => c.colour == Colour.Red)
   .Select (c => c.wheels);

Anwendung von SelectMany

Anwendung von Bind

do-Notation

Wdlhg: der Typkonstruktor Maybe

Die Konstruktorklasse Monad

Axiome für Monaden

Maybe als Monade

Maybe in C# (Nullable)

Nullable als Monade

wie heißen Return und Bind?

Anwendung (Testfall)

class C { 
  readonly int x; public C(int x){this.x=x;}  
  public C f(){return this.x>0 ? new C(x-1) : null;}
} 

new C(1) .f() .f() .f()
new C(1)?.f()?.f()?.f()

Übungen zu Monaden

  1. (wurde in der VL vorgeführt) Testen der Monaden-Axiome für Maybe in ghci:

    import Test.LeanCheck
import Test.LeanCheck.Function

f >=> g = \ x -> f x >>= g

check $ \ f x -> 
   ((f :: Bool -> Maybe Int) >=> return) x == f x

    beachten Sie

Hausaufgaben zu Monaden (für KW 28)

  1. zeigen Sie, daß >=> für Maybe nicht kommutativ ist. Betrachten Sie dabei nur Testfälle, in denen der statische Typ die Kommutation erlaubt.

    Mit Leancheck Gegenbeispiel ausrechnen, dann erklären.

  2. zur Listen-Monade:

    Erfüllt die folgende Instanz die Monaden-Axiome?

    return x = [x]
xs >>= f = take 2 (concat (map f xs))

    Hinweis: import Prelude hiding ((>>=)), dann (>>=) wie hier. return wird unverändert importiert.

    Definieren Sie den Operator f >=> g = \ xs -> f xs >>= g, testen Sie die Axiome mittels Leancheck.

  3. Nullable<T> in C# (oder Alternative aus Modul Control.Applicative in Haskell) Ist ?? (bzw. <|>) tatsächlich assoziativ? Vergleichen Sie die Bedeutung von (a ?? b) ?? c und a ?? (b ?? c) unter diesen Aspekten:

    • statische Semantik: Typisierung

    • dynamische Semantik: einschließlich \(\bot\) (Exceptions)

  4. Optional<T> in Java:

    • welche Methoden realisieren bind und return?

    • was entspricht dem Operator ?? aus C#?

    beides: Primär-Quellen (Dokumentation) angeben, Rechnungen in jshell vorführen.

  5. (Zusatz, evtl. autotool) definieren Sie eine Monad-Instanz jeweils für

    • binäre Bäume mit Schlüsseln nur in den Blättern

    • …nur in den Verzweigungsknoten

    • …in allen Knoten

    • beliebig verweigende Bäume rose trees data Tree a = Node a [Tree a]

    überprüfen Sie ein Einhaltung der Axiome.

Mehr zu Monaden

Wiederholung: Definition, Beispiele

Die Zustands-Monade

Parser als Monaden

data Parser t a = 
     Parser ( [t] -> [(a,[t])] )

Schnittstelle zu Betriebssystem

Transaktionaler Speicher (STM)

Arbeiten mit Collections im Ganzen

Wiederholung/Motivation

Beispiel Implementierung Mengenop.

Mengenoperationen

Laufzeitmessungen Mengen-Op.

Anwendung Mengen-Operationen (Bsp.)

Effiziente Repr. von Mengen von Zahlen

Übung (sequentielle) Mengen-Operationen

Hausaufgaben

  1. Data.Set benutzt balancierte Bäume.

    1. Erzeugen Sie einen Baum, der kein AVL-Baum ist. Hinweis:

      import qualified Data.Set as S
putStrLn $ S.showTree $ S.fromList [ 1 .. 5 ]

    2. Erzeugen Sie zwei unterschiedliche Bäume, die die gleiche Menge repräsentieren.

    3. Zeigen Sie die Stelle im offiziellen Quelltext, die die Balance testet bzw. herstellt.

  2. Führen Sie das Beispiel Anzahl der Vorkommen der Elemente einer Folge möglichst ähnlich in C#/LINQ vor.

    Hinweise: GroupBy,

    API erforschen und benutzen. Keine explizite Iteration/Rekursion. foldl ist gestattet, das heißt Aggregate.

    Hinweis: benutzen Sie Original-Dokumentation (z.B. https://msdn.microsoft.com/en-us/library/bb549218(v=vs.110).aspx und keine zweifelhafte Sekundärliteratur (Hausaufgabenwebseiten).

  3. Wir betrachten diese Realisierung von Relationen auf einer Menge \(s\):

    type Rel s = M.Map s (S.Set s, S.Set s)

    Dabei soll für den Wert \((V,N)\) zum Schlüssel \(x\) gelten:

    \(V\) ist die Menge aller direkten Vorgänger von \(x\),

    \(N\) ist die Menge aller direkten Nachfolger von \(x\).

    Für die folgenden Operationen: jeweils

    • (allgemeinsten) Typ angeben,

    • Implementierung angeben,

    • Testfälle angeben und vorführen:

    1. die leere Relation, die Einer-Relation \(\{(x,y)\}\)

    2. das Einfügen eines Paares \((x,y)\) in eine Relation

    3. die Funktion fromList, die Funktion toList

    4. der Durchschnitt von zwei Relationen

    5. das Produkt von zwei Relationen

    die letzte Teilaufgabe (Produkt) ist entscheidend, alles andere ist nur Vorbereitung.

  4. Eine frühere Variante der vorigen Aufgabenstellung war: …Relationen \(R\subseteq s\times t\)

    type Rel s t = M.Map s (S.Set t, S.Set t)

    das geht aber nicht, denn damit kann man schon

    singleton :: (Ord s, Ord t) => s -> t -> Rel s t

    nicht realisieren. Es geht mit

    data Rel s t = Rel
  { fore :: M.Map s (S.Set t)
  , back :: M.Map t (S.Set s)
  }

Zusammenfassung, Ausblick

Themen

Aussagen

Programmierer(in) sollte

Eigenschaften und Grenzen von Typsystemen

Software-Verifikation (Beispiele)

CYP — check your proofs

Theorems for Free: Beispiel

Theorems for Free: Quelle

Struktur-erhaltende Transformationen

Theorems for Free: Systematik, Beispiele

Anwendungen der funktionalen Progr.

Beispiel: Yesod https://www.yesodweb.com/ Michael Snoyman (O’Reilly 2012)

Anwendung: https://gitlab.imn.htwk-leipzig.de/autotool/all0/tree/master/yesod

Marcellus Siegburg: REST-orientierte Refaktorisierung des E-Learning-Systems Autotool (Masterarbeit 2015)

Funktionale Programmierung in der Industrie

Anwendungen v. Konzepten der fktl. Prog.

Ein weiterer Vorzug der Fktl. Prog.