Organisatorisches (Ü KW 15)

Beispiel: C-Compiler

Inhalt der Vorlesung

Konzepte von Programmiersprachen

realisieren durch

Hilfsmittel:

Einleitung: Sprachverarbeitung

Literatur

Anwendungen von Techniken des Compilerbaus

Organisation der Vorlesung

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?

Datentypen für Folgen (von Zeichen)

Verstecken von Implementierungsdetails

Verwendung standardisierter Namen

Einsparung von Konstruktor-Aufrufen

Übung (Haskell)

Übung (Interpreter)

Übung (effiziente Imp. von Bezeichnern)

Inferenz-Systeme

Motivation

Definition

ein Inferenz-System \(I\) besteht aus

eine Ableitung für \(F\) bzgl. \(I\) ist ein Baum:

Def: \(I \vdash F\) \(:\iff\) \(\exists\) \(I\)-Ableitungsbaum mit Wurzel \(F\).

Regel-Schemata

Inferenz-Systeme (Beispiel)

Primalitäts-Zertifikate

Inferenz von Typen

Inferenz von Werten

Umgebungen (Spezifikation)

Umgebungen (Implementierung)

Umgebung ist (partielle) Funktion von Name nach Wert

Realisierungen: type Env = String -> Integer

Operationen:

Beispiel

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

