1

Grundlagen der Programmierung 3 A

Typen, Typberechnung und Typcheck

Prof. Dr. Manfred Schmidt-Schauß

Sommersemester 2017

Haskell, Typen, und Typberechnung

Ziele:

• Haskells Typisierung

• Typisierungs-Regeln

• Typ-Berechnung

• Milners Typcheck (Robin Milner)

Grundlagen der Programmierung 2 (Typen-A) – 2/37 –

Einige andere Programmiersprachen

ab Java 5: generische Typen verwandt mit polymorphenTypen

ML (und CAML, OCAML) hat parametrisch polymorphesTypsystem

JavaScript Nachteile: Es fehlt eine statische Typisierung

TypeScript (Microsoft): Neue JavaScript Variante mitstatischer Typisierung und Typinferenz.

Google Ankundigung: Angular 2 (JavaScript-Webframework)zukunftig auf Basis von TypeScript

Grundlagen der Programmierung 2 (Typen-A) – 3/37 –

Typisierung in Haskell

Haskell hat eine starke, statische Typisierung.mit parametrisch polymorphen Typen.

• jeder Ausdruck muss einen Typ haben

• Der Typchecker berechnet Typen aller Ausdruckeund pruft Typen zur Compilezeit

• Es gibt keine Typfehler zur Laufzeitd.h. kein dynamischer Typcheck notig.

Grundlagen der Programmierung 2 (Typen-A) – 4/37 –

Uberladung und Konversion in Haskell

Haskell: keine Typkonversion

Es gibt Uberladung:z.B. arithmetische Operatoren: +,−.∗, /

Zahlkonstanten fur ganze Zahlen sind uberladen

Typcheck erstmal ohne Uberladungohne Kindsund ohne Typen hoherer Ordnung

Grundlagen der Programmierung 2 (Typen-A) – 5/37 –

Uberladung und Konversion in Haskell

Haskell: keine Typkonversion

Es gibt Uberladung:z.B. arithmetische Operatoren: +,−.∗, /

Zahlkonstanten fur ganze Zahlen sind uberladen

Typcheck erstmal ohne Uberladungohne Kindsund ohne Typen hoherer Ordnung

Grundlagen der Programmierung 2 (Typen-A) – 5/37 –

Typisierung, Begriffe

polymorph: Ein Ausdruck kann viele Typen haben(vielgestaltig, polymorph).

parametrischpolymorph:

Die (i.a. unendliche) Menge der Typenentspricht einem schematischen Typausdruck

Beispiel length

Schema: [a]->Int

Instanzen: [Int]->Int, [Char]->Int, [[Char]]->Intusw.

Grundlagen der Programmierung 2 (Typen-A) – 6/37 –

Syntax von Typen in Haskell (ohne Typklassen)

〈Typ〉 ::= 〈Basistyp〉 | (〈Typ〉) | 〈Typvariable〉

| 〈Typkonstruktorn〉{〈Typ〉}n

(n = Stelligkeit)

〈Basistyp〉 ::= Int | Integer | Float | Rational | Char | . . .

Grundlagen der Programmierung 2 (Typen-A) – 7/37 –

Syntax von Typen

Typkonstruktoren konnen benutzerdefiniert sein (z.B. Baum a)

Vordefinierte Liste [·]Typkonstruktoren: Tupel (.,...,.)

Funktionen · → · (Stelligkeit 2, Infix)

Konvention zu Funktionstypen mit →a→ b→ c→ d bedeutet: a→ (b→ (c→ d)).

Grundlagen der Programmierung 2 (Typen-A) – 8/37 –

Interpretation der Typen

length :: [a] -> Int

Interpretation: Fur alle Typen typ ist length eine Funktion,die vom Typ [typ]→ Int ist.

Grundlagen der Programmierung 2 (Typen-A) – 9/37 –

Komposition

Beispiel: Komposition von Funktionen:

komp::(a -> b) -> (c -> a) -> c -> b

