Beispiel: C-Compiler

• int gcd (int x, int y) {
    while (y>0) { int z = x%y; x = y; y = z; }
    return x; }

• gcc -S -O2 gcd.c erzeugt gcd.s:

  .L3:    movl    %edx, %r8d ; cltd  ; idivl   %r8d
          movl    %r8d, %eax  ;   testl   %edx, %edx
          jg      .L3

  Ü: was bedeutet cltd, warum ist es notwendig?

  Ü: welche Variable ist in welchem Register?

• identischer (!) Assembler-Code für

  int gcd_func (int x, int y) {
    return y > 0 ? gcd_func (y,x % y) : x;
  }

• vollständige Quelltexte: siehe Repo

• Bsp Java-Kompilation: https://www.imn.htwk-leipzig.de/~waldmann/etc/safe-speed/

Inhalt der Vorlesung

Konzepte von Programmiersprachen

• Semantik von einfachen (arithmetischen) Ausdrücken

• lokale Namen, $\bullet$ Unterprogramme (Lambda-Kalkül)

• Zustandsänderungen (imperative Prog.)

• Continuations zur Ablaufsteuerung

realisieren durch

• Interpretation, $\bullet$ Kompilation

Hilfsmittel:

• Theorie: Inferenzsysteme (f. Auswertung, Typisierung)

• Praxis: Haskell, Monaden (f. Auswertung, Parser)

Einleitung: Sprachverarbeitung

• mit Interpreter:

  • Quellprogramm, Eingaben $\stackrel{\text{Interpreter}}{⟶}$ Ausgaben

• mit Compiler:

  • Quellprogramm $\stackrel{\text{Compiler}}{⟶}$ Zielprogramm

  • Eingaben $\stackrel{\text{Zielprogramm}}{⟶}$ Ausgaben

• Mischform:

  • Quellprogramm $\stackrel{\text{Compiler}}{⟶}$ Zwischenprogramm

  • Zwischenprogramm, Eingaben $\stackrel{\text{virtuelleMaschine}}{⟶}$ Ausgaben

• reale Maschine (CPU) ist Interpreter für Maschinen- sprache (Interpretation in Hardware, in Microcode)

• gemeinsam ist: syntaxgesteuerte Semantik (Ausführung oder Übersetzung)

Literatur

Anwendungen von Techniken des Compilerbaus

• Implementierung höherer Programmiersprachen

• architekturspezifische Optimierungen (Parallelisierung, Speicherhierarchien)

• Entwurf neuer Architekturen (RISC, spezielle Hardware)

• Programm-Übersetzungen (Binär-Übersetzer, Hardwaresynthese, Datenbankanfragesprachen)

• Software-Werkzeuge (z.B. Refaktorisierer)

• domainspezifische Sprachen

Organisation der Vorlesung

• pro Woche eine Vorlesung, eine Übung.

• in Vorlesung, Übung und Hausaufgaben:

  • Theorie,

  • Praxis: Quelltexte (weiter-)schreiben

• Prüfungszulassung: regelmäßiges und erfolgreiches Bearbeiten von Übungsaufgaben

• Prüfung: Klausur (120 min, keine Hilfsmittel)

  Bei Interesse und nach voriger Absprache: Ersatz eines Teiles der Klausur durch vorherige Hausarbeit

  z.B. Reparaturen an autotool-Aufgaben oder anderem open-source-Projekt (Ihrer Wahl), bei denen Techniken des Compilerbaus angewendet werden

Beispiel: Interpreter f. arith. Ausdrücke

data Exp = Const Integer 
         | Plus Exp Exp | Times Exp Exp
    deriving ( Show )

ex1 :: Exp
ex1 = 
  Times ( Plus ( Const 1 ) ( Const 2 ) ) ( Const 3 )

value :: Exp -> Integer
value x = case x of
    Const i -> i
    Plus x y -> value x + value y
    Times x y -> value x * value y

das ist syntax-gesteuerte Semantik:

Wert des Terms wird aus Werten der Teilterme kombiniert

Beispiel: lokale Variablen und Umgebungen

data Exp = ... | Let String Exp Exp | Ref String
ex2 :: Exp
ex2 = Let "x" ( Const 3 ) 
     ( Times ( Ref "x" ) (Ref "x" ) )
type Env = ( String -> Integer )
extend n w e = \ m -> if m == n then w else e m
value :: Env -> Exp -> Integer
value env x = case x of
    Ref n -> env n
    Let n x b -> value (extend n (value env x) env) b
    Const i -> i
    Plus x y -> value env x + value env y
    Times x y -> value env x * value env y
test2 = value (\ _ -> 42) ex2

Bezeichner sind Strings — oder nicht?

• ... | Let String Exp Exp — wirklich?

• es gilt type String = [Char], also

  • einfach verkettete Liste von Zeichen

  • mit Bedarfsauswertung (lazy Konstruktoren)

• das ist

  • ineffizient (in Platz und Zeit)

  • egal (für unseren einfachen Anwendungsfall)

  • gefährlich (wenn man es für andere Anwendungen übernimmt)

• deswegen jetzt schon Diskussion …

  • von alternativen Implementierungen

  • und wie man diese versteckt

Datentypen für Folgen (von Zeichen)

• type String = [Char]: einfach verkettet, lazy: ist in den allermeisten Fällen unzweckmäßig

• data Vector a: Array (d.h., zusammenhängender Speicherbereich, deswegen effiziente Indizierung) mit kostenlosem slicing (Abschnitt-Bildung)

• data Bytestring: $\approx$ Vektor von Bytes (d.h., für rein binären Datenaustausch)

• data Text (aus Modul Data.Text) efficient packed, immutable Unicode text type, (d.h., Zeichen $=$ Bytefolge)

• Modul Data.Text.Lazy: lazy Liste von (strikten) Text-Abschnitten, für Stream-Verarbeitung

Verstecken von Implementierungsdetails

• Implementierung direkt sichtbar:

  data Exp = ... | Let Text Exp Exp

• Verschieben der Implementierungs-Entscheidung:

  type Id = Text; data Exp = ... | Let Id Exp Exp

  bleibt aber sichtbar (type-Deklarationen werden bei Kompilation immer expandiert)

• Verstecken der Entscheidung: modul Id (Id) where data Id = Id Text exportiert wird Typ-Name, aber nicht der Konstruktor

  der Anwender (Importeur) von Id sieht Text nicht

• data-Deklaration mit genaue einem Konstruktor: erstetzen durch newtype Id = Id Text

  dieser kostet gar nichts (keine Zeit, keinen Platz)

Verwendung standardisierter Namen

• alle benötigten Funktionen (einschl. Konstruktoren) für Id implementieren und exportieren (es sind nicht viele)

  eqId::Id->Id->Bool; eqId (Id s) (Id t) = s == t

• diese spezifischen Namen will sich keiner merken $\Rightarrow$ verwende standardisierte Typklassen, Bsp.

  instance Eq Id where (Id s) == (Id t) = s == t

  der Importeur von Id sieht den Namen (==) bereits, weil er in Prelude definiert ist

• wenn die Implementierung einer standardisierten Klasse eine einfache Delegation ist, kann sie vom Compiler erzeugt werden

  newtype Id = Id Text deriving Eq

Einsparung von Konstruktor-Aufrufen

•     -- Implementierung des Konstruktors
  import qualified Data.Text as T
  fromString::String->Id;fromString s = Id (T.pack s)        
      -- Anwendung:
  foo :: Id ; foo = fromString "bar"

