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 KW14

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_1,\ldots,t_k)| = 1 + \sum_{i=1}^k |t_i|\).

Vervollständigen Sie die Definition der Tiefe von Termen:

\[\begin{aligned} && \operatorname{depth}( f() ) = 0 \\ k>0 &\Rightarrow& \operatorname{depth}(f(t_1,\ldots,t_k)) = \dots\end{aligned}\]

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\).

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

Programme

Funktionale Programme

1pt …sind spezielle Term-Ersetzungssysteme. Beispiel:

Signatur: \(S\) einstellig, \(Z\) nullstellig, \(f\) zweistellig.

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

Startterm \(f(S(S(Z)),S(Z))\).

entsprechendes funktionales Programm:

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

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

Auswertung \(=\) Folge von Ersetzungsschritten \(\to_R^*\)
Resultat \(=\) Normalform (hat keine \(\to_R\)-Nachfolger)

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:

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:

Pattern Matching in versch. Sprachen

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

Übung Pattern Matching, Programme

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)

Operationen auf Listen (II)

Die vorige Implementierung von reverse ist (für einfach verkettete Listen) nicht effizient.

Besser ist:

reverse xs = rev_app xs Nil

mit Spezifikation

rev_app xs ys = append (reverse xs) ys

Übung: daraus die Implementierung von rev_app ableiten

rev_app xs ys = case xs of ...

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)

Übung Polymorphie

Geben Sie alle Elemente dieser Datentypen an:

Operationen auf Listen:

Operationen auf Bäumen:

Kochrezept: Objektkonstruktion

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

Lösung (Bsp):

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

Vorgehen (allgemein)

Kochrezept: Typ-Bestimmung

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:

Statische Typisierung und Polymorphie

Def: dynamische Typisierung:

Def: statische Typisierung:

Bsp. für Programm ohne statischen Typ (Javascript)

function f (x) { 
  if (x>0) { return function () { return 42; } } 
  else { return "foobar"; } }

Dann: Auswertung von f(1)() ergibt 42, Auswertung von f(0)() ergibt Laufzeit-Typfehler.

entsprechendes Haskell-Programm ist statisch fehlerhaft

f x = case x > 0 of
  True  -> \ () -> 42
  False -> "foobar"

Nutzen der statischen Typisierung:

Nutzen der Polymorphie:

Von der Spezifikation zur Implementierung (I)

Bsp: Addition von Peano-Zahlen data N = Z | S N

plus :: N -> N -> N

aus der Typdeklaration wird abgeleitet:

plus x y = case x of
  Z    ->
  S x' ->

erster Zweig: plus Z y = 0 + y = y

zweiter Zweig : plus (S x') y = (1 + x') + y =

mit Assoziativität von + gilt ... = 1 + (x' + y) = S (plus x' y)

Bsp. (Ü): Multiplikation. Hinweis: benutze Distributivgesetz.

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.

Funktionen

Funktionen als Daten

Der Lambda-Kalkül

…als weiteres Berechnungsmodell,

(vgl. Termersetzungssysteme, Turingmaschine, Random-Access-Maschine)

Syntax: die Menge der Lambda-Terme \(\Lambda\) ist

Semantik: eine Relation \(\to_\beta\) auf \(\Lambda\)

(vgl. \(\to_R\) für Termersetzungssystem \(R\))

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.)

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

Umbenennung von lokalen Variablen

int x = 3;
int f(int y) { return x + y; }
int g(int x) { return (x + f(8)); }  
// g(5) => 16

Darf f(8) ersetzt werden durch \(f[y:=8]\) ? - Nein:

int x = 3;
int g(int x) { return (x + (x+8)); }  
// g(5) => 18

Das freie \(x\) in \((x+y)\) wird fälschlich gebunden.

Lösung: lokal umbenennen

int g(int z) { return (z + f(8)); }

dann ist Ersetzung erlaubt

int x = 3;
int g(int z) { return (z + (x+8)); }  
// g(5) => 16

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(8)

funktionales Interface (FI): hat genau eine Methode

Lambda-Ausdruck (burger arrow) erzeugt Objekt einer anonymen Klasse, die FI implementiert.

interface I { int foo (int x); }
I f = (x)-> x+1;         
System.out.println (f.foo(8));

vordefinierte FIs:

import java.util.function.*;

Function<Integer,Integer> g = (x)-> x*2;
   System.out.println (g.apply(8));
Predicate<Integer> p = (x)-> x > 3;
   if (p.test(4)) { System.out.println ("foo"); }

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.

Übung Lambda-Kalkül