komp f g x = f (g x)

In Haskell ist komp vordefiniert und wird als”.“ geschrieben:

Beispielaufruf:

*Main> suche_nullstelle (sin . quadrat) 1 4 0.00000001

←↩1.772453852929175

(sin . quadrat) entspricht sin(x2)und quadrat . sin entspricht (sin(x))2.

Grundlagen der Programmierung 2 (Typen-A) – 10/37 –

Typ der Komposition

Erklarung zum Typ von komp, wobei {a,b,c} Typvariablen sind.Ausdruck: f ‘komp‘ g bzw. f . g

(a->b) -> (c->a) -> c->b Typ von (.)

(τ1 -> τ2) Typ von f(τ3 -> τ1) Typ von g

τ3 Typ des Arguments xder Komposition f . g

τ2 Typ des Resultatsder Komposition f(g x)

(τ3 -> τ2) Typ von (f . g)

x :: τ3g // τ1

f // τ2

Grundlagen der Programmierung 2 (Typen-A) – 11/37 –

Typ der Komposition

Erklarung zum Typ von komp, wobei {a,b,c} Typvariablen sind.Ausdruck: f ‘komp‘ g bzw. f . g

(a->b) -> (c->a) -> c->b Typ von (.)

(τ1 -> τ2) Typ von f(τ3 -> τ1) Typ von g

τ3 Typ des Arguments xder Komposition f . g

τ2 Typ des Resultatsder Komposition f(g x)

(τ3 -> τ2) Typ von (f . g)

x :: τ3g // τ1

f // τ2

Grundlagen der Programmierung 2 (Typen-A) – 11/37 –

Typ der Komposition

Erklarung zum Typ von komp, wobei {a,b,c} Typvariablen sind.Ausdruck: f ‘komp‘ g bzw. f . g

(a->b) -> (c->a) -> c->b Typ von (.)

(τ1 -> τ2) Typ von f(τ3 -> τ1) Typ von g

τ3 Typ des Arguments xder Komposition f . g

τ2 Typ des Resultatsder Komposition f(g x)

(τ3 -> τ2) Typ von (f . g)

x :: τ3g // τ1

f // τ2

Grundlagen der Programmierung 2 (Typen-A) – 11/37 –

Typen von Konstruktoren

Typen von Konstruktoren werden durch deren data-Definitionautomatisch festgelegt!

data Baum a b = Empty | Blatt b

| Knoten a (Baum a b) Baum a b)

Typen der Konstruktoren:Empty :: Baum a bBlatt :: b→ Baum a bKnoten :: b→ Baum a b→ Baum a b→ Baum a b

Grundlagen der Programmierung 2 (Typen-A) – 12/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: ?

Beispiele:

quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ

, t :: σ

(s t) :: ?

Beispiele:

quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: ?

Beispiele:

quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:

quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:

quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: ?

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int

, 2 :: Int

(quadrat 2) :: ?

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: ?

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ?

, 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int)

, 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: ? , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: (Int→ Int) , 2:: Int

((1 +) 2) :: ?

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregeln

Wie berechnet man Typen von Ausdrucken?

Anwendung von Funktionsausdruck auf Argument

s :: σ → τ , t :: σ

(s t) :: τ

Beispiele:quadrat :: Int→ Int , 2 :: Int

(quadrat 2) :: Int

+ :: Int→ (Int→ Int) , 1 :: Int

(1 +) :: (Int→ Int) , 2:: Int

((1 +) 2) :: Int

Grundlagen der Programmierung 2 (Typen-A) – 13/37 –

Typregel”Anwendung“: mehrere Argumente

s :: σ1 → σ2 . . .→ σn → τ , t1 :: σ1 , . . . , tn :: σn(s t1 . . . tn) :: τ

Beispiele

+ :: Int→ Int→ Int, 1 :: Int , 2 :: Int

(+ 1 2) :: Int

+ :: Int→ Int→ Int

(1 + 2) :: Int