• der Schreibaufwand wird verringert durch

           -- bei Implementierung:
  import Data.String;
  instance IsString Id where fromString = T.pack
           -- bei Anwendung:
  {-# language OverloadedStrings #-}
  foo :: Id ; foo = "bar"

  String-Literale sind dann überladen $\Rightarrow$ Compiler setzt fromString vor jedes ("bar"$\Rightarrow$fromString "bar")

Übung (Haskell)

• Wiederholung Haskell

  • Interpreter/Compiler: ghci http://haskell.org/

  • Funktionsaufruf nicht f(a,b,c+d), sondern f a b (c+d)

  • Konstruktor beginnt mit Großbuchstabe und ist auch eine Funktion

• Wiederholung funktionale Programmierung/Entwurfsmuster

  • rekursiver algebraischer Datentyp (ein Typ, mehrere Konstruktoren)

    (OO: Kompositum, ein Interface, mehrere Klassen)

  • rekursive Funktion

• Wiederholung Pattern Matching:

  • beginnt mit case ... of, dann Zweige

  • jeder Zweig besteht aus Muster und Folge-Ausdruck

  • falls das Muster paßt, werden die Mustervariablen gebunden und der Folge-Ausdruck auswertet

Übung (Interpreter)

• Benutzung:

  • Beispiel für die Verdeckung von Namen bei geschachtelten Let

  • Beispiel dafür, daß der definierte Name während seiner Definition nicht sichtbar ist

• Erweiterung:

  Verzweigungen mit C-ähnlicher Semantik:

  Bedingung ist arithmetischer Ausdruck, verwende 0 als Falsch und alles andere als Wahr.

  data Exp = ...
           | If Exp Exp Exp

Übung (effiziente Imp. von Bezeichnern)

• welche Operationen auf Id werden benötigt?

  • Konstruktion (fromString)

  • Gleichheit

  • Ausgabe (nur für Fehlermeldungen!)

• für newtype Id = Id Text deriving Eq:

  wie teuer ist Vergleich? wie könnte man das verbessern?

• für type Env und extend wie angegeben: wie teuer ist das Aufsuchen des Wertes eines Namens in einer Umgebung, die durch $n$ geschachtelte extend entsteht?

  wie könnte man das verbessern?

  Hinweis: mit Env als Funktion: gar nicht.

  Welcher andere Typ könnte verwendet werden?

Motivation

• inferieren $=$ ableiten

• Inferenzsystem $I$, Objekt $O$,

  Eigenschaft $I⊢O$ (in $I$ gibt es eine Ableitung für $O$)

• damit ist $I$ eine Spezifikation einer Menge von Objekten

• man ignoriert die Implementierung ($=$ das Finden von Ableitungen)

• Anwendungen im Compilerbau:

  Auswertung von Programmen, Typisierung von Programmen

Definition

ein Inferenz-System $I$ besteht aus

• Regeln (besteht aus Prämissen, Konklusion)

  Schreibweise $\frac{P_1,\dots ,P_n}{K}$

• Axiomen ($=$ Regeln ohne Prämissen)

eine Ableitung für $F$ bzgl. $I$ ist ein Baum:

• jeder Knoten ist mit einem Objekt beschriftet

• jeder Knoten (mit Vorgängern) entspricht Regel von $I$

• Wurzel (Ziel) ist mit $F$ beschriftet

Def: $I⊢F$ $:⟺$ $\mathrm{\exists }$ $I$-Ableitungsbaum mit Wurzel $F$.

Regel-Schemata

• um unendliche Menge zu beschreiben, benötigt man unendliche Regelmengen

• diese möchte man endlich notieren

• ein Regel-Schema beschreibt eine (mglw. unendliche) Menge von Regeln, Bsp: ${\displaystyle \frac{(x,y)}{(x-y,y)}}$

• Schema wird instantiiert durch Belegung der Schema-Variablen

  Bsp: Belegung $x\mapsto 13,y\mapsto 5$

  ergibt Regel ${\displaystyle \frac{(13,5)}{(8,5)}}$

Inferenz-Systeme (Beispiel)

• Grundbereich $=$ Zahlenpaare $\mathbb{Z}\times \mathbb{Z}$

• Axiom: ${\displaystyle \frac{}{(13,5)}}$

• Regel-Schemata: ${\displaystyle \frac{(x,y)}{(x-y,y)}}$, ${\displaystyle \frac{(x,y)}{(x,y-x)}}$

• gilt $I⊢(1,1)$ ?

• Ü: Beziehung zu einem alten Algorithmus (früh im Studium, früh in der Geschichte der Menschheit)

Primalitäts-Zertifikate

• Satz: $p\in \mathbb{P}⟺$ $\mathrm{\exists }g:$ $g$ ist primitive Wurzel mod $p$:

  $[g^0,g^1,g^2,\dots ,g^{p-2}]$ ist Permutation von $[1,2,\dots ,p-1]$

  let {p = 7; g = 3}
  in map (`mod` p) $ take (p-1) $ iterate (*g) 1
  [1,3,2,6,4,5]

• Inferenzregel ${\displaystyle \frac{g_1:p_1,\dots ,g_k:p_k}{g:p}}$,

  falls $p-1=q_1^{e_1}\cdots q_k^{e_k}$ und $\mathrm{\forall }i:g^{(p-1)/q_i}\ne 1\mathrm{mod}p$

• Vaughan Pratt, Each Prime has a Succinct Certificate, SIAM J. Comp. 1975

• es folgt $\mathbb{P}\in \mathsf{\text{NP}}\cap \mathsf{\text{co-NP}}$, aber $\mathbb{P}$ not known to be in $\mathsf{\text{P}}$

• Agrawal, Kayal, Saxena: Primes is in P, 2004

Inferenz von Typen

• später implementieren wir das, als statische Analyse im Interpreter/Compiler,

  jetzt geben wir nur die Regel an: ${\displaystyle \frac{f:T_1\to T_2,x:T_1}{fx:T_2}}$

• Bsp. für Verwendung eines Inferenzsystems: Manuel Chakravarty, Gabriele Keller, Simon Peyton Jones, Simon Marlow, Associated Types with Class, POPL 2005

  Absch. 4.2 (Fig. 2) Grundbereich: $\mathrm{\Theta }|\mathrm{\Gamma }⊢e:\sigma$

  means that in type environment $\mathrm{\Gamma }$ and instance environment $\mathrm{\Theta }$ the expression $e$ has type $\sigma$

  Bsp. für ein Regelschema: ${\displaystyle \frac{(v:\sigma )\in \mathrm{\Gamma }}{\mathrm{\Theta }|\mathrm{\Gamma }⊢v:\sigma }(\text{textsl}var)}$

Inferenz von Werten

• Grundbereich: Aussagen $\mathsf{wert}(p,z)$ mit $p\in \mathtt{\text{Exp}}$ , $z\in \mathbb{Z}$

  data Exp = Const Integer
           | Plus Exp Exp | Times Exp Exp

• Axiome: $\mathsf{wert}(\mathtt{\text{Const}}z,z)$

• Regeln:

  ${\displaystyle \frac{\mathsf{wert}(X,a),\mathsf{wert}(Y,b)}{\mathsf{wert}(\mathtt{\text{Plus}}XY,a+b)},\frac{\mathsf{wert}(X,a),\mathsf{wert}(Y,b)}{\mathsf{wert}(\mathtt{\text{Times}}XY,a\cdot b)},\dots }$

• das ist syntaxgesteuerte Semantik:

  für jeden Konstruktor von $p\in \mathtt{\text{Exp}}$
  gibt es genau eine Regel mit Konklusion $\mathsf{wert}(p,\dots )$

Umgebungen (Spezifikation)

• Grundbereich: Aussagen der Form $\mathsf{wert}(E,p,z)$

  (in Umgebung $E$ hat Programm $p$ den Wert $z$)

  Umgebungen konstruiert aus $\mathrm{\varnothing }$ und $E[v:=b]$

• Regeln für Operatoren ${\displaystyle \frac{\mathsf{wert}(E,X,a),\mathsf{wert}(E,Y,b)}{\mathsf{wert}(E,\mathtt{\text{Plus}}XY,a+b)},\dots }$

• Regeln für Umgebungen ${\displaystyle \frac{}{\mathsf{wert}(E[v:=b],v,b)},\frac{\mathsf{wert}(E,v^{\prime },b^{\prime })}{\mathsf{wert}(E[v:=b],v^{\prime },b^{\prime })}}$ für $v\ne v^{\prime }$

• Regeln für Bindung: ${\displaystyle \frac{\mathsf{wert}(E,X,b),\mathsf{wert}(E[v:=b],Y,c)}{\mathsf{wert}(E,\mathtt{let}v=X\mathtt{in}Y,c)}}$

Umgebungen (Implementierung)

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Integer

Operationen:

• empty :: Env leere Umgebung

• lookup :: Env -> String -> Integer

  Notation: $e(x)$

• extend :: String -> Integer -> Env -> Env

  Notation: $e[v:=z]$

Beispiel

lookup (extend  "y" 4 (extend "x" 3 empty)) "x"

entspricht $(\mathrm{\varnothing }[x:=3][y:=4])x$

Übung

1. Primalitäts-Zertifikate

   • welche von $2,4,8$ sind primitive Wurzel mod 101?

   • vollst. Primfaktorzerlegung von 100 angeben

   • ein vollst. Prim-Zertifikat für 101 angeben.

   • bestimmen Sie $2^{(101-1)/5}\mathrm{mod}101$ von Hand

     Hinweise: 1. das sind nicht 20 Multiplikationen,

     2. es wird nicht mit riesengroßen Zahlen gerechnet.

2. Geben Sie den vollständigen Ableitungsbaum an für die Auswertung von

   let {x = 5} in let {y = 7} in x

Semantische Bereiche

• bisher: Wert eines arithmetischen Ausdrucks ist Zahl.

• jetzt erweitern (Motivation: if-then-else mit richtigem Typ):

  data Val = ValInt Int
           | ValBool Bool

• typische Verarbeitung:

  value env x = case x of 
    Plus l r ->
      case value env l of
        ValInt l ->
          case value env r of
            ValInt r -> 
              ValInt ( i + j )

Continuations

• Programmablauf-Abstraktion durch Continuations:

  with_int  :: Val -> (Int  -> Val) -> Val
  with_int v k = case v of
      ValInt i -> k i
      _ -> error "expected ValInt"

  k ist die continuation (die Fortsetzung im Erfolgsfall)

• eben geschriebenen Code refaktorisieren zu:

  value env x = case x of 
      Plus l r -> 
          with_int ( value env l ) $ \ i -> 
          with_int ( value env r ) $ \ j -> 
          ValInt ( i + j )

Aufgaben

1. Bool im Interpreter

   • Boolesche Literale

   • relationale Operatoren (==, <, o.ä.),

   • Inferenz-Regel(n) für Auswertung des If

   • Implementierung der Auswertung von if/then/else mit with_bool,

2. Striktheit der Auswertung

   • einen Ausdruck e :: Exp angeben, für den value undefined e eine Exception ist (zwei mögliche Gründe: nicht gebundene Variable, Laufzeit-Typfehler)

   • mit diesem Ausdruck: diskutiere Auswertung von let {x = e} in 42

3. bessere Organisation der Quelltexte

   • Cabalisierung (Quelltexte in src/, Projektbeschreibungsdatei cb.cabal), Anwendung: cabal repl usw.

   • separate Module für Exp, Env, Value,

Beispiele

• in verschiedenen Prog.-Sprachen gibt es verschiedene Formen von Unterprogrammen:

  • Prozedur, sog. Funktion, Methode, Operator, Delegate, anonymes Unterprogramm

• allgemeinstes Modell:

  • Kalkül der anonymen Funktionen (Lambda-Kalkül),

Interpreter mit Funktionen

• abstrakte Syntax:

  data Exp = ...
    | Abs { par :: Name , body :: Exp }
    | App { fun :: Exp  , arg :: Exp }

• konkrete Syntax:

  let { f = \ x -> x * x }  in  f (f 3)

• konkrete Syntax (Alternative):

  let { f x = x * x }  in  f (f 3)

Semantik (mit Funktionen)

• erweitere den Bereich der Werte:

  data Val = ... | ValFun ( Val -> Val )

• erweitere Interpreter:

  value :: Env -> Exp -> Val
  value env x = case x of
      ... | Abs n b -> _ | App f a -> _

• mit Hilfsfunktion with_fun :: Val -> ...

• Testfall (in konkreter Syntax)

  let { x = 4 } in  let { f = \ y -> x * y }
      in  let { x = 5 }  in  f x

Let und Lambda

• let { x = A } in Q

  kann übersetzt werden in

  (\ x -> Q) A

• let { x = a , y = b } in Q

  wird übersetzt in …

• beachte: das ist nicht das let aus Haskell

Mehrstellige Funktionen

…simulieren durch einstellige:

• mehrstellige Abstraktion:

  \ x y z -> B := \x -> (\y -> (\z -> B ))

• mehrstellige Applikation:

  f P Q R    :=   ((f P) Q) R

  (die Applikation ist links-assoziativ)

• der Typ einer mehrstelligen Funktion:

  T1 -> T2 -> T3 -> T4   :=
     T1 -> (T2 -> (T3 -> T4))

  (der Typ-Pfeil ist rechts-assoziativ)

Semantik mit Closures

• bisher: ValFun ist Funktion als Datum der Gastsprache

  value env x = case x of ...
    Abs n b -> ValFun $ \ v -> 
      value (extend n v env) b
    App f a -> 
      with_fun ( value env f ) $ \ g -> 
      with_val ( value env a ) $ \ v -> g v

• alternativ: Closure: enthält Umgebung env und Code b

  value env x = case x of ...
    Abs n b -> ValClos env n b
    App f a -> ...

Closures (Spezifikation)

• Closure konstruieren (Axiom-Schema):

  ${\displaystyle \frac{}{\mathsf{wert}(E,\lambda n.b,\mathsf{Clos}(E,n,b))}}$

• Closure benutzen (Regel-Schema, 3 Prämissen)

  ${\displaystyle \frac{\begin{array}{c}\mathsf{wert}(E_1,f,\mathsf{Clos}(E_2,n,b)),\\ \mathsf{wert}(E_1,a,w),\mathsf{wert}(E_2[n:=w],b,r)\end{array}}{\mathsf{wert}(E_1,fa,r)}}$

• Ü: Inferenz-Baum für Auswertung des vorigen Testfalls (geschachtelte Let) zeichnen

• …oder Interpreter so erweitern, daß dieser Baum ausgegeben wird

Rekursion?

• Das geht nicht, und soll auch nicht gehen:

  let { x = 1 + x } in x

• aber das hätten wir doch gern:

  let { f = \ x -> if x > 0 
                   then x * f (x -1) else 1 
      } in  f 5

  (nächste Woche)

• aber auch mit nicht rekursiven Funktionen kann man interessante Programme schreiben:

Testfall (2)

let { t f x = f (f x) }
in  let { s x = x + 1 }
    in  t t t t s 0

• auf dem Papier den Wert bestimmen

• mit selbstgebautem Interpreter ausrechnen

• mit Haskell ausrechnen

• in JS (node) ausrechnen

Repräsentation von Fehlern

• Fehler explizit im semantischen Bereich des Interpreters repräsentieren (anstatt als Exception der Gastsprache)

  data Val = ... | ValErr Text

• strikte Semantik: ValErr niemals in Umgebung (bei Let-Bindung oder UP-Aufruf)

• Ü: realisieren durch Aufruf (an geeigneten Stellen) von

  with_val :: Val -> (Val -> Val) -> Val
  with_val v k = case v of
    ValErr _ -> v
    _ -> k v

Übungen

1. eingebaute primitive Rekursion (Induktion über Peano-Zahlen):

   implementieren Sie die Funktion fold :: r -> (r -> r) -> N -> r

   Testfall: fold 1 (\x -> 2*x) 5 == 32

   durch data Exp = .. | Fold .. und neuen Zweig in value

   Wie kann man damit die Fakultät implementieren?

2. alternative Implementierung von Umgebungen

   • bisher type Env = Id -> Val

   • jetzt type Env = Data.Map.Map Id Val oder Data.HashMap

   Messung der Auswirkungen: 1. Laufzeit eines Testfalls, 2. Laufzeiten einzelner UP-Aufrufe (profiling)

Motivation

1. Modellierung von Funktionen:

• intensional: Fkt. ist Berechnungsvorschrift, Programm

• (extensional: Fkt. ist Menge v. geordneten Paaren)

2. Notation mit gebundenen (lokalen) Variablen, wie in

• Analysis: $\int x^2\mathrm{d}x,\sum _{k=0}^n{k}^2$

• Logik: $\mathrm{\forall }x\in A:\mathrm{\forall }y\in B:P(x,y)$

• Programmierung: static int foo (int x) { ... }

Der Lambda-Kalkül

• ist der Kalkül für Funktionen mit benannten Variablen

• Alonzo Church, 1936 …Henk Barendregt, 1984 …

• die wesentliche Operation ist das Anwenden einer Funktion:

  $$(\lambda x.B)A{\to }_{\beta }B[x:=A]$$

  Beispiel: $(\lambda x.x\ast x)(3+2){\to }_{\beta }(3+2)\ast (3+2)$

• Im reinen Lambda-Kalkül gibt es nur Funktionen

  (keine Zahlen, Wahrheitswerte usw.)

Lambda-Terme

• Menge $\mathrm{\Lambda }$ der Lambda-Terme

  (mit Variablen aus einer Menge $V$):

  • (Variable) wenn $x\in V$, dann $x\in \mathrm{\Lambda }$

  • (Applikation) wenn $F\in \mathrm{\Lambda },A\in \mathrm{\Lambda }$, dann $(FA)\in \mathrm{\Lambda }$

  • (Abstraktion) wenn $x\in V,B\in \mathrm{\Lambda }$, dann $(\lambda x.B)\in \mathrm{\Lambda }$

  Beispiele: $x,(\lambda x.x),((xz)(yz)),(\lambda x.(\lambda y.(\lambda z.((xz)(yz)))))$

• verkürzte Notation (Klammern weglassen)

  • $(\dots ((F{A}_1)A_2)\dots A_n)\sim F{A}_1{A}_2\dots A_n$

  • $\lambda x_1.(\lambda x_2.\dots (\lambda x_n.B)\dots )\sim \lambda x_1{x}_2\dots x_n.B$

  mit diesen Abkürzungen simuliert $(\lambda x_1\dots x_n.B)A_1\dots A_n$ eine mehrstellige Funktion und -Anwendung

Eigenschaften der Reduktion

• ${\to }_{\beta }$ auf $\mathrm{\Lambda }$ ist nicht terminierend (es gibt Terme mit unendlichen Ableitungen)

  $W=\lambda x.xx,\mathrm{\Omega }=WW$.

• es gibt Terme mit Normalform und unendlichen Ableitungen, $KI\mathrm{\Omega }$ mit $K=\lambda xy.x,I=\lambda x.x$

• ${\to }_{\beta }$ auf $\mathrm{\Lambda }$ ist konfluent

  $\mathrm{\forall }A,B,C\in \mathrm{\Lambda }:A{\to }_{\beta }^{\ast }B\wedge A{\to }_{\beta }^{\ast }C\Rightarrow \mathrm{\exists }D\in \mathrm{\Lambda }:B{\to }_{\beta }^{\ast }D\wedge C{\to }_{\beta }^{\ast }D$

• Folgerung: jeder Term hat höchstens eine Normalform

Beziehung zur Semantik des Interpreters

• $\lambda$-Kalkül: Rel. ${\to }_{\beta }$ substituiert Variablen im Term

  schwache Reduktion: wie ${\to }_{\beta }$, aber niemals unter $\lambda$

  unser Interpreter: realisiert schwache Reduktion, Regeln für $\mathsf{wert}(E,X,w)$ speichern Substitutionen in Umgebung

• ein Zusammenhang wird hergestellt durch Kalküle für explizite Substitutionen,

  Pierre-Louis Curien: An Abstract Framework for Environment Machines, TCS 82 (1991),

  https://doi.org/10.1016/0304-3975(91)90230-Y

  Abadi, Cardelli, Curien, Levy: Explicit Substitutions, JFP 1991,

  https://doi.org/10.1017/S0956796800000186,

Daten als Funktionen

• Simulation von Daten (Tupel)
  durch Funktionen (Lambda-Ausdrücke):

  • Konstruktor: $⟨D_1,\dots ,D_k⟩:=\lambda s.s{D}_1\dots D_k$

  • Selektoren: $s_i^k:=\lambda t.t(\lambda d_1\dots d_k.d_i)$

  es gilt $s_i^k⟨D_1,\dots ,D_k⟩{\to }_{\beta }^{\ast }{D}_i$

  Ü: überprüfen für $k=2$

• Anwendungen:

  • Modellierung von Listen, Zahlen

  • Auflösung simultaner Rekursion

Lambda-Kalkül als universelles Modell

• Wahrheitswerte:

  $\mathsf{\text{True}}:=\lambda xy.x,\mathsf{\text{False}}:=\lambda xy.y$

• Verzweigung: $\mathtt{\text{if}}b\mathtt{\text{then}}x\mathtt{\text{else}}y:=bxy$

• natürliche Zahlen als iterierte Paare (Ansatz)

  $(0):=⟨\mathsf{\text{True}},\lambda x.x⟩;(n+1):=⟨\mathsf{\text{False}},n⟩$

• $s_2^2$ ist partielle Vorgänger-Funktion: $s_2^2(n+1)=n$

• Verzweigung: $\mathtt{\text{if}}a=0\mathtt{\text{then}}x\mathtt{\text{else}}y:=s_1^{2}axy$

• Ü: nachrechnen. Ü: das geht sogar mit $(0)=\lambda x.x$

• Rekursion?

Fixpunkt-Kombinatoren (Motivation)

• Beispiel: die Fakultät

  f = \ x -> if x=0 then 1 else x*f(x-1)

  erhalten wir als Fixpunkt einer Fkt. 2. Ordnung

  g = \ h x -> if x=0 then 1 else x * h(x-1)
  f = fix g   -- d.h., f = g f

• Ü: $g(\lambda z.z)7$, Ü: $\mathtt{\text{fix}}g7$

• Implementierung von fix mit Rekursion:

  fix g = g (fix g)

• es geht aber auch ohne Rekursion. Ansatz: $\mathtt{\text{fix}}=AA$,

  dann $\mathtt{\text{fix}}g=AAg=g(AAg)=g(\mathtt{\text{fix}}g)$

  eine Lösung ist $A=\lambda xy.\dots$

Fixpunkt-Kombinatoren (Implementierung)

• Definition (der Fixpunkt-Kombinator von Turing)

  $\mathrm{\Theta }=(\lambda xy.(y(xxy)))(\lambda xy.(y(xxy)))$

• Satz: $\mathrm{\Theta }f{\to }_{\beta }^{\ast }f(\mathrm{\Theta }f)$, d. h. $\mathrm{\Theta }f$ ist Fixpunkt von $f$

• Folgerung: im Lambda-Kalkül kann man simulieren:

  • Daten: Zahlen, Tupel von Zahlen

  • Programmablaufsteuerung durch:

    • Nacheinanderausführung:

      Verkettung von Funktionen

    • Verzweigung,

    • Wiederholung: durch Rekursion (mit Fixpunktkomb.)

Lambda-Berechenbarkeit

Satz: (Church, Turing)

• Menge der Turing-berechenbaren Funktionen

  (Zahlen als Wörter auf Band)

  Alan Turing: On Computable Numbers, with an Application to the Entscheidungsproblem, Proc. LMS, 2 (1937) 42 (1) 230–265 https://dx.doi.org/10.1112/plms/s2-42.1.230

• Menge der Lambda-berechenbaren Funktionen

  (Zahlen als Lambda-Ausdrücke)

  Alonzo Church: A Note on the Entscheidungsproblem, J. Symbolic Logic 1 (1936) 1, 40–41

• Menge der while-berechenbaren Funktionen

  (Zahlen als Registerinhalte)

Kodierung von Zahlen nach Church

• $c:\mathbb{N}\to \mathrm{\Lambda }:n\mapsto \lambda fx.f^n(x)$

  mit $f^0(x):=x,f^{n+1}(x):=f(f^n(x))$

• in Haskell: c n f x = iterate f x !! n

• Decodierung: d e = e (\x -> x+1) 0

• Nachfolger: $s(c_n)=c_{n+1}$ für $s=\lambda nfx.f(nfx)$

  1. auf Papier beweisen, 2. mit leancheck prüfen

  benutze check $ \ (Natural x) -> ...

• Addition: $\mathtt{\text{plus}}{c}_a{c}_b=c_{a+b}$ für $\mathtt{\text{plus}}=\lambda abfx.af(bfx)$

• implementiere die Multiplikation, beweise, prüfe

• Potenz: $\mathtt{\text{pow}}{c}_a{c}_b=c_{a^b}$ für $\mathtt{\text{pow}}=\lambda ab.ba$

Übung Lambda-Kalkül (I)

• die Fakultät (z.B. von 7) …

  • in Haskell (ohne Rekursion, aber mit Data.Function.fix)

  • in unserem Interpreter (ohne Rekursion, mit Turing-Fixpunktkombinator $\mathrm{\Theta }$)

  • in Javascript (ohne Rekursion, mit $\mathrm{\Theta }$)

• Kodierung von Wahrheitswerten und Zahlen (nach Church)

  • implementiere Test auf 0: $\mathtt{\text{iszero}}{c}_n=$ if $n=0$ then $\mathsf{\text{True}}$ else $\mathsf{\text{False}}$

  • implementiere Addition, Multiplikation, Fakultät

    ohne If, Eq, Const, Plus, Times

  • für nützliche Ausgaben: das Resultat nach ValInt dekodieren (dabei muß Plus und Const benutzt werden)

Übung Lambda-Kalkül (II)

folgende Aufgaben aus H. Barendregt: Lambda Calculus

• (Abschn. 6.1.5) gesucht wird $F$ mit $Fxy=FyxF$.

  Musterlösung: es gilt $F=\lambda xy.FyxF=(\lambda fxy.fyxf)F$,

  also $F=\mathrm{\Theta }(\lambda fxy.fyxf)$

• (Aufg. 6.8.2) Konstruiere $K^{\mathrm{\infty }}\in {\mathrm{\Lambda }}^0$ (ohne freie Variablen) mit $K^{\mathrm{\infty }}x=K^{\mathrm{\infty }}$ (hier und in im folgenden hat $=$ die Bedeutung $({\to }_{\beta }\cup {\to }_{\beta }^{-}{)}^{\ast }$

• Konstruiere $A\in {\mathrm{\Lambda }}^0$ mit $Ax=xA$

• beweise den Doppelfixpunktsatz (Kap. 6.5)

  $\mathrm{\forall }F,G:\mathrm{\exists }A,B:A=FAB\wedge B=GAB$

• (Aufg. 6.8.17, B. Friedman) Konstruiere Null, Nulltest, partielle Vorgängerfunktion für Zahlensystem mit Nachfolgerfunktion $s=\lambda x.⟨x⟩$ (das 1-Tupel)

• (Aufg. 6.8.14, J. W. Klop) $$\begin{array}{rlr}& & X=\lambda abcdefghijklmnopqstuvvxyzr.\\ & & r(thisisafixedpointcombinator)\\ & & Y=X^{27}=\underset{27}{\underbrace{X\dots X}}\end{array}$$ Zeige, daß $Y$ ein Fixpunktkombinator ist.

Motivation

Das ging bisher gar nicht:

let { f = \ x -> if x > 0 
                 then x * f (x -1) else 1 
    } in  f 5

Lösung 1: benutze Fixpunktkombinator

let { Theta =  ... } in
let { f = Theta ( \ g -> \ x -> if x > 0
                 then x * g (x - 1) else 1 )
    } in f 5

Lösung 2 (später): realisiere Fixpunktberechnung im Interpreter (neuer AST-Knotentyp Fix)

Existenz von Fixpunkten

Fixpunkt von $f::C\to C$ ist $x::C$ mit $fx=x$.

Existenz? Eindeutigkeit? Konstruktion?

Satz: Wenn $C$ pointed CPO und $f$ stetig,
dann besitzt $f$ genau einen kleinsten Fixpunkt.

• CPO $=$ complete partial order $=$ vollständige Halbordnung

• complete $=$ jede monotone Folge besitzt Supremum ($=$ kleinste obere Schranke)

• pointed: $C$ hat kleinstes Element $\mathrm{\perp }$

Ü (Wdhlg) Def. obere Schranke, Supremum

Beispiele f. Halbordnungen, CPOs

Halbordnung? pointed? complete?

• $\le$ auf $\mathbb{N}$

• $\le$ auf $\mathbb{N}\cup \{+\mathrm{\infty }\}$

• $\le$ auf $\{x\mid x\in \mathbb{R},0\le x\le 1\}$

• $\le$ auf $\{x\mid x\in \mathbb{Q},0\le x\le 1\}$

• Teilbarkeit auf $\mathbb{N}$

• Präfix-Relation auf ${\mathrm{\Sigma }}^{\ast }$

• $\{((x_1,y_1),(x_2,y_2))\mid (x_1\le x_2)\vee (y_1\le y_2)\}$ auf ${\mathbb{R}}^2$

• $\{((x_1,y_1),(x_2,y_2))\mid (x_1\le x_2)\wedge (y_1\le y_2)\}$ auf ${\mathbb{R}}^2$

• Relation $\subseteq$ auf $\{\{A\},\{B\},\{A,B\}\}$

• identische Relation ${\mathrm{id}}_M$ auf einer beliebigen Menge $M$

• $\{(\mathrm{\perp },x)\mid x\in M_{\mathrm{\perp }}\}\cup {\mathrm{id}}_M$ auf $M_{\mathrm{\perp }}:=\{\mathrm{\perp }\}\cup M$

Stetige Funktionen

$f$ ist stetig $:=$

• $f$ ist monoton: $x\le y\Rightarrow f(x)\le f(y)$

• und für monotone Folgen $[x_0,x_1,\dots ]$ gilt: $f(sup[x_0,x_1,\dots ])=sup[f(x_0),f(x_1),\dots ]$

Beispiele: in $(\mathbb{N}\cup \{+\mathrm{\infty }\},\le )$

• $x\mapsto 42$ ist stetig

• $x\mapsto$ if $x<+\mathrm{\infty }$ then $x+1$ else $+\mathrm{\infty }$

• $x\mapsto$ if $x<+\mathrm{\infty }$ then $42$ else $+\mathrm{\infty }$

Satz: Wenn $C$ pointed CPO und $f:C\to C$ stetig,
dann besitzt $f$ genau einen kleinsten Fixpunkt …

Beweis: …und dieser ist $sup[\mathrm{\perp },f(\mathrm{\perp }),f^2(\mathrm{\perp }),\dots ]$

CPO auf Menge von Funktionen

• Menge der partiellen Funktionen von $B$ nach $B$:

  $C=(B\hookrightarrow B)$

• partielle Funktion $f:B\hookrightarrow B$
  entspricht totaler Funktion $f:B\to B_{\mathrm{\perp }}$

• $C$ geordnet durch $f\le g⟺\mathrm{\forall }x\in B:f(x)\le g(x)$,

  wobei $\le$ die vorhin definierte CPO auf $B_{\mathrm{\perp }}$

• $f\le g$ bedeutet: $g$ ist Verfeinerung von $f$

• Das Bottom-Element von $C$ ist die überall undefinierte Funktion. (diese heißt auch $\mathrm{\perp }$)

Funktionen als CPO, Beispiel

• der Operator $F=$

  \ g -> ( \ x -> if (x==0) then 0
                  else 2 + g (x - 1) )

  ist stetig auf $(\mathbb{N}\hookrightarrow \mathbb{N})$ (Beispiele nachrechnen!)

• Iterative Berechnung des Fixpunktes: $$\begin{array}{rlr}\mathrm{\perp }& =& \mathrm{\varnothing }\text{überall undefiniert}\\ F\mathrm{\perp }& =& \{(0,0)\}\\ F(F\mathrm{\perp })& =& \{(0,0),(1,2)\}\\ F^3\mathrm{\perp }& =& \{(0,0),(1,2),(2,4)\}\end{array}$$

• $sup[\dots ,F^k\mathrm{\perp },\dots ]=\{(x,2x)\mid x\in \mathbb{N}\}$

Welche Funktionale sind stetig?

• die Erfahrung (der Programmierung mit rekursiven Funktionen) lehrt: alle Operatoren \g -> \x -> .. g .. sind stetig.

• denn die Semantik der (von uns bisher benutzten) AST-Konstruktoren bildet stetige Ftk. auf stetige Fkt. ab

• Ü: $(\lambda x.\mathsf{\text{if}}x=\mathrm{\perp }\mathsf{\text{then}}42\mathsf{\text{else}}\mathrm{\perp })$ ist nicht stetig.

• Diskussion: eine solche Funktion kann nicht die Semantik eines Programms sein, weil das Halteproblem nicht entscheidbar ist

Fixpunkte und Laziness

• Fixpunkte existieren in pointed CPOs.

  • (Maschinen-) Zahlen: nicht pointed

    (arithmetische Operatoren sind strikt)

  • (Haskell-) Daten (Listen, Bäume usw.): pointed:

    (Konstruktoren sind nicht strikt)

  • Funktionen (Unterprogramme):

    Abstraktion ($\lambda$) ist nicht strikt, in jeder Sprache!

• Beispiele in Haskell:

  fix f = f (fix f)
  xs = fix $ \ zs -> 1 : zs
  g = fix $ \h -> \x -> if x==0 then 1 else x*h(x-1)

• in Sprachen mit strikter Semantik üblicherweise:

  keine rekursiven Daten, aber rekursive Unterprogramme

Fixpunktberechnung im Interpreter

• Erweiterung der abstrakten Syntax:

  data Exp = ... | Rec Name Exp

• Beispiel

  App 
    (Rec g (Abs v (if v==0 then 0 else 2 + g(v-1))))
    5

• Bedeutung: Rec x B ist Fixpunkt von $(\lambda x.B)$

• Semantik: ${\displaystyle \frac{\mathsf{wert}(E,(\lambda x.B)(\mathsf{\text{Rec}}xB),v)}{\mathsf{wert}(E,\mathsf{\text{Rec}}xB,v)}}$

• Ü: verwende Let statt App (Abs ..) ..

• Ü: das Beispiel mit dieser Regel auswerten

Arithmetik mit Bedarfsauswertung

• über $\mathbb{Q}$ hat $f=\lambda x.1+x/4$ einen Fixpunkt ($4/3$),

  aber $\underset{k}{sup}{f}^k\mathrm{\perp }=\mathrm{\perp }$, weil die Operationen strikt sind.

• wirklich? Kommt auf die Repräsentation der Zahlen an!

  Op. auf Maschinenzahlen sind strikt. — Aber:

• Zahl als lazy Liste von Ziffern (Bsp: Basis 2)

  x=plus(1:repeat 0)(0:0:x)=[1,0,1,0,1,0..]

• Ü: bestimme $y=\sqrt{2}-1$ aus $2=(1+y{)}^2$,

  d.h., als Fixpunkt von $\lambda y.(1-y^2)/2$

• Kombiniere https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.4249 (Jerzy Karczmarczuk 1998), http://joerg.endrullis.de/publications/productivity/

Simultane Rekursion: letrec

• Beispiel (aus: D. Hofstadter, Gödel Escher Bach, 1979)

  letrec { f = \ x -> if x == 0 then 1 
                      else x - g(f(x-1))
         , g = \ x -> if x == 0 then 0 
                      else x - f(g(x-1))
  } in f 15

  Bastelaufgabe: für welche $x$ gilt $f(x)\ne g(x)$?

• weitere Beispiele:

  letrec { y = x * x, x = 3 + 4  } in x - y
  letrec { f = \ x -> .. f (x-1) } in f 3

letrec nach rec (falsch)

• Plan: mit Lambda-Ausdrücken für Konstruktor, Selektor

  LetRec [(n1,x1), .. (nk,xk)] y   
  => ( rec t ( let n1 = select1 t
                   ...
                   nk = selectk t
               in  tuple x1 .. xk ) )
     ( \ n1 .. nk -> y )

• benutzt $⟨x_1,\dots ,x_k⟩f=f{x}_1\dots x_k$

• terminiert nicht, die Auswertungsstrategie des Interpreters ist dafür zu eifrig (eager)

• Lösung: tuple direkt unter rec t,

  let .. tuple .. $\Rightarrow$ tuple (let ..) (let ..)

letrec nach rec (richtig)

• Teilausdrücke (für jedes $i$)

  let { n1 = select1 t, ..  nk = selectk t 
      } in xi

  äquivalent vereinfachen zu t (\ n1 .. nk -> xi)

• LetRec [(n1,x1), .. (nk,xk)] y   
  => ( rec t 
        ( tuple ( t ( \ n1 .. nk -> x1 ))
                ...
                ( t ( \ n1 .. nk -> xk )) ))
     ( \ n1 .. nk -> y )

• Ü: implementiere letrec {f = _, g = _} in f 15

Übung Fixpunkte

1. Limes der Folge $F^k(\mathrm{\perp })$ für

   F h = \ x -> if x > 23 then x - 11 
                else h (h (x + 14))

2. Ist $F$ stetig? Gib den kleinsten Fixpunkt von $F$ an:

   F h =  \ x -> if x >= 2 then 1 + h(x-2) 
       else if x == 1 then 1 else h(4) - 2

   Hat $F$ weitere Fixpunkte?

3. $C=$ Menge der Formalen Sprachen über $\mathrm{\Sigma }=\{a,b\}$, halbgeordnet durch $\subseteq$. ist CPO? pointed?

   $g:C\to C:L\mapsto \{ϵ\}\cup \{a\}\cdot L\cdot \{b\}$ ist stetig? Fixpunkt(e)?

   $h:C\to C:L\mapsto \{a\}\cup L\cdot \{b\}\cdot ({\mathrm{\Sigma }}^{\ast }\setminus L)$

4. in der Relation $\subseteq$ auf $\{\{A\},\{B\},\{A,B\}\}$: geben Sie eine stetige Funktion an, die zwei verschiedene kleinste Fixpunkte besitzt.

   Ist das eine Widerspruch zum CPO-Theorem?

5. Geben Sie Argumente aus dieser Diskussion wieder: …distinguish bindings that are self-referentially recursive from non-recursive bindings https://github.com/ghc-proposals/ghc-proposals/pull/401 (O. Charles, 8. Febr. 2021)

   Vergleichen Sie mit let (rec) in OCaml (Primärquelle angeben, d.h., Sprachstandard)

   Für Haskell-Lückentext-Aufgaben in autotool: um die Benutzung von Rekursionsmustern zu erzwingen, wäre es nützlich, beliebige Rekursion zu verbieten.

Haskell-Software-Pakete

• Paket (package) $:=$ Quelltexte $+$ Beschreibung von

  • herstellbaren Artefakten

    (Bibliotheken, Executables, Testfälle)

  • benötigten Paketen (und Versionen-Constraints)

  Format der Beschreibung: Textdatei foo.cabal

• Paket-Sammlung: https://hackage.haskell.org/

• Build-Werkzeug: cabal install|test|repl

• Installation in $HOME/.cabal/{bin,lib,*},

  ist projekt-übergreifender Cache

Kuratierte Paket-Mengen

• Versions-Constraints in Cabal-Files können streng bis großzügig sein (oder ganz fehlen),

• gebaut wird mit den letzten passenden Hackage-Versionen, kann zu nicht reproduzierbaren Builds führen (oder schlimmer, cabal hell)

• https://stackage.org/ definiert Resolver (Bsp. LTS-14.14), das sind exakte Versionsnummern von konsistenten Paketmengen.

• Datei stack.yaml enthält Resolver und ggf. weitere Paketquellen (z.B. git-clone-URL)

• siehe auch https://www.imn.htwk-leipzig.de/~waldmann/etc/untutorial/haskell/build/

Continuous Intergration

• lokal:

  • im Editor: mit HIE https://github.com/haskell/haskell-ide-engine,

    benutzt Language Server Protocol https://microsoft.github.io//language-server-protocol/specifications/specification-3-17/

  • CLI: ghcid, siehe https://github.com/ndmitchell/ghcid

• remote: Beispiel siehe

  https://git.imn.htwk-leipzig.de/waldmann/haskell-ci-cabal-test https://git.imn.htwk-leipzig.de/waldmann/haskell-ci-stack-test

Haskell-Module

• Modul: benannte Menge von Definitionen (Werte, Typen)

  module M (M (), foo) where
  import C (f); import qualified D ;
  data M = A | B 
  foo :: M -> Bool ; foo x = ... f ..
  bar :: Int -> M ; bar y = ... D.g ..

• Ziele:

  • Abstraktion (z.B. Konstruktoren von M nicht exportiert)

    damit kann man Invarianten (hier: von M) erzwingen

  • getrennte Kompilation,

    aus M.hs entstehen M.o und M.hi

Modul-Abhängigkeiten

• Abhängigkeitsgraph $G$: Knoten $=$ Module,

  Kante $C\to M$, falls module M where import C

• Kompilation verwendet topologische Ordnung auf $G$

  (Kompilation von M benötigt C.hi) $\Rightarrow$ $G$ kreisfrei

• Kreise entfernen: Env = Map Name Val, Val = .. | ValClos Name Exp Env

  durch Typargumente Env k v = Map k v

  Ü: Beziehung zw. Val und Action?

• Kreiskante $C\to M$ entfernen: File M.hs-boot

  Typ- und data-Deklarationen ohne Konstruktoren

  module C where import {-# SOURCE #-} M

  https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/separate_compilation.html#how-to-compile-mutually-recursive-modules

Motivation

bisherige Programme sind nebenwirkungsfrei, das ist nicht immer erwünscht:

• direktes Rechnen auf von-Neumann-Maschine: Änderungen im Hauptspeicher

• direkte Modellierung von Prozessen mit Zustandsänderungen ((endl.) Automaten)

Dazu muß semantischer Bereich geändert werden.

• bisher: Val, jetzt: State -> (State, Val)
  (dabei ist (A,B) die Notation für $A\times B$)

Semantik von (Teil-)Programmen ist Zustandsänderung.

Speicher (Daten)

• Implementierung benutzt größenbalancierte Suchbäume

  http://hackage.haskell.org/package/containers/docs/Data-Map.html

• Notation mit qualifizierten Namen:

  import qualified Data.Map as M
  newtype Addr = Addr Int 
  type Store = M.Map Addr Val

• newtype: wie data mit genau einem Konstruktor,

  Konstruktor wird zur Laufzeit nicht repräsentiert

• Aktion: liefert neue Speichernbelegung und Resultat

  newtype Action a = 
      Action ( Store -> ( Store, a ))

Speicher (Operationen)

• newtype Action a = Action ( Store -> ( Store, a ))

• spezifische Aktionen:

  new :: Val -> Action Addr
  get :: Addr -> Action Val
  put :: Addr -> Val -> Action ()

• Aktion ausführen, Resultat liefern (Zielzustand ignorieren)

  run :: Store -> Action a -> a

• Aktionen nacheinander ausführen

  bind :: Action a ->  ... Action b -> Action b

  Aktion ohne Zustandsänderung result :: a -> Action a

Auswertung von Ausdrücken

• Ausdrücke (mit Nebenwirkungen):

  date Exp = ... 
     | New Exp | Get Exp | Put Exp Exp

• Resultattyp des Interpreters ändern:

  value    :: Env -> Exp ->        Val
           :: Env -> Exp -> Action Val

• semantischen Bereich erweitern:

  data Val = ... | ValAddr Addr

• Aufruf des Interpreters:

  run Store.empty $ value env0 $ ...

Änderung der Hilfsfunktionen

• bisher:

  with_int :: Val -> ( Int -> Val ) -> Val
  with_int v k = case v of
      ValInt i -> k i

• jetzt:

  with_int :: Action Val 
    -> ( Int -> Action Val ) -> Action Val
  with_int a k = bind a $ \ v -> case v of
      ValInt i -> k i

• Hauptprogramm muß kaum geändert werden (!)

Variablen?

in unserem Modell haben wir:

• veränderliche Speicherstellen,

• aber immer noch unveränderliche Variablen (lokale Namen)

$\Rightarrow$ der Wert eines Namens kann eine Speicherstelle sein, aber dann immer dieselbe.

Imperative Programmierung

es fehlen noch wesentliche Operatoren:

• Nacheinanderausführung (Sequenz)

• Wiederholung (Schleife)

diese kann man:

• simulieren (durch let)

• als neue AST-Knoten realisieren (Übung)

Rekursion

mehrere Möglichkeiten zur Realisierung

• im Lambda-Kalkül (in der interpretierten Sprache)

  mit Fixpunkt-Kombinator

• durch Rekursion in der Gastsprache des Interpreters

• simulieren (in der interpretierten Sprache)

  durch Benutzung des Speichers

Rekursion (operational)

• Idee: eine Speicherstelle anlegen und als Vorwärtsreferenz auf das Resultat der Rekursion benutzen

• Rec n (Abs x b)  ==> 
      a := new 42
      put a ( \ x -> let { n = get a } in b )
      get a

Speicher—Übung

Fakultät imperativ:

let { fak = \ n -> 
        { a := new 1 ;
          while ( n > 0 ) 
            { a := a * n ; n := n - 1; }
          return a; 
        }
    } in  fak 5

1. Schleife durch Rekursion ersetzen und Sequenz durch let:

   fak = let { a = new 1 }
         in  Rec f ( \ n -> ... )

2. Syntaxbaumtyp erweitern um Knoten für Sequenz und Schleife

…unter verschiedenen Aspekten

• unsere Motivation: semantischer Bereich,

  result :: a -> m a als wirkungslose Aktion,

  Operator bind :: m a -> (a -> m b) -> m b zum Verknüpfen von Aktionen

• auch nützlich: do-Notation (anstatt Ketten von >>=)

• die Wahrheit: a monad in X is just a monoid
  in the category of endofunctors of X

• die ganze Wahrheit:

  Functor m => Applicative m => Monad m

• weitere Anwendungen: IO, Parser-Kombinatoren,
  weitere semant. Bereiche (Continuations, Typisierung)

Die Konstruktorklasse Monad

• Definition (in Standardbibliothek)

  class Monad m where
      return  :: a -> m a
      ( >>= ) :: m a -> (a -> m b) -> m b

• Instanz (für benutzerdefinierten Typ)

  instance Monad Action where
    return = result ; (>>=) = bind

• Benutzung der Methoden:

  value e l >>= \ a ->
  value e r >>= \ b ->
  return ( a + b )

Do-Notation für Monaden

value e l >>= \ a ->
value e r >>= \ b ->
return ( a + b )

do-Notation (explizit geklammert):

do { a <- value e l
   ; b <- value e r
   ; return ( a + b )
   }

do-Notation (implizit geklammert):

do a <- value e l
   b <- value e r
   return ( a + b )

Haskell: implizite Klammerung nach let, do, case, where

Beispiele für Monaden

• Aktionen mit Speicheränderung (vorige Woche)

  Action (Store -> (Store, a))

• Aktionen mit Welt-Änderung: IO a

• Transaktionen (Software Transactional Memory) STM a

• Vorhandensein oder Fehlen eines Wertes

  data Maybe a = Nothing | Just a

• …mit Fehlermeldung

  data Either e a = Left e | Right a

• Nichtdeterminismus (eine Liste von Resultaten): [a]

• Parser-Monade (nächste Woche)

Die IO-Monade

data IO a -- abstract
instance Monad IO -- eingebaut

readFile :: FilePath -> IO String
putStrLn :: String -> IO ()

Alle Funktionen, deren Resultat von der Außenwelt (Systemzustand) abhängt, haben Resultattyp IO ..., sie sind tatsächlich Aktionen.

Am Typ einer Funktion erkennt man ihre möglichen Wirkungen bzw. deren garantierte Abwesenheit.

main :: IO ()
main = do 
   cs <- readFile "foo.bar" ; putStrLn cs

Grundlagen: Kategorien

• Kategorie $C$ hat Objekte ${\text{Obj}}_C$ und Morphismen ${\text{Mor}}_C$,

  jeder Morphismus $m$ hat als Start ($S$) und Ziel ($T$) ein Objekt, Schreibweise: $m:S\to T$ oder $m\in {\text{Mor}}_C(S,T)$

• für jedes $O\in {\text{Obj}}_C$ gibt es ${\text{id}}_O:O\to O$

• für $f:S\to M$ und $g:M\to T$ gibt es $f\circ g:S\to T$.

  es gilt immer $f\circ \text{id}=f$, $\text{id}\circ g=g$, $f\circ (g\circ h)=(f\circ g)\circ h$

Beispiele:

• Set: ${\text{Obj}}_{\text{Set}}$ = Mengen, ${\text{Mor}}_{\text{Set}}$ = totale Funktionen

• Grp: ${\text{Obj}}_{\text{Grp}}$ = Gruppen, ${\text{Mor}}_{\text{Grp}}$ = Homomorphismen

• für jede Halbordnung $(M,\le )$: $\text{Obj}=M,\text{Mor}=(\le )$

• Hask: ${\text{Obj}}_{\text{Hask}}$ = Typen, ${\text{Mor}}_{\text{Hask}}$ = Funktionen

Kategorische Definitionen und Sätze

Beispiel: Isomorphie

• eigentlich: Abbildung, die die Struktur (der abgebildeten Objekte) erhält

• Struktur von $O\in \text{Obj}(C)$ ist aber unsichtbar

• Eigenschaften von Objekten werden beschrieben
  durch Eigenschaften ihrer Morphismen
  (vgl. abstrakter Datentyp, API)

  Bsp: $f:A\to B$ ist Isomorphie (kurz: ist iso),
  falls es ein $g:B\to A$ gibt mit $f\circ g={\text{id}}_A\wedge g\circ f={\text{id}}_B$

weiteres Beispiel

• Def: $m:a\to b$ monomorph: $\mathrm{\forall }f,g:f\circ m=g\circ m\Rightarrow f=g$

• Satz: $f$ mono $\wedge$ $g$ mono $\Rightarrow$ $f\circ g$ mono.

Produkte

• Def: $P$ ist Produkt von $A_1$ und $A_2$
  mit Projektionen ${\text{proj}}_1:P\to A_1,{\text{proj}}_2:P\to A_2$,

  wenn für jedes $B$ und Morphismen $f_1:B\to A_1,f_2:B\to A_2$

  es existiert genau ein $g:B\to P$
  mit $g\circ {\text{proj}}_1=f_1$ und $g\circ {\text{proj}}_2=f_2$

• für Set ist das wirklich das Kreuzprodukt

• für die Kategorie einer Halbordnung?

• für Gruppen? (Beispiel?)

Dualität

• Wenn ein Begriff kategorisch definiert ist,

  erhält man den dazu dualen Begriff
  durch Spiegeln aller Pfeile

• Bsp: dualer Begriff zu Produkt (heißt Summe)

  Definition hinschreiben, Beispiele angeben

• Ü: dualer Begriff zu: mono (1. allgemein, 2. Mengen)

• entsprechend: die duale Aussage

  diese gilt gdw. die originale (primale) Aussage gilt

• Ü: duale Aussage für Komposition von mono.

Funktoren

• Def: Funktor $F$ von Kategorie $C$ nach Kategorie $D$:

  • Wirkung auf Objekte: $F_{\text{Obj}}:\text{Obj}(C)\to \text{Obj}(D)$

  • Wirkung auf Pfeile: $F_{\text{Mor}}:(g:s\to t)\mapsto (g^{\prime }:F_{\text{Obj}}(S)\to F_{\text{Obj}}(T))$

  mit den Eigenschaften:

  • $F_{\text{Mor}}({\text{id}}_o)={\text{id}}_{F_{\text{Obj}}(o)}$

  • $F_{\text{Mor}}(g{\circ }_{C}h)=F_{\text{Mor}}(g){\circ }_D{F}_{\text{Mor}}(h)$

• Bsp: Funktoren zw. Kategorien von Halbordnungnen?

• class Functor f where 
    fmap :: (a -> b) -> (f a -> f b)

  Beispiele: List, Maybe, Action

Die Kleisli-Konstruktion

• Plan: für Kategorie $C$, Endo-Funktor $F:C\to C$

  definiere sinnvolle Struktur auf Pfeilen $s\to Ft$

• Durchführung: die Kleisli-Kategorie $K$ von $F$:

  $\text{Obj}(K)=\text{Obj}(C)$, Pfeile: $s\to Ft$

• …$K$ ist tatsächlich eine Kategorie, wenn:

  • identische Morphismen (return), Komposition (>=>)

  • mit passenden Eigenschaften

  $(F,\mathtt{\text{return}},\mathtt{\text{(>=>)}})$ heißt dann Monade

Diese Komposition ist f >=> g = \ x -> (f x >>= g)

Aus o.g. Forderung ($K$ ist Kategorie) ergibt sich Spezifikation für return und >>=

Functor, Applicative, Monad

https://wiki.haskell.org/Functor-Applicative-Monad_Proposal

class Functor f where 
  fmap :: (a -> b) -> (f a -> f b)
class Functor f => Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> (f a -> f b)
class Applicative m => Monad m where
  (>>=) :: m a -> (a -> m b) -> m b

eine Motivation: effizienterer Code für >>=,
wenn das rechte Argument eine konstante Funktion ist

(d.h. die Folge-Aktion hängt nicht vom Resultat der ersten Aktion ab: dann ist Monad nicht nötig, es reicht Applicative)

Die Maybe-Monade

data Maybe a = Nothing | Just a
instance Monad Maybe where ...

Beispiel-Anwendung:

case ( evaluate e l ) of
    Nothing -> Nothing
    Just a  -> case ( evaluate e r ) of
        Nothing -> Nothing
        Just b  -> Just ( a + b )

mittels der Monad-Instanz von Maybe:

evaluate e l >>= \ a ->
    evaluate e r >>= \ b ->
        return ( a + b)

Ü: dasselbe mit do-Notation

List als Monade

instance Monad [] where
    return = \ x - > [x]
    m >>= f = case m of 
        []     -> [] 
        x : xs -> f x ++ ( xs >>= f )

Beispiel:

do a <- [ 1 .. 4 ]
   b <- [ 2 .. 3 ]
   return ( a * b )

Anwendung: Ablaufsteuerung für Suchverfahren

Monaden: Zusammenfassung

• verwendet zur Definition semantischer Bereiche,

• Monade $=$ Monoid über Endofunktoren in Hask,

  (Axiome für return, >=> bzw. >>=)

• Notation do { x <- foo ; bar ; .. }

  (>>= ist das benutzer-definierte Semikolon)

• Grundlagen: Kategorien-Theorie (ca. 1960),

  in Funktl. Prog. seit ca. 1990 http://homepages.inf.ed.ac.uk/wadler/topics/monads.html

• in anderen Sprachen: F#: Workflows, C#: LINQ-Syntax

• GHC ab 7.10: Control.Applicative: pure und <*>

  ($=$ return und eingeschränktes >>=)

Monaden-Transformatoren

• Motivation: Kombination verschiedener Semantiken:

  • Zustands-Änderung (Action)

  • Fehlschlagen der Rechnung (Maybe)

  • Schritt-Zählen

  • Logging

  in einer Monade

• diese nicht selbst schreiben,

  sondern Monaden-Transformatoren verwenden, z.B.

  type Sem = ExceptT Err (StateT Store Identity)

• Standard-Bibliotheken dafür: transformers, mtl

Der Zustands-Transformator

• newtype StateT s m a 
    = StateT { runStateT :: s -> m (a,s) }

• die elementaren Operationen:

  get :: Monad m => StateT s m s
  put :: Monad m => s -> StateT s m ()

• instance Monad m => Monad (StateT s m)

• Anwendung auf

  newtype Identity a = Identity { runIdentity :: a}

  ergibt type State s = StateT s Identity

Der Ausnahme-Transformator MaybeT

• newtype MaybeT m a = 
    MaybeT { runMaybeT :: m (Maybe a) }

• Anwendung im Interpreter:

  type Sem = StateT Store (MaybeT Identity)
  with_int :: Sem Val->(Val -> Sem r)->Sem r
  with_int a k = a >>= \ case
    ValInt i -> k i   ;  _ -> lift Nothing

• benutzt Einbettung der inneren Monade:

  class MonadTrans t where 
    lift :: Monad m => m a -> t m a 
  instance MonadTrans (StateT s)

Der Ausnahme-Transformator ExceptT

• wie MaybeT, aber mit Fehlermeldungen (Exceptions)

  newtype ExceptT e m a = ExceptT (m (Either e a))
  instance Monad m => Monad (ExceptT e m)
  instance MonadTrans (ExceptT e)

• Operationen:

  runExceptT :: ExceptT e m a -> m (Either e a)
  throwE :: Monad m => e -> ExceptT e m a 
  catchE :: Monad m => ExceptT e m a -> (e -> ..) -> ..

• Ü: verwende Sem = StateT (ExceptT Err Id.) mit sinnvollem data Err = ..

• Ü: Unterschied zu ExceptT Err (StateT Id.)

Bibliotheken für Monaden-Transformatoren

• gemeinsame Grundlage: Mark P Jones: Functional Programming with Overloading and Higher-Order Polymorphism, AFP 1995, http://web.cecs.pdx.edu/~mpj/pubs/springschool.html (S. 36 ff.)

• https://hackage.haskell.org/package/transformers: wie hier beschrieben

• https://hackage.haskell.org/package/mtl: zusätzliche Typklassen und Instanzen

  class Monad m => MonadState s m | m -> s where
    get :: ... ; put :: ...
  instance MonadState s m => MonadState s (MaybeT m)

  dadurch braucht man fast keine lift zu schreiben

Aufgaben Kategorien

SS 24 : zur VL KW 22: Aufgaben 1, 2, 3 (b, c)

1. der identische Morphismus jedes Objektes ist eindeutig (das bedeutet: falls es ${\text{id}}_1,{\text{id}}_2$ gibt mit $\mathrm{\forall }f:{\text{id}}_k\circ f=f=f\circ {\text{id}}_k$, dann ${\text{id}}_1={\text{id}}_2$)

2. Definieren Sie den duale Begriff zu Monomorphismus. Geben Sie Beispiele und Gegenbeispiele für Monom. und duale Monom. in der Kategorie der Mengen an

3. Beweise: für das (kategorisch definierte) Produkt $P$ von endlichen Mengen $A_1,A_2$ gilt: $|P|=|A_1\times A_2|$.

   1. (Musterlösung) $|P|\ge |A_1\times A_2|$: indirekter Beweis.

      Falls $|P|<|A_1\times A_2|$, wähle $B=A_1\times A_2$, $f_i(x_1,x_2)=x_i$.

      Dann ist $g$ nicht injektiv: es gibt $x=(x_1,x_2)\ne (y_1,y_2)=y$, mit $g(x)=g(y)$.

      Für diese $x,y$ gilt $x_i\ne y_i$ für wenigstens ein $i\in \{1,2\}$.

      Aus $g\circ {\text{proj}}_i=f_i$ folgt $x_i=f_i(x)=(g\circ {\text{proj}}_i)(x)={\text{proj}}_i(g(x))={\text{proj}}_i(g(y))=(g\circ {\text{proj}}_i)(y)=f_i(y)=y_i$, Widerspruch.

   2. (Aufgabe) $|P|\le |A_1\times A_2|$

   3. Geben Sie eine entsprechende Aussage für das duale Produkt endlicher Mengen an und beweisen Sie diese.

4. Kategorie mit gerichteten Graphen als Objekte,

   $f:\mathsf{\text{V}}(G)\to \mathsf{\text{V}}(H)$ ist Morphismus, falls $\mathrm{\forall }x,y:(x,y)\in \mathsf{\text{E}}(G)⟺(f(x),f(y))\in \mathsf{\text{E}}(H)$.

   Was bedeuten dort mono, epi?

   Produkt, Summe? Welche Graph-Operationen (aus VL Modellierung) haben die passenden Eigenschaften?

Aufgaben Monaden

SS 24: zu KW 22: Aufgaben 1, 3, 4

1. (Functor, Monad für Action)

   1. implementieren Sie instance Functor Action direkt.

      überprüfen Sie die Funktor-Gesetze an Beispielen.

   2. eine indirekte Implementierung ist

      instance Functor m where fmap f a = a >>= \ x -> return (f x)

      Beweisen Sie: für jede Monade m erfüllt dieses fmap die Funktor-Gesetze.

2. die Konstruktorklasse Applicative hat unter anderem diese Methoden

   class Functor f => Applicative f where
     pure :: a -> f a
     (<*>) :: f (a -> b) -> f a -> f b
     liftA2 :: (a -> b -> c) -> f a -> f b -> f c

   im folgenden geht es nur um statische Semantik (Typkorrektheit), (noch) nicht um dynamische Semantik (Axiome)

   1. Implementieren Sie (<*>) durch liftA2

   2. Implementieren Sie liftA2 durch (<*>)

   3. geben Sie eine Implementierung für liftA2 mit Monaden-Operationen an. (Beachte: andersherum geht das nicht, denn nicht jedes Applicative ist auch Monade)

   4. was ist the monad of no return?

3. Funktor- und Monadengesetze (mit leancheck in ghci)

   cabal install --lib leancheck
   
   import Test.LeanCheck
   import Test.LeanCheck.Function 
   -- Kleisli-Komposition:
   import Control.Monad ((>=>)) 
   
   :set -XPatternSignatures
   
   -- return ist rechts neutral
   check $ \ (f:: Bool -> Maybe Bool) x -> (f x == (return >=> f) x)
   
   -- ein Test, der zeigt, daß eine falsche Aussage erkannt wird:
   check $ \ (f:: Bool -> Maybe Bool) x -> (f x == (f >=> f) x)

4. falsche Functor-/Monad-Instanzen für Maybe, List, Tree (d.h. typkorrekt, aber semantisch falsch)

   Standard-Datentyp mit newtype verpacken

   newtype List a = List [a]
   instance Functor List where
     -- korrekte Instanz für List
     fmap f (List xs) =
       -- benutzt korrekte Instanz für []
       List (fmap f xs) 

   oder strukturgleichen Typ selbst definieren

   import Prelude hiding (Maybe)
   data Maybe a = Nothing | Just a deriving (Eq, Show)
   instance Monad Maybe where ...

5. StateT Int zum Zählen der Auswertungsschritte (Aufrufe von value) einbauen

   import qualified Control.Monad.Trans.State as S
   import qualified Control.Monad.Trans.Class as T
   import Numeric.Natural
   
   type Domain = S.StateT Natural Action Val
   
   value :: Env Name Val -> Exp -> Domain
   ...
     Put e f -> with_addr (value env e) $ \ a ->
       with_value (value env f) $ \ v -> 
       T.lift (put a v) >>= \ _ ->
       return ValUnit
   
   test3 = print $ run state0 $ flip S.runStateT 0 $ value env0
      $ Let "a" (New $ LitInt 0) ...

6. WriterT [String] zur Protokollierung (Argumente und Resultat von value)

7. Lesen der Umgebung mit ReaderT Env. Änderung der Umgebung (in Let, App) durch welche Funktion?

Datentyp für Parser

• data Parser c a = 
       Parser ( [c] -> [ (a, [c]) ] )

  • über Eingabestrom von Zeichen (Token) $c$,

  • mit Resultattyp $a$,

  • nichtdeterministisch (List).

• Beispiel-Parser, aufrufen mit:

  parse :: Parser c a -> [c] -> [(a,[c])]
  parse (Parser f) w = f w

• alternative Definition:

  type Parser c a = StateT [c] [] a

Elementare Parser (I)

-- | das nächste Token
next :: Parser c c  
next = Parser $ \ toks -> case toks of
    [] -> []
    ( t : ts ) -> [ ( t, ts ) ]
-- | das Ende des Tokenstroms
eof :: Parser c ()
eof = Parser $ \ toks -> case toks of
    [] -> [ ( (), [] ) ]
    _  -> []
-- | niemals erfolgreich
reject :: Parser c a
reject = Parser $ \ toks -> []

Monadisches Verketten von Parsern

Definition:

instance Monad ( Parser c ) where
  return x = Parser $ \ s -> return ( x, s ) 
  p >>= g = Parser $ \ s -> do
    ( a, t ) <- parse p s
    parse (g a) t

beachte: das return/do gehört zur List-Monade

Anwendungsbeispiel:

p :: Parser c (c,c)
p = do x <- next ; y <- next ; return (x,y)

mit Operatoren aus Control.Applicative:

p = (,) <$> next <*> next 

Elementare Parser (II)

satisfy :: ( c -> Bool ) -> Parser c c
satisfy p = do 
    x <- next 
    if p x then return x else reject

expect :: Eq c => c -> Parser c c
expect c = satisfy ( == c )

ziffer :: Parser Char Integer
ziffer = ( \ c ->  fromIntegral 
           $ fromEnum c - fromEnum '0' )
  <$> satisfy Data.Char.isDigit

Kombinatoren für Parser (I)

• Folge (and then) (ist >>= aus der Monade)

• Auswahl (oder) (ist Methode aus class Alternative)

  ( <|> ) :: Parser c a -> Parser c a -> Parser c a
  Parser f <|> Parser g = Parser $ \ s -> f s ++ g s

• Wiederholung (beliebig viele, wenigstens einer)

  many, some :: Parser c a -> Parser c [a]
  many p = some p <|> return [] 
  some p = (:) <$> p <*> many p

zahl :: Parser Char Integer = 
  foldl (\ a z -> 10*a+z) 0 <$> some ziffer

Kombinatoren für Parser (II)

(aus Control.Applicative)

• der zweite Parser hängt nicht vom ersten ab:

  (<*>) :: Parser c (a -> b) 
        -> Parser c a -> Parser c b

• eines der Resultate wird exportiert, anderes ignoriert

  (<*) :: Parser a -> Parser b -> Parser a
  (*>) :: Parser a -> Parser b -> Parser b

  Eselsbrücke: Ziel des Pfeiles wird benutzt

• der erste Parser ändert den Zustand nicht (fmap)

  (<$>) :: (a -> b) -> Parser a -> Parser b

Kombinator-Parser und Grammatiken

• CFG-Grammatik mit Regeln $S\to aSbS,S\to ϵ$ entspricht

  s :: Parser Char ()
  s =  (expect 'a' *> s *> expect 'b' *> s )
    <|> return ()

  Anwendung: parse (s <* eof) "abab"

• CFG: Variable $=$ Parser, nur <*> und <|> benutzen

• höherer Ausdrucksstärke (Chomsky-Stufe 1, 0) durch

  • Argumente ($\approx$ unendlich viele Variablen)

  • Monad (bind) statt Applicative (abhängige Fortsetzung)

Parser für Operator-Ausdrücke

• chainl1 :: Parser c a -> Parser c (a -> a -> a)
         -> Parser c a
  chainl1 p op = (foldl ...) 
    <$> p <*> many ((,) <$> op <*> p)

• expression :: [[Parser c (a -> a -> a)]]
    -> Parser c a -> Parser c a
  expression opss atom = 
    foldl ( \ p ops -> chainl1 ... ) atom opss

• exp = expression 
    [ [ string "*" *> return Times ]
    , [ string "+" *> return Plus  ] ]
    ( Exp.Const <$> zahl )

Robuste Parser-Bibliotheken

• Designfragen:

  • Nichtdeterminismus einschränken

  • Backtracking einschränken

  • Fehlermeldungen (Quelltextposition)

• klassisches Beispiel: Parsec (Autor: Daan Leijen) http://hackage.haskell.org/package/parsec

• Ideen verwendet in vielen anderen Bibliotheken, z.B. http://hackage.haskell.org/package/attoparsec (benutzt z.B. in http://hackage.haskell.org/package/aeson)

Asymmetrische Komposition

gemeinsam:

(<|>) :: Parser c a -> Parser c a 
      -> Parser c a
Parser p <|> Parser q = Parser $ \ s -> ...

• symmetrisch: p s ++ q s

• asymmetrisch: if null p s then q s else p s

Anwendung: many liefert nur maximal mögliche Wiederholung (nicht auch alle kürzeren)

Nichtdeterminismus einschränken

• Nichtdeterminismus $=$ Berechnungsbaum $=$ Backtracking

• asymmetrisches p <|> q : probiere erst p, dann q

• häufiger Fall: p lehnt sofort ab

Festlegung (in Parsec): wenn p wenigstens ein Zeichen verbraucht, dann wird q nicht benutzt (d. h. p muß erfolgreich sein)

Backtracking dann nur durch try p <|> q

Fehlermeldungen

• Fehler $=$ Position im Eingabestrom, bei der es nicht weitergeht

• und auch durch Backtracking keine Fortsetzung gefunden wird

• Fehlermeldung enthält:

  • Position

  • Inhalt (Zeichen) der Position

  • Menge der Zeichen mit Fortsetzung

Applicative, aber nicht Monad (Beispiele)

• Roman Cheplyaka, 2015 https://hackage.haskell.org/package/regex-applicative

  data RE s a = ...
  instance Applicative (RE s) where ...
  --  | Attempt to match a string of symbols
  -- against the regular expression:
  match :: RE s a -> [s] -> Maybe a
  match re = let obj = compile re in \str ->
      listToMaybe $ results $ foldl (flip step) obj str

  Erläuterung (geraten): regulärer Ausdruck wird in endlichen nicht-det. Automaten übersetzt (compile re),

  unabhängig von der Eingabe (str) — deswegen keine Monad-Instanz,

  Rechnung des dazu äquivalenten det. Automaten wird simuliert (für diese eine Eingabe, ohne den gesamten Potenzmengenautomaten auszurechnen), vgl. https://www.imn.htwk-leipzig.de/~waldmann/edu/ss23/afs/folien/#(61)

• Paolo Capriotti, Huw Campbell, 2012– https://hackage.haskell.org/package/optparse-applicative

  Anwendungs-Beispiel: https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/src/Matchbox/Config.hs#L118

Übung Kombinator-Parser

1. Bezeichner parsen (alphabetisches Zeichen, dann Folge von alphanumerischen Zeichen),

   Hinweis: fmap fromString $ (:) <$> _ <*> many _

2. Whitespace ignorieren (verwende Data.Char.isSpace)

   Hinweis: jeder Token-Parser t (Bsp: Bezeichner, Zahl-Literal) wird abgeschlossen durch t <* space (warum nicht space *> t?)

3. konkrete Haskell-ähnliche Syntax realisieren

   • if .. then .. else ..

   • let { .. = .. } in ..

   • Abstraktion (\ x -> ..) einstellig

   • Applikation (f a b c) mehrstellig

     Hinweis:

     exp  = foldl App <$> atom <*> many atom
     atom = Const <$> number <|> _ <|> parens exp

   • Abstraktion (\ x y z -> ..) mehrstellig (im Parser übersetzen in geschachtelte einstellige)

4. Implementierung chainl1, expression ergänzen, Operator-Parser vervollständigen für Ausdrücke mit Multiplikation, Addition, Vergleichen

   Hinweis: Operatoren sollen schwächer binden als Applikation (Bsp: f a + b bedeutet (f a) + b), realisieren durch

   exp = expression _ app
   app = foldl App <$> atom ... -- wie oben
   atom = ... <|> parens exp      -- wie oben

5. den Typ des Parsers ändern

   type Parser c = StateT [c] []    -- vorher
   type Parser c = StateT [c] Maybe -- nachher

   und Auswirkung diskutieren.

6. Fehlermeldungen mit

   type Parser c = StateT [c] (Except String)
   
   char c = satisfy (== c)
     <|> throwError ("expected: " <> [c])

7. den Eigenbau-Parser Parser Char durch Text.Parsec.String.Parser ersetzen https://hackage.haskell.org/package/parsec/

   Operator-Ausdrücke dann mit Text.Parsec.Expr

Motivation

• Node "foo" (Node "baz" Leaf Leaf) (Node "foobaz" Leaf Leaf)

  much easier to read if it is presented as

  Node "foo" (Node "baz" Leaf Leaf)
             (Node "foobaz" Leaf Leaf)

  A pretty-printer’s job is to lay out structured data appropriately (John Hughes 1995)

• inappropriate wäre deriving Show,

  denn Ausgabe ist dort immer einzeilig

• Anwendung: Code-Ausgabe in Kompilation,

  (Mensch soll es lesen, hat es aber nicht geschrieben)

Spezifikation

• data Doc abstrakter Dokumententyp für Textblöcke

• Konstruktor: text :: String -> Doc

• Kombinatoren:

  vcat       :: [ Doc ] -> Doc -- vertikal
  hcat, hsep :: [ Doc ] -> Doc -- horizontal

• Ausgabe: render :: Doc -> String (oder Text)

• der wesentliche Punkt ist

  cat       :: [ Doc ] -> Doc

  vertikal oder horizontal je nach verfügbarem Platz

• nachvollziehbare Spezifikation, effiziente Implement.

Implementierung von Hughes, Peyton Jones

• John Hughes: The Design of a Pretty-printing Library in Advanced Functional Programming, 1995 Johan Jeuring and Erik Meijer (eds), LNCS 925

  https://www.cse.chalmers.se/~rjmh/Papers/pretty.html

• verwendet in GHC (Glasgow Haskell Compiler) von Anfang an

  Übung: wirklich? https://downloads.haskell.org/~ghc/0.29/

  und GHC heute?

• alleinstehende Implementierung

  https://hackage.haskell.org/package/pretty

Implementierung von Wadler und Leijen

• Phil Wadler: A Prettier Printer, 1997

  https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf

• Implementierung (Daan Leijen 2000)

  https://hackage.haskell.org/package/wl-pprint

• modern (David Luposchainksi)

  https://hackage.haskell.org/package/prettyprinter

  dort auch Vergleich verschiedener Prettyprinter

  vgl. https://xkcd.com/927/ Standards

Klasse, Generierung, Präzedenzen

• class Pretty a where pretty :: a -> Doc

• (z.B. in autotool) automatische Code-Erzeugung für instance Pretty T für algebraische Datentypen

  https://git.imn.htwk-leipzig.de/waldmann/autotool/-/blob/master/todoc/src/Autolib/ToDoc/Class.hs?ref_type=heads

• Klammern weglassen (in Operator-Ausdrücken) durch Berücksichtigung von Präzedenzen

  class Pretty a where pretty_prec :: Int -> a -> Doc

Bidirektionale Programme

Motivation: parse und (pretty-)print aus einem gemeinsamen Quelltext

Tillmann Rendel and Klaus Ostermann: Invertible Syntax Descriptions, Haskell Symposium 2010

http://lambda-the-ultimate.org/node/4191

Datentyp

data PP a = PP
  { parse :: String -> [(a,String)]
  , print :: a -> Maybe String
  }

Spezifikation, elementare Objekte, Kombinatoren?

Definition

(alles nach: Turbak/Gifford Ch. 17.9)

CPS-Transformation (continuation passing style):

• original: Funktion gibt Wert v zurück

  f = \ x y -> let { ... } in v

• cps: Funktion erhält zusätzliches Argument, das ist eine Fortsetzung (continuation), die den Wert verarbeitet:

  f_cps = \ x y k -> let { ... } in k v