Übung Fkt. höherer Ordnung

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 ...

Übung Rekursionsmuster

Stelligkeit von Funktionen

Nützliche Funktionen höherer Ordnung

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

Spezialfälle des Fold

Weitere Übungsaufgaben zu Fold

Objektorientierte Entwurfmuster

Definition, Geschichte

Beispiel Strategie-Muster

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);  }

Aufgabe: Besucher für Listen

Schreibe das Kompositum für

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

und den passenden Besucher. Benutze für

Quelltexte aus Vorlesung (Eclipse-Projekt)

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

Polymorphie

Arten der Polymorphie

moderne OO-Sprachen (u.a. Java, C#) bieten beide Formen der Polymorphie

mit statischer Sicherheit (d.h. statische Garantie, daß zur Laufzeit keine Methoden fehlen)

Java-Notation f. generische Polymorphie

generischer Typ (Typkonstruktor):

statische generische Methode:

(Übung: Angabe der Typargumente für polymorphe nicht statische Methode)

Beispiel f. dynamische Polymorphie

interface I { int m (); }
class A implements I 
    { int m () { return 0; }}
class B implements I 
    { int m () { return 1; }}
I x =    // statischer Typ von x ist I
    new A(); // dynamischer Typ ist hier A
System.out.println (x.m());
x = new B(); // dynamischer Typ ist jetzt B
System.out.println (x.m());

Klassen, Schnittstellen und Entwurfsmuster

Erzwingen von Abstraktionen

Das Fabrik-Muster

interface I { }
class A implements I { A (int x) { .. } }
class B implements I { B (int x) { .. } }

die Gemeinsamkeit der Konstruktoren kann nicht in I ausgedrückt werden.

interface F // abstrakte Fabrik 
   { I construct (int x); }
class FA implements F // konkrete Fabrik
{ I construct (int x) { return new A(x); } }
class FB implements F { .. }
main () { 
   F f = Eingabe ? new FA() : new FB();
   I o1=f.construct(3); I o2=f.construct(4);

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]

Unterschiede Typklasse/Interface (Bsp)

Typklassen können mehr als Interfaces

in Java, C#, …kann Schnittstelle (interface) in Deklarationen wie Typ (class) benutzt werden, das ist

1. praktisch, aber nur 2. soweit es eben geht

Grundwissen Typklassen

Übung Polymorphie

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

Anwendungen der verzögerten Auswertg. (I)

Abstraktionen über den Programm-Ablauf

Anwendungen der verzögerten Auswertg. (II)

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 : ys

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

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

Aufgaben zu Striktheit

Übung: Rekursive Stream-Definitionen

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/

OO-Simulation v. Bedarfsauswertung

Motivation (Wdhlg.)

0pt 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) { ... }

Beispiele Iterator

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 res;
      }
      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:

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; }

Aufgaben Iterator C#

IEnumerable<int> Nats () {
    for (int s = 0; true; s++) {
        yield return s;
    }
}

Implementiere das merge aus mergesort (Spezifikation?)

static IEnumerable<E> Merge<E> 
    (IEnumerable<E> xs, IEnumerable<E> ys) 
  where E : IComparable<E>

zunächst für unendliche Ströme, Test: Merge(Nats().Select(x=>x*x),Nats().Select(x=>3*x+1)).Take(10)

(benötigt using System.Linq und Assembly System.Core)

Dann auch für endliche Ströme, Test: Merge(new int [] {1,3,4}, new int [] {2,7,8})

Dann Mergesort

   static IEnumerable<E> Sort<E> (IEnumerable<E> xs) 
        where E : IComparable<E> {
        if (xs.Count() <= 1) {
            return xs;
        } else { // zwei Zeilen folgen
            ...
        }
    }

Test: Sort(new int [] { 3,1,4,1,5,9})

Streams in C#: funktional, Linq

Funktional

IEnumerable.Range(0,10).Select(x => x^3).Sum();

Typ von Select? Implementierung?

Linq-Schreibweise:

(from x in new Range(0,10) select x*x*x).Sum();

Beachte: SQL-select vom Kopf auf die Füße gestellt.

Fkt. höherer Ord. für Streams

Motivation

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)

Zusammenfassung: Ströme

…und ihre Verarbeitung

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

Bsp: die Spezifikation von TakeWhile

https://msdn.microsoft.com/en-us/library/bb534804(v=vs.110).aspx

zeigt Nachteile natürlichsprachlicher Spezifikationen:

Es wäre schon gegangen, man hätte nur wollen müssen:

“w.TakeWhile(p) ist der maximale Präfix von w, dessen Elemente sämtlich die Bedingung \(p\) erfüllen.”

(Notation \(u\sqsubseteq w\) für \(u\) ist Präfix von \(w\), Def.: \(\exists v: u\cdot v = w\))

korrekte Spezifikation: w.TakeWhile(p) = u iff

Arbeiten mit Collections in Haskell

Bsp: Data.Set und Data.Map aus https://hackage.haskell.org/package/containers

Beispiel-Funktionen mit typischen Eigenschaften:

unionWith 
  :: Ord k => (v->v->v)->Map k v->Map k v->Map k v
fromListWith 
  :: Ord k => (v->v->v) -> [(k, v)] -> Map k v

Anwendungen:

Linq-Syntax (type-safe SQL)

var stream = from c in cars 
   where c.colour == Colour.Red
   select c.wheels;

wird vom Compiler übersetzt in

var stream = cars
   .Where (c => c.colour == Colour.Red)
   .Select (c.wheels);

Beachte:

Übung: Ausdrücke mit mehreren from, mit group .. by ..

Linq-Syntax (type-safe SQL) (II)

var stream = 
  from x in Enumerable.Range(0,10) 
  from y in Enumerable.Range(0,x) select y

wird vom Compiler übersetzt in

var stream = Enumerable.Range(0,10)
      .SelectMany(x=>Enumerable.Range(0,x))

Linq und Parallelität

…das ist ganz einfach: anstatt

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

schreibe

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

Dadurch werden

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

Übung Stream-Operationen

Bsp: nicht durch fold darstellbare Funktion

filter, takeWhile, dropWhile :: (a -> Bool) -> [a] -> [a]

die ersten beiden lassen sich durch fold darstellen, aber dropWhile nicht. Beweis (indirekt):

Falls doch dropWhile p xs = fold n c xs, dann entsteht folgender Widerspruch:

   [False,True] 
== dropWhile id [False,True]
== fold n c [False,True]
== c False (fold n c [True])
== c False (dropWhile id [True])
== c False []
== c False (dropWhile id [])
== c False (fold n c [])
== fold n c [False]
== dropWhile id [False]
== [ False ]

Ü: läßt sich dropWhile als foldl schreiben?

Fold-Left: Eigenschaften

Fold-Left: Implementierung

Fold-Left: allgemeiner Typ

Organisatorisches

KW 26 und KW 27

Funktional-Reactive Programmierung

Motivation

Verhaltensmuster: Beobachter

Beobachter: Beispiel

public class Counter extends Observable {
    private int count = 0;
    public void step () { this.count ++;
        this.setChanged(); 
        this.notifyObservers();   }   }
public class Watcher implements Observer {
    private final int threshold;
    public void update(Observable o, Object arg) {
       if (((Counter)o).getCount() >= this.threshold) {
           System.out.println ("alarm");  }   }  }
public static void main(String[] args) {
    Counter c = new Counter ();
    Watcher w = new Watcher (3);
    c.addObserver(w); c.step(); c.step (); c.step (); }

Funktional-Reaktive Programmierung

FRP-Beispiel

dollar <- UI.input ; euro   <- UI.input
getBody window #+ [
  column [ grid [[string "Dollar:", element dollar]
                 ,[string "Euro:"  , element euro  ]]
        ]]
euroIn   <- stepper "0" $ UI.valueChange euro
dollarIn <- stepper "0" $ UI.valueChange dollar
let rate = 0.7 :: Double
    withString f = maybe "-" (printf "%.2f") . fmap f . readMay
    dollarOut = withString (/ rate) <$> euroIn
    euroOut   = withString (* rate) <$> dollarIn
element euro   # sink value euroOut
element dollar # sink value dollarOut

https://github.com/HeinrichApfelmus/threepenny-gui/tree/master/samples

Anwendungen von Typklassen

Testdaten für property based testing

Typklassen für small/lean-check

(Data) dependent types

Simulation v. dependent types d. Typklassen

Zusammenfassung, Ausblick

Themen

Aussagen

Programmierer(in) sollte

Eigenschaften und Grenzen von Typsystemen

Software-Verifikation (Beispiele)

CYP — check your proofs

Anwendungen der funktionalen Progr.

Beispiel: Framework Yesod http://www.yesodweb.com/

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

Industrielle Anwendg. d funkt. Progr.

siehe Workshops Commercial users of functional programming http://cufp.org/2015/

Diskussion:

Anwendungen v. Konzepten der fktl. Prog.

Ein weiterer Vorzug der Fktl. Prog.