Grundlagen der Programmierung 2 (Typen-A) – 14/37 –

Beispiel

even::Int -> Bool a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b)) c.= Int; b

.= Bool

quadrat::Int -> Int c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool

a -> b.= Int -> Bool

(.)::(a -> b) -> (c -> a) -> c -> b

c.= Int; b

.= Bool

quadrat::Int -> Int

c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool

a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b))

c.= Int; b

.= Bool

quadrat::Int -> Int

c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b))

c.= Int; b

.= Bool

quadrat::Int -> Int

c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b))

c.= Int; b

.= Bool

quadrat::Int -> Int c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b)) c.= Int; b

.= Bool

quadrat::Int -> Int c -> a.= Int -> Int

even . quadrat :: ???

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Beispiel

even::Int -> Bool a -> b.= Int -> Bool

(.)::(a -> b) -> ((c -> a) -> (c -> b)) c.= Int; b

.= Bool

quadrat::Int -> Int c -> a.= Int -> Int

even . quadrat :: Int -> Bool

Grundlagen der Programmierung 2 (Typen-A) – 15/37 –

Anwendungsregel fur polymorphe Typen

Ziel: Anwendung der Typregel fur z.B. length oder map

Neuer Begriff: γ ist eine Typsubstitutionwenn sie Typen fur Typvariablen einsetztγ(τ) nennt man Instanz von τ

BeispielTypsubstitution: γ = {a 7→ Char, b 7→ Float}Instanz: γ([a]→ Int) = [Char]→ Int

Grundlagen der Programmierung 2 (Typen-A) – 16/37 –

Anwendungsregel fur polymorphe Typen

s :: σ → τ, t :: ρ und γ(σ) = γ(ρ)

(s t) :: γ(τ)

Berechnet den Typ von (s t)wenn die Typen von s, t schon bekannt sind

Hierbei ist zu beachten:Damit alle Freiheiten erhalten bleiben:

die Typvariablen in ρ mussen vorher umbenannt werden,so dass σ und ρ keine gemeinsamen Typvariablen haben.

Grundlagen der Programmierung 2 (Typen-A) – 17/37 –

Beispiel zur polymorphen Anwendungsregel

Typ von (map quadrat) ?

map :: (a→ b) → ([a]→ [b])quadrat :: Int → Int

Instanziiere mit: γ = {a 7→ Int, b 7→ Int}ergibt: map :: (Int→ Int)→ ([Int]→ [Int])

Regelanwendung ergibt:

map :: (Int→ Int)→ ([Int]→ [Int]), quadrat :: (Int→ Int)

(map quadrat) :: [Int]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 18/37 –

Beispiel zur polymorphen Anwendungsregel

Typ von (map quadrat) ?

map :: (a→ b) → ([a]→ [b])quadrat :: Int → Int

Instanziiere mit: γ = {a 7→ Int, b 7→ Int}

ergibt: map :: (Int→ Int)→ ([Int]→ [Int])

Regelanwendung ergibt:

map :: (Int→ Int)→ ([Int]→ [Int]), quadrat :: (Int→ Int)

(map quadrat) :: [Int]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 18/37 –

Beispiel zur polymorphen Anwendungsregel

Typ von (map quadrat) ?

map :: (a→ b) → ([a]→ [b])quadrat :: Int → Int

Instanziiere mit: γ = {a 7→ Int, b 7→ Int}ergibt: map :: (Int→ Int)→ ([Int]→ [Int])

Regelanwendung ergibt:

map :: (Int→ Int)→ ([Int]→ [Int]), quadrat :: (Int→ Int)

(map quadrat) :: [Int]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 18/37 –

Beispiel zur polymorphen Anwendungsregel

Typ von (map quadrat) ?

map :: (a→ b) → ([a]→ [b])quadrat :: Int → Int

Instanziiere mit: γ = {a 7→ Int, b 7→ Int}ergibt: map :: (Int→ Int)→ ([Int]→ [Int])