entspricht \((\emptyset[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} \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

Continuations

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,

Unterprogramme

Beispiele

Interpreter mit Funktionen

Semantik (mit Funktionen)

Let und Lambda

Mehrstellige Funktionen

…simulieren durch einstellige:

Semantik mit Closures

Closures (Spezifikation)

Rekursion?

Testfall (2)

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

Repräsentation von Fehlern

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

Lambda-Kalkül (Wdhlg.)

Motivation

1. Modellierung von Funktionen:

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

Der Lambda-Kalkül

Lambda-Terme

Eigenschaften der Reduktion

Beziehung zur Semantik des Interpreters

Daten als Funktionen

Lambda-Kalkül als universelles Modell

Fixpunkt-Kombinatoren (Motivation)

Fixpunkt-Kombinatoren (Implementierung)

Lambda-Berechenbarkeit

Satz: (Church, Turing)

Kodierung von Zahlen nach Church

Übung Lambda-Kalkül (I)

Übung Lambda-Kalkül (II)

folgende Aufgaben aus H. Barendregt: Lambda Calculus

Fixpunkte

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 \(f x=x\).

Existenz? Eindeutigkeit? Konstruktion?

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

Ü (Wdhlg) Def. obere Schranke, Supremum

Beispiele f. Halbordnungen, CPOs

Halbordnung? pointed? complete?

Stetige Funktionen

\(f\) ist stetig \(:=\)

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

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

Beweis: …und dieser ist \(\sup [\bot,f(\bot),f^2(\bot),\ldots]\)

CPO auf Menge von Funktionen

Funktionen als CPO, Beispiel

Welche Funktionale sind stetig?

Fixpunkte und Laziness

Fixpunktberechnung im Interpreter

Arithmetik mit Bedarfsauswertung

Simultane Rekursion: letrec

letrec nach rec (falsch)

letrec nach rec (richtig)

Übung Fixpunkte

  1. Limes der Folge \(F^k(\bot)\) 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 \(\Sigma=\{a,b\}\), halbgeordnet durch \(\subseteq\). ist CPO? pointed?

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

    \(h: C\to C: L\mapsto \{a\}\cup L\cdot \{b\}\cdot (\Sigma^*\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.

Verpackung und Verteilung

Haskell-Software-Pakete

Kuratierte Paket-Mengen

Continuous Intergration

Haskell-Module

Modul-Abhängigkeiten

Zustand/Speicher

Motivation

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

Dazu muß semantischer Bereich geändert werden.

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

Speicher (Daten)

Speicher (Operationen)

Auswertung von Ausdrücken

Änderung der Hilfsfunktionen

Variablen?

in unserem Modell haben wir:

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

Imperative Programmierung

es fehlen noch wesentliche Operatoren:

diese kann man:

Rekursion

mehrere Möglichkeiten zur Realisierung

Rekursion (operational)

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

Monaden

…unter verschiedenen Aspekten

Die Konstruktorklasse Monad

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

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

Beispiele:

Kategorische Definitionen und Sätze

Beispiel: Isomorphie

weiteres Beispiel

Produkte

Dualität

Funktoren

Die Kleisli-Konstruktion

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

Monaden-Transformatoren

Der Zustands-Transformator

Der Ausnahme-Transformator MaybeT

Der Ausnahme-Transformator ExceptT

Bibliotheken für Monaden-Transformatoren

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 \(\operatorname{\text{id}}_1, \operatorname{\text{id}}_2\) gibt mit \(\forall f: \operatorname{\text{id}}_k\circ f = f = f \circ \operatorname{\text{id}}_k\), dann \(\operatorname{\text{id}}_1 = \operatorname{\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)\neq(y_1,y_2)=y\), mit \(g(x)=g(y)\).

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

      Aus \(g\circ\operatorname{\text{proj}}_i=f_i\) folgt \(x_i=f_i(x)=(g\circ \operatorname{\text{proj}}_i)(x)=\operatorname{\text{proj}}_i(g(x)) = \operatorname{\text{proj}}_i(g(y)) = (g\circ \operatorname{\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:\operatorname{\textsf{V}}(G)\to \operatorname{\textsf{V}}(H)\) ist Morphismus, falls \(\forall x,y: (x,y)\in \operatorname{\textsf{E}}(G) \iff (f(x),f(y))\in \operatorname{\textsf{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?

Kombinator-Parser

Datentyp für Parser

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)

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

Kombinatoren für Parser (II)

(aus Control.Applicative)

Kombinator-Parser und Grammatiken

Parser für Operator-Ausdrücke

Robuste Parser-Bibliotheken

Asymmetrische Komposition

gemeinsam:

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

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

Nichtdeterminismus einschränken

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

Applicative, aber nicht Monad (Beispiele)

Ü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

Pretty-Printing

Motivation

Spezifikation

Implementierung von Hughes, Peyton Jones

Implementierung von Wadler und Leijen

Klasse, Generierung, Präzedenzen

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?

Ablaufsteuerung/Continuations

Definition

(alles nach: Turbak/Gifford Ch. 17.9)

CPS-Transformation (continuation passing style):

aus g (f 3 2)

wird \ k -> f_cps 3 2 $ \ v -> g_cps v k

Motivation

Funktionsaufrufe in CPS-Programm kehren nie zurück, können also als Sprünge implementiert werden!

CPS als einheitlicher Mechanismus für

CPS für Linearisierung

(a + b) * (c + d) wird übersetzt (linearisiert) in

( \ top -> 
   plus a b $ \ x -> 
   plus c d $ \ y -> 
   mal  x y top
) ( \ z -> z )

plus x y k = k (x + y)
mal  x y k = k (x * y)

später tatsächlich als Programmtransformation (Kompilation)

CPS für Resultat-Tupel

wie modelliert man Funktion mit mehreren Rückgabewerten?

CPS/Tupel-Beispiel

erweiterter Euklidischer Algorithmus:

prop_egcd x y = 
    let (p,q) = egcd x y
    in  (p*x + q*y) == gcd x y

egcd :: Integer -> Integer 
     -> ( Integer, Integer )
egcd x y = if y == 0 then ???
           else let (d,m) = divMod x y
                    (p,q) = egcd y m
                in  ???

vervollständige, übersetze in CPS

CPS für Ablaufsteuerung

Wdhlg: CPS-Transformation von 1+(2*(3-(4+5))) ist

\ top -> plus 4 5 $ \ a ->
         minus 3 a $ \ b ->
         mal 2 b $ \ c ->
         plus 1 c top

Neu: label und jump

1 + label foo (2 * (3 - jump foo (4 + 5)))

Semantik: durch label wird die aktuelle Continuation benannt: foo = \ c -> plus 1 c top

und durch jump benutzt:

\ top -> plus 4 5 $ \ a -> foo a

Vergleiche: label: Exception-Handler deklarieren,
jump: Exception auslösen

Semantik für CPS

Semantik von Ausdruck x in Umgebung \(E\)

ist Funktion von Continuation nach Wert (Action)

value(E, label L B) = \ k -> 
  value (E[L:=k], B) k
value (E, jump L B) = \ k -> 
  value (E, L) $ \ k' ->
  value (E, B) k'

Beispiel 1:

value (E, label x x) 
  = \ k -> value (E[x:=k], x) k
  = \ k -> k k

Beispiel 2

value (E, jump (label x x) (label y y))
= \ k ->
  value (E, label x x) $ \ k' -> 
  value (E, label y y) k'
= \ k -> 
  ( \ k0 -> k0 k0 ) $ \ k' -> 
  value (E, label y y) k'
= \ k -> 
  ( \ k0 -> k0 k0 ) $ \ k' -> 
  ( \ k1 -> k1 k1 ) k'

Semantik

semantischer Bereich:

type Continuation a = a -> Action Val
newtype CPS a 
   = CPS ( Continuation a -> Action Val )
value :: Env -> Exp -> CPS Val

Plan:

CPS als Monade

Der CPS-Transformator

Übungsaufgaben

Rekursion (bzw. Schleifen) mittels Label/Jump

(und ohne Rec oder Fixpunkt-Kombinator)

folgende Beispiele sind aus Turbak/Gifford, DCPL, 9.4.2

Typen

Grundlagen

Typ \(=\) statische Semantik

(Information über mögliches Programm-Verhalten, erhalten ohne Programm-Ausführung)

formale Beschreibung:

Inferenzsystem für Typen (Syntax)

Inferenzsystem für Typen (Semantik)

hierbei (vorläufige) Design-Entscheidungen:

Inferenz für Let

(alles ganz analog zu Auswertung von Ausdrücken)

Applikation und Abstraktion

Beziehung zw. dyn. und stat. Semantik

Grenzen der einfachen Typisierung

Übung

  1. Typisierung für

    • Vergleichs-Operatoren für Zahlen

    • If-Then-Else,

    • New, Get, Put — Vorsicht: dann gibt es getypte, aber trotzdem nicht terminierende Programme.

  2. für Tupel mit abstrakter Syntax

    data Exp = ... | Tuple [Exp] | Nth Int Exp

    • dynamische Semantik,

    • statische Semantik (einschl. Prüfung des Index, deswegen nicht Nth Exp Exp)

    • konkrete Syntax (Parser)

  3. konkrete Syntax für AbsTyped

    (dazu Parser für Typ-Ausdrücke, dabei soll (->) rechts-assoziativ sein)

Polymorphe Typen

Motivation

ungetypt:

let { t = \ f x -> f (f x)
    ; s = \ x -> x + 1
    } in (t t s) 0

einfach getypt nur so möglich:

let { t2 = \ (f :: (Int -> Int) -> (Int -> Int)) 
             (x :: Int -> Int) -> f (f x)
    ; t1 = \ (f :: Int -> Int) (x :: Int) -> f (f x)
    ; s = \ (x :: Int) -> x + 1
    } in (t2 t1 s) 0

wie besser?

Typ-Argumente (Beispiel)

Typ-Argumente (Inferenz-Regeln)

Rekonstruktion polymorpher Typen

…ist im Allgemeinen nicht möglich:

Joe Wells: Typability and Type Checking in System F Are Equivalent and Undecidable, Annals of Pure and Applied Logic 98 (1998) 111–156,

übliche Einschränkung (ML, Haskell): Typ-Abstraktionen nur für let-gebundene Bezeichner:

Luis Damas, Roger Milner: Principal Type Schemes for Functional Programs 1982,

let { t = \ f x -> f(f x) ; s = \ x -> x+1 } 
in t t s 0

folgendes ist dann nicht typisierbar (t ist monomorph):

( \ t s -> t t s 0 ) 
  ( \ f x -> f (f x) ) (\ x -> x+1)

Diskussion: Variablen

Diskussion: Kinds (in Haskell)

Diskussion: Agda

Übung Polymorphie

Plan für Compiler

Transformationen/Ziel

Ziel: maschinen(nahes) Programm mit

CPS-Transformation

CPS-Transformation: Spezifikation

(als Schritt im Compiler)

CPS-Transformation: Zielsyntax

drei Teilmengen von data Exp:

Exp_CPS ==> App Identifier Exp_Value^*
    | If Exp_Value Exp_CPS Exp_CPS
    | Let Identifier Exp_Letable Exp_CPS
Exp_Value ==> Literal | Identifier 
Exp_Letable ==> Literal
    | Abs Identifier Exp_CPS
    | Exp_Value Op Exp_Value

Übung 1: Übersetze von Exp nach Exp_CPS:

(0 - (b * b)) + (4 * (a * c))

Übung 2: wegen CPS brauchen wir tatsächlich:

\ k -> k ((0 - (b * b)) + (4 * (a * c))

Beispiel

Lösung 1:

(0 - (b * b)) + (4 * (a * c))
==>
let { t.3 = b * b } in
  let { t.2 = 0 - t.3 } in
    let { t.5 = a * c } in
       let { t.4 = 4 * t.5 } in
         let { t.1 = t.2 + t.4 } in
            t.1

Lösung 2:

\ k -> let  ... in k t.1

CPS-Transf. f. Abstraktion, Applikation

vgl. Sect. 6 in: Gordon Plotkin: Call-by-name, call-by-value and the \(\lambda\)-calculus,

Th. Comp. Sci. 1(2) 1975, 125–159 http://dx.doi.org/10.1016/0304-3975(75)90017-1 , http://homepages.inf.ed.ac.uk/gdp/

dabei sind \(k,f,a\) frische Namen.

Bsp. \(\operatorname{CPS}(\lambda x.9)=\lambda k_2.k_2(\lambda x.\operatorname{CPS}(9)) =\lambda k_2.k_2(\lambda x k_1.k_1 9),\)

\(\operatorname{CPS}((\lambda x.9) 8) = \lambda k_4.(\lambda k_2.k_2(\lambda x k_1.k_1 9)) (\lambda f.((\lambda k_3.k_3 8) (\lambda a.f a k_4)))\)

Ü: Normalform von \(\operatorname{CPS}((\lambda x.9)8) (\lambda z.z)\)

Realisierung der CPS-Transformation

Namen

Anwendung der Namens-Erzeugung

Kompilation des If

Kompilation des Let

Umrechnung zw. Continuations (App)

Umrechnung zw. Continuations (Abs)

Vergleich CPS-Interpreter/Transformator

Wiederholung CPS-Interpreter:

type Cont = Val -> Action Val
eval :: Env -> Exp -> Cont -> Action Val
eval env x = \ k -> case x of
    ConstInt i -> ... 
    Plus a b -> ...

CPS-Transformator:

type Cont = ExpValue -> Fresh ExpCPS
cps :: Exp -> Cont -> Fresh ExpCPS
cps x = \ m -> case x of
    ConstInt i -> ... 
    Plus a b -> ...

Übung CPS-Transformation

Closure Conversion

Motivation

(Literatur: DCPL 17.10) — Beispiel:

let { linear = \ a -> \ x -> a * x + 1 
    ; f = linear 2 ; g = linear 3
    } 
in  f 4 * g 5

beachte nicht lokale Variablen: (\ x -> .. a .. )

Spezifikation

closure conversion:

geschlossen: alle Variablen sind lokal

Ansatz:

closure passing style

\ x -> a * x + 1
==>
\ clo x -> 
  let { a = nth 1 clo } in a * x + 1

Closure-Konstruktion?
Komplette Übersetzung des Beispiels?

Transformation

CLC[ \ i_1 .. i_n -> b ] =
   (tuple ( \ clo i_1 .. i_n ->
            let { v_1 = nth 1 clo ; .. }
            in  CLC[b] 
          ) v_1 .. )

wobei \(\{v_1,\ldots\}=\) freie Variablen in \((\lambda i_1 \ldots i_n \to b)\)

CLC[ (f a_1 .. a_n) ] =
  let { clo = CLC[f] 
      ; code = nth 0 clo 
  } in  code clo CLC[a_1] .. CLC[a_n]

Lifting

Spezifikation

(lambda) lifting:

Motivation: in Maschinencode gibt es nur globale Sprungziele

(CPS-Transformation: Unterprogramme kehren nie zurück \(\Rightarrow\) globale Sprünge)

Realisierung

nach closure conversion sind alle Abstraktionen geschlossen, diese müssen nur noch aufgesammelt und eindeutig benannt werden.

let { g1 = \ v1 .. vn -> b1
    ...
    ; gk = \ v1 .. vn -> bk
} in b

dann in b1, .., bk, b keine Abstraktionen gestattet

Lambda-Lifting (Plan)

um ein Programm zu erhalten, bei dem alle Abstraktionen global sind:

Lambda-Lifting (Realisierung)

Beispiel: \(\operatorname{\textsf{lift}}(\lambda x.\lambda y.y x) = \operatorname{\textsf{lift}}_x(\operatorname{\textsf{lift}}_y(y x)) = \operatorname{\textsf{lift}}_x(S I (K x)) = S (K( S I )) (S (K K) I)\)

Registervergabe

Motivation

Plan (I)

Plan (II)

Registerbenutzung

Compiler-Übungen

  1. Testen Sie die richtige Kompilation von

    let { d = \ f x -> f (f x) } 
in d d d d (\ x -> x+1) 0

  2. implementieren Sie fehlende Codegenerierung/Runtime für

    let { p = new 42 
    ; f = \ x -> if (x == 0) then 1 
                 else  (x * (get p) (x-1)) 
    ; foo = put p f 
    } in f 5

  3. ergänzen Sie das Programm, so daß \(5!\) ausgerechnet wird

    let { f = label x (x, 5, 1) } 
in  if ( 0 == nth 1 f ) 
    then nth 2 f  
    else jump ...
              (..., ..., ...)

    Kompilieren Sie das Programm. Dazu muß für label, jump, tuple, nth die CPS-Transformation implementiert werden.

  4. Bei der CPS-Transformation von If wird die Continuation \(k\) kopiert:

          If b' <$> cps j k <*> cps n k

    Geben Sie ein Beispiel dafür an, daß dadurch der Ausgabetext groß werden kann.

    Geben Sie eine andere Übersetzung für If an, bei der \(k\) nur einmal angewendet wird. (Benutzen Sie cont2exp.)

    Überprüfen Sie für das eben angegebene Beispiel.

  5. Alle Tests bis hier kompilieren konstante Ausdrücke. Diese könnte man auch sofort auswerten.

    Ändern Sie Compiler und Laufzeitsystem, so daß Funktionen kompiliert werden, die zur Laufzeit Argumente (Zahlen) von der Kommandozeile bekommen.

  6. Register Allocator in GCC: siehe https://gcc.gnu.org/onlinedocs/gccint/RTL-passes.html.

    Suchen Sie die entsprechende Beschreibung/Implementierung in clang (llvm).

    Vergleichen Sie an Beispielen die Anzahl der Register in dem von unserem Compiler erzeugten Code und dem daraus durch GCC (clang) erzeugten Assemblercode.

    Wo findet die Register-Allokation für Java-Programme statt?

und wer Zeit hat …

Automatische Speicherverwaltung

Motivation

Speicher-Allokation durch Konstruktion von

Modell: Speicherbelegung \(=\) gerichteter Graph

Knoten lebendig: von Register aus erreichbar.

sonst tot \(\Rightarrow\) automatisch freigeben

Gliederung:

Mark/Sweep

Plan: wenn Speicher voll, dann:

Problem: zum Markieren muß man den Graphen durchqueren, man hat aber keinen Platz (z. B. Stack), um das zu organisieren.

Lösung:

H. Schorr, W. Waite: An efficient machine-independent procedure for garbage collection in various list structures, Communations of the ACM, 10(8):481-492, August 1967.

temporäre Änderungen im Graphen selbst (pointer reversal)

Pointer Reversal (Invariante)

ursprünglicher Graph \(G_0\), aktueller Graph \(G\):

Knoten (cons) mit zwei Kindern (head, tail), markiert mit

globale Variablen \(p\) (parent), \(c\) (current).

Invariante: man erhält \(G_0\) aus \(G\), wenn man

Pointer Reversal (Ablauf)

Schritt (neue Werte immer mit \('\)): falls \(\operatorname{mark}(c)=\) …

Knoten werden in Tiefensuch-Reihenfolge betreten.

Eigenschaften Mark/Sweep

Ablegen von Markierungs-Bits:

Stop-and-copy (Plan)

Plan:

auch hier: Verwaltung ohne Zusatzspeicher (Stack)

C. J. Cheney: A nonrecursive list compacting algorithm, Communications of the ACM, 13(11):677–678, 1970.

Stop-and-copy (Invariante)

fromspace, tospace \(:\) array [ 0 …\(N\) ] of cell

Variablen: \(0 \le \text{scan} \le \text{free} \le N\)

einige Zellen im fromspace enthalten Weiterleitung (\(=\) Adresse im tospace)

Invarianten:

Stop-and-copy (Ablauf)

Schritt: while scan \(<\) free:

Besucht Knoten in Reihenfolge einer Breitensuche.

Stop-and-copy (Eigenschaften)

Speicher mit Generationen

Beobachtung: es gibt

Plan:

Lösung: benutze Generationen, bei GC in Generation \(k\): betrachte alle Zellen in Generationen \(>k\) als lebend.

Speicherverwaltung in JVM

Speicheraufteilung:

Ablauf

Speicherverwaltung in JVM (II)

Ausblick

Informative Typen

in \(X::T\), der deklarierte Typ \(T\) kann eine schärfere Aussage treffen als aus \(X\) (Implementierung) ableitbar.

data T a = C a -- C :: a -> T a
data T a where C :: Bool -> T Bool

das ist u.a. nützlich bei der Definition und Implementierung von (eingebetteten) domainspezifischen Sprachen

GADT

Higher Order Abstract Syntax

data Exp a  where
  Var :: a -> Exp a
  Abs :: (a -> Exp b) -> Exp (a -> b)
  App :: Exp (a -> b) -> Exp a -> Exp b

App (Abs $ \x -> Plus (C 1) (Var x)) (C 2) 

value :: Exp a -> a
value e = case e of
  App f a -> value f ( value a )

Ü: vervollständige Interpreter

Quelle: Frank Pfenning, Conal Elliott: HOAS, PLDI 1988 http://conal.net/papers/

Zusammenfassung

Methoden

Semantik

Monaden zur Programmstrukturierung

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

Anwendungen:

Testfragen (für jede Monad-Instanz):

Wozu braucht man den Compilerbau?

Prüfungsvorbereitung

Beispielklausur http://www.imn.htwk-leipzig.de/~waldmann/edu/ws11/cb/klausur/