Einleitung

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

Inferenzsystem: (aussagenlog.) Resolution

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

Aufgaben Inferenz

  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

  3. warum ist aussagenlog. Resolution nicht vollständig? (es gilt nicht: \((M\models F)\Rightarrow(M\vdash F)\).) Ein einfaches Gegenbeispiel reicht.

  4. ein Paper aus POPL heraussuchen, das Inferenzsysteme verwendet zur Beschreibung von statischer oder dynamische Semantik einer Programmiersprache

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

Visualisierung und Sonifizierung

Fixpunktberechnung im Interpreter

Direkte Realisierung von Tupeln

Simultane Rekursion: letrec

letrec nach rec

Übung Lambda-Kalkül (I)

Übung Lambda-Kalkül (II)

folgende Aufgaben aus H. Barendregt: Lambda Calculus

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 (Motivation, Kategorien)

…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

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?

Monaden (Definition, Beispiele)

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

Typ-Rekonstruktion

Motivation

Realisierung mit Constraints

Inferenz für Aussagen der Form \(E \vdash X : (T, C)\)

wobei

Bsp: \(U=\{u,v,w\}, C=\{(u,\textsf{Int}\to v),(w\to \textsf{Bool}, u)\0\}\),

\(\sigma=\{(u,\textsf{Int}\to\textsf{Bool}),(v,\textsf{Bool}),(w,\textsf{Int})\}\)

Inferenzregeln f. Rekonstruktion (Plan)

Plan:

Für (fast) jeden Teilausdruck eine eigene (frische) Typvariable ansetzen, Beziehungen zwischen Typen durch Constraints ausdrücken.

Inferenzregeln? Lösbarkeit? Implementierung? — Testfall:

\ f g x y -> 
   if (f x y) then (x+1) else (g (f x True))

Inferenzregeln f. Rekonstrukion

Implementierung Constraint-Erzeugung

Substitutionen (Definition)

Substitutionen: Produkt

Produkt von Substitutionen: \(t (\sigma_1 \circ \sigma_2) = (t \sigma_1) \sigma_2\)

Beispiel 1:

\(\sigma_1=\{X\mapsto Y\}, \sigma_2 = \{Y\mapsto a\}, \sigma_1 \circ \sigma_2 = \{ X\mapsto a, Y\mapsto a\}\).

Beispiel 2 (nachrechnen!):

\(\sigma_1 = \{X\mapsto Y\}, \sigma_2=\{Y \mapsto X\}, \sigma_1\circ\sigma_2 = \sigma_2\)

Eigenschaften:

Implementierung:

import Data.Map 
type Substitution = Map Identifier Term
times :: Substitution -> Substitution -> Substition

Substitutionen: Ordnung

Substitution \(\sigma_1\) ist allgemeiner als Substitution \(\sigma_2\):

\(\sigma_1 \raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}\sigma_2 \iff \exists \tau : \sigma_1 \circ \tau = \sigma_2\)

Beispiele:

Eigenschaften

Unifikation—Definition

Unifikationsproblem

(allgemeinst: infimum bzgl. \(\raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}\))

Satz: jedes Unifikationsproblem ist

lösbar.

Unifikation—Algorithmus

Unifikation—Komplexität

Bemerkungen:

Bsp: Signatur \(\{f/2, a/0\}\),

unifiziere \(f(X_1,f(X_2,f(X_3,f(X_4,a))))\) mit \(f(f(X_2,X_2),f(f(X_3,X_3),f(f(X_4,X_4),f(a,a))))\)

Hausaufgaben

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