Regelanwendung ergibt:

map :: (Int→ Int)→ ([Int]→ [Int]), quadrat :: (Int→ Int)

(map quadrat) :: [Int]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 18/37 –

Polymorphe Regel fur n Argumente

s :: σ1 → σ2 . . .→ σn → τ, t1 :: ρ1, . . . , tn :: ρn und ∀i : γ(σi) = γ(ρi)

(s t1 . . . tn) :: γ(τ)

Die Typvariablen in ρ1, . . . , ρn mussen vorher umbenannt werden.

Beachte: verwende moglichst allgemeines γ(kann berechnet werden; s.u.)

Grundlagen der Programmierung 2 (Typen-A) – 19/37 –

Wie berechnet man die Typsubstitutionen?

Unifikation: Berechnung der allgemeinsten Typsubstitutionim Typberechnungsprogramm bzw Typchecker

Unifikation wird benutzt im Typchecker von Haskell!

Grundlagen der Programmierung 2 (Typen-A) – 20/37 –

polymorphe Typen; Unifikation

s :: σ → τ , t :: ρ und γ ist allgemeinster Unifikator von σ.= ρ

(s t) :: γ(τ)

(die Typvariablen in ρ mussen vorher umbenannt werden.)

Grundlagen der Programmierung 2 (Typen-A) – 21/37 –

Unifikation: Regelbasierter Algorithmus

Man braucht 4 Regeln, die auf (E;G) operieren:

E: Menge von Typgleichungen,G: Losung; mit Komponenten der Form x 7→ t.

Beachte: x, y ist Typvariablesi, ti, s, t sind Typen,f, g sind Typkonstruktoren

Grundlagen der Programmierung 2 (Typen-A) – 22/37 –

Unifikation: Die Regeln

Start mit G = ∅;E: zu losende Gleichung(en)

• G; {x .= x} ∪ EG;E

• G; {t .= x} ∪ EG; {x .

= t} ∪ EWenn t keine Variable ist

• G; {x .= t} ∪ E

G[t/x] ∪ {x 7→ t};E[t/x]Wenn x nicht in t vorkommt

• G; {(f s1 . . . sn).= (f t1 . . . tn)} ∪ E

G; {s1.= t1, . . . , sn

.= tn)} ∪ E

Ersetzung: E[t/x]: alle Vorkommen von x werden durch t ersetztEffekt: G[t/x]: jedes y 7→ s wird durch y 7→ s[t/x] ersetzt

Grundlagen der Programmierung 2 (Typen-A) – 23/37 –

Unifikation: Regelbasierter Algorithmus

Fehlerabbruch, wenn:

• x.= t in E, x 6= t und x kommt in t vor. (Occurs-Check)

• (f(. . .).= g(. . .) kommt in E vor und f 6= g. (Clash)

Fehlerabbruch bedeutet: nicht typisierbar

Grundlagen der Programmierung 2 (Typen-A) – 24/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) →

(

[a]→ [b]

)

id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}

{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}

{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅

{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Beispiel mit Typvariablen

Berechne Typ von (map id)

map:: (a→ b) → ([a]→ [b])id:: a′ → a′

Gesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= (a′ → a′):

G E

∅; {(a→ b).= (a′ → a′)}

∅; {a .= a′, b

.= a′}

{a 7→ a′}; {b .= a′}{a 7→ a′, b 7→ a′}; ∅{a 7→ a′, b 7→ a′};

Einsetzen der Losung γ = {a 7→ a′, b 7→ a′}in [a]→ [b] ergibt:

(map id) :: ([a′]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 25/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) →

(

[a]→ [b]

)

head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}

{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}

{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅

{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Noch ein Beispiel

Berechne Typ von (map head)

map:: (a→ b) → ([a]→ [b])head:: [a]→ aGesuchter Typ: γ([a]→ [b])

Regelanwendung benotigt Losung γ von (a→ b).= ([a′]→ a′):

G E

∅; {(a→ b).= ([a′]→ a′)}

∅; {a .= [a′], b

.= a′}

{a 7→ [a′]}; {b .= a′}{a 7→ [a′], b 7→ a′}; ∅{a 7→ [a′], b 7→ a′};

Einsetzen der Losung γ = {a 7→ [a′], b 7→ a′}in [a]→ [b] ergibt:

(map head) :: ([[a′]]→ [a′]).

Grundlagen der Programmierung 2 (Typen-A) – 26/37 –

Beispiel (foldr (:) []) :: ??

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

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

umbenannt: c -> [c] -> [c]

([]) :: [a]

umbenannt: [d]

G E

∅

{a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}

{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel (foldr (:) []) :: ??

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ b.= c→ [c]→ [c], b

.= [d]}

{b 7→ [d]} {a→ [d]→ [d].= c→ [c]→ [c]}

{b 7→ [d]} {a .= c, [d]

.= [c], [d]

.= [c]}

{b 7→ [d], a 7→ c} {[d] .= [c], [d].= [c]}

{b 7→ [d], a 7→ c} {d .= c, [d]

.= [c]}

{b 7→ [c], a 7→ c, d 7→ c} {[c] .= [c]}{b 7→ [c], a 7→ c, d 7→ c} {c .= c}{b 7→ [c], a 7→ c, d 7→ c} {}

(foldr (:) [])::[c]→ [c] = γ([a]→ b)

Grundlagen der Programmierung 2 (Typen-A) – 27/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

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

umbenannt: c -> [c] -> [c]

([]) :: [a]

umbenannt: [d]

G E

∅

{a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .= [d]}

nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .= [d]}

nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}

nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel. Linksfaltung: (foldl (:) [])?

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

(:) :: a -> [a] -> [a] umbenannt: c -> [c] -> [c]

([]) :: [a] umbenannt: [d]

G E

∅ {a→ b→ a.= c→ [c]→ [c], a

.= [d]}

{a 7→ [d]} {[d]→ b→ [d].= c→ [c]→ [c]}

{a 7→ [d]} {[d] .= c, b.= [c], [d]

.= [c]}

{a 7→ [d], b 7→ [c]} {[d] .= c, [d].= [c]}

{a 7→ [d], b 7→ [c]} {c .= [d], [d].= [c]}

{a 7→ [d], b 7→ [[d]], c 7→ [d]} {[d] .= [[d]]}{a 7→ [d], b 7→ [[d]], c 7→ [d]} {d .

= [d]}nicht losbar, da d in [d] echt vorkommt

(foldl (:) []) ist nicht typisierbar!

Grundlagen der Programmierung 2 (Typen-A) – 28/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}

{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiel zu Typberechnung

Typ von map length

map :: (a→ b)→ ([a]→ [b]), length :: [a′]→ Int

(map length) :: ? = γ([a]→ [b])

Unifiziere (a→ b).= [a′]→ Int

G E

∅; {(a→ b).= ([a′]→ Int)}

∅; {a .= [a′], b

.= Int}

{a 7→ [a′]}; {b .= Int}{a 7→ [a′], b 7→ Int}; ∅

Somit: (map length) :: γ([a]→ [b]) = [[a′]]→ [Int]

Grundlagen der Programmierung 2 (Typen-A) – 29/37 –

Beispiele zu polymorpher Typberechnung

Berechne Typ der Liste [1]:

1 : Int (:) :: a→ [a]→ [a] [] :: [b]

1 : [] ::?

Anwendungsregel ergibt Gleichungen: {a .= Int, [a]

.= [b]}

Losung: γ = {a 7→ Int}

Typ (1 : []) :: [Int]

Grundlagen der Programmierung 2 (Typen-A) – 30/37 –

Beispiel zu Typfehler

[1, ’a’] hat keinen Typ:• 1 : ( ’a’ : [])• 1 :: Integer, [] :: [b], ’a’ :: Char (Typen der Konstanten.)• (1 :) :: [Integer]→ [Integer] und

(’a’:[]) :: [Char].

Kein Typ als Resultat, denn:[Integer]

.= [Char] ist nicht losbar.

Grundlagen der Programmierung 2 (Typen-A) – 31/37 –

Beispiel zu Typfehler im Interpreter

Prelude> [1,’a’] ←↩

<interactive>:1:1:

No instance for (Num Char)

arising from the literal ‘1’ at <interactive>:1:1

Possible fix: add an instance declaration for (Num Char)

In the expression: 1

In the expression: [1, ’a’]

In the definition of ‘it’: it = [1, ’a’]

Grundlagen der Programmierung 2 (Typen-A) – 32/37 –

Typ eines Ausdrucks

Typ von (map quadrat [1,2,3,4]) :• map:: (a→ b)→ [a]→ [b]

• quadrat:: Integer→ Integer, und [1, 2, 3, 4] :: [Integer].

• γ = {a 7→ Integer, b 7→ Integer}.

• Das ergibt: γ(a) = Integer, γ([a]) = [Integer], γ([b]) = [Integer].

• Resultat: γ([b]) = [Integer]

Grundlagen der Programmierung 2 (Typen-A) – 33/37 –

Typisierung von Funktionen und Ausdrucken

Kompexe Sprachkonstrukte: rekursiv definierte FunktionenLambda-Ausdrucke, let-AusdruckeListen-Komprehensionen.

Typcheckalgorithmus von Robin Milner (in Haskell und ML)• ist schnell, (i.a.)• liefert allgemeinste (Milner-)Typen• benutzt Unifikation (eine optimierte Variante)

• schlechte worst-case Komplexitat:in seltenen Fallen exponentieller Zeitbedarf

• Liefert in seltenen Fallen nichtdie allgemeinsten moglichen polymorphen Typen

Grundlagen der Programmierung 2 (Typen-A) – 34/37 –

Typisierung von Funktionen, Milner

Satz zur Milner-Typisierung in Haskell:

Sei t ein getypter Haskell-Ausdruck, ohne freie Variablen.Dann wird die Auswertung des Ausdrucks tnicht mit einem Typfehler abbrechen.

Allgemeine Aussage zu starken Typsystemen

Es gibt keine dynamischen Typfehler,wenn das Programm statisch korrekt getypt ist

Grundlagen der Programmierung 2 (Typen-A) – 35/37 –

Typisierung und Reduktion

Beachte: Nach Reduktionen kann ein Ausdruckmehr Typen (bzw. einen allgemeineren Typ) habenals vor der Reduktion

Beispiel:if 1 > 0 then [] else [1] :: [Integer]

arithmetische-Reduktion:−→ if True then [] else [1] :: [Integer]

Case-Reduktion:−→ [] :: [a]

Grundlagen der Programmierung 2 (Typen-A) – 36/37 –

Typisierung und Reduktion

Beachte: Nach Reduktionen kann ein Ausdruckmehr Typen (bzw. einen allgemeineren Typ) habenals vor der Reduktion

Beispiel:if 1 > 0 then [] else [1] :: [Integer]

arithmetische-Reduktion:−→ if True then [] else [1] :: [Integer]

Case-Reduktion:−→ [] :: [a]

Grundlagen der Programmierung 2 (Typen-A) – 36/37 –

Typisierung und Reduktion

weiteres Beispiel:

(if 1 > 0 then foldr else foldl) ::(a -> a -> a) -> a -> [a] -> a

Reduktion ergibt als Resultat:

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

der Typ ist allgemeiner geworden!

Grundlagen der Programmierung 2 (Typen-A) – 37/37 –

Typisierung und Reduktion

weiteres Beispiel:

(if 1 > 0 then foldr else foldl) ::(a -> a -> a) -> a -> [a] -> a

Reduktion ergibt als Resultat:

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

der Typ ist allgemeiner geworden!

Grundlagen der Programmierung 2 (Typen-A) – 37/37 –