Algoritmické typování
IB015 Neimperativní programování
Kolektiv cvičících IB015
Fakulta informatiky, Masarykova univerzita
podzim 2018
IB015: Algoritmické typování podzim 2018 1 / 5
Typování funkcí: teorie
Intuitivní typování
výraz posoudíme z hlediska toho, co dělá, a na základě toho
určíme typ
vhodné pro jednoduché výrazy
Algoritmické typování
exaktní určení typu typovacím algoritmem
zdlouhavější, ale funguje pro všechny výrazy
IB015: Algoritmické typování podzim 2018 2 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head?
Jaký typ má map?
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map?
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
map :: (b → c) → [b] → [c]
head :: ([a] → a)
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Rovnosti:
map :: (b → c) → [b] → [c]
head :: ([a] → a)
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Rovnosti: b = [a]
map :: (b → c) → [b] → [c]
head :: ([a] → a)
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Rovnosti: b = [a] , c = a
map :: (b → c) → [b] → [c]
head :: ([a] → a)
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Rovnosti: b = [a] , c = a
map :: (b → c) → [b] → [c]
map :: ([a] → a) → [[a]] → [a]
head :: ([a] → a)
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head?
Jaký typ má head? [a] -> a
Jaký typ má map? (b -> c) -> [b] -> [c]
Rovnosti: b = [a] , c = a
map :: (b → c) → [b] → [c]
map :: ([a] → a) → [[a]] → [a]
head :: ([a] → a)
map head :: [[a]] → [a]
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd?
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)?
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
(.) :: (e→f) → (d→e) → d → f
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti:
(.) :: (e→f) → (d→e) → d → f
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti: e = [[a]], f = [a]
(.) :: (e→f) → (d→e) → d → f
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti: e = [[a]], f = [a] , d = (b,c), e = c
(.) :: (e→f) → (d→e) → d → f
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti: e = [[a]], f = [a] , d = (b,c), e = c
(.) :: (e→f) → (d→e) → d → f
(.) :: ([[a]]→[a]) → ((b, [[a]])→[[a]]) → (b,[[a]]) → [a]
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti: e = [[a]], f = [a] , d = (b,c), e = c
(.) :: (e→f) → (d→e) → d → f
(.) :: ([[a]]→[a]) → ((b, [[a]])→[[a]]) → (b,[[a]]) → [a]
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
snd :: ((b, [[a]])→[[a]])
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad I
Jaký typ má výraz map head . snd?
Jaký typ má map head? [[a]] -> a
Jaký typ má snd? (b, c) -> c
Jaký typ má (.)? (e -> f) -> (d -> e) -> d -> f
Rovnosti: e = [[a]], f = [a] , d = (b,c), e = c
(.) :: (e→f) → (d→e) → d → f
(.) :: ([[a]]→[a]) → ((b, [[a]])→[[a]]) → (b,[[a]]) → [a]
map head :: ([[a]]→[a])
snd :: ((b,c)→c)
snd :: ((b, [[a]])→[[a]])
result :: (b,[[a]]) → [a]
IB015: Algoritmické typování podzim 2018 3 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4?
Jaký typ má (>)?
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)?
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)? (Ord b) => b -> b -> Bool
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)? (Ord b) => b -> b -> Bool
(>) :: (Ord b) => b -> b -> Bool
4 :: (Num a) => a
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)? (Ord b) => b -> b -> Bool
Rovnosti: b = a
(>) :: (Ord b) => b -> b -> Bool
4 :: (Num a) => a
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)? (Ord b) => b -> b -> Bool
Rovnosti: b = a
(>) :: (Ord b) => b -> b -> Bool
(>) :: (Ord a) => a -> a -> Bool
4 :: (Num a) => a
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)?
Jaký typ má 4? (Num a) => a
Jaký typ má (>)? (Ord b) => b -> b -> Bool
Rovnosti: b = a
(>) :: (Ord b) => b -> b -> Bool
(>) :: (Ord a) => a -> a -> Bool
4 :: (Num a) => a
(4>) :: (Ord a, Num a) => a -> Bool
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum?
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)?
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
(.) :: (d→e) → (c→d) → c → e
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Rovnosti: d = a, e = Bool
(.) :: (d→e) → (c→d) → c → e
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Rovnosti: d = a, e = Bool , c = [b], d = b
(.) :: (d→e) → (c→d) → c → e
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Rovnosti: d = a, e = Bool , c = [b], d = b
(.) :: (d→e) → (c→d) → c → e
(.) :: (Ord a, Num a) => (a→Bool) → ([a]→a) → [a] → Bool
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Rovnosti: d = a, e = Bool , c = [b], d = b
(.) :: (d→e) → (c→d) → c → e
(.) :: (Ord a, Num a) => (a→Bool) → ([a]→a) → [a] → Bool
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
maximum :: (Ord a, Num a) => ([a]→a)
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
Jaký typ má (4>)? (Ord a, Num a) => a -> Bool
Jaký typ má maximum? (Ord b) => [b] -> b
Jaký typ má (.)? (d -> e) -> (c -> d) -> c -> e
Rovnosti: d = a, e = Bool , c = [b], d = b
(.) :: (d→e) → (c→d) → c → e
(.) :: (Ord a, Num a) => (a→Bool) → ([a]→a) → [a] → Bool
(4>) :: (Ord a, Num a) => (a→Bool)
maximum :: (Ord b) => ([b]→b)
maximum :: (Ord a, Num a) => ([a]→a)
result :: (Ord a, Num a) => [a] → Bool
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter?
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter? (b -> Bool) -> [b] -> [b]
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter? (b -> Bool) -> [b] -> [b]
filter :: (b -> Bool) -> [b] -> [b]
(4>).maximum :: (Ord a, Num a) => ([a] -> Bool)
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter? (b -> Bool) -> [b] -> [b]
Rovnosti: b = [a]
filter :: (b -> Bool) -> [b] -> [b]
(4>).maximum :: (Ord a, Num a) => ([a] -> Bool)
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter? (b -> Bool) -> [b] -> [b]
Rovnosti: b = [a]
filter :: (b -> Bool) -> [b] -> [b]
filter :: (Ord a, Num a) => ([a] -> Bool) -> [[a]] -> [[a]]
(4>).maximum :: (Ord a, Num a) => ([a] -> Bool)
IB015: Algoritmické typování podzim 2018 4 / 5
Algoritmické typování: příklad II
Jaký typ má výraz filter ((4 >) . maximum)?
Jaký typ má (4>) . maximum?
(Ord a, Num a) => [a] -> Bool
Jaký typ má filter? (b -> Bool) -> [b] -> [b]
Rovnosti: b = [a]
filter :: (b -> Bool) -> [b] -> [b]
filter :: (Ord a, Num a) => ([a] -> Bool) -> [[a]] -> [[a]]
(4>).maximum :: (Ord a, Num a) => ([a] -> Bool)
result :: (Ord a, Num a) => [[a]] -> [[a]]
IB015: Algoritmické typování podzim 2018 4 / 5
Typování funkcí – lambda-abstrakce
Jaký typ má funkce: (\x y -> takeWhile y ('a': x)) ?
IB015: Algoritmické typování podzim 2018 5 / 5
Typování funkcí – lambda-abstrakce
Jaký typ má funkce: (\x y -> takeWhile y ('a': x)) ?
Vidíme, že funkce bere 2 argumenty (x a y) a vrací jednu
hodnotu. Takže zatím máme typ: a -> b -> c.
IB015: Algoritmické typování podzim 2018 5 / 5
Typování funkcí – lambda-abstrakce
Jaký typ má funkce: (\x y -> takeWhile y ('a': x)) ?
Vidíme, že funkce bere 2 argumenty (x a y) a vrací jednu
hodnotu. Takže zatím máme typ: a -> b -> c.
V těle lambda-abstrakce je x použito ve výrazu ('a': x),
z toho vyplývá, že x musí být typu [Char]. Dostáváme
[Char] -> b -> c.
IB015: Algoritmické typování podzim 2018 5 / 5
Typování funkcí – lambda-abstrakce
Jaký typ má funkce: (\x y -> takeWhile y ('a': x)) ?
Vidíme, že funkce bere 2 argumenty (x a y) a vrací jednu
hodnotu. Takže zatím máme typ: a -> b -> c.
V těle lambda-abstrakce je x použito ve výrazu ('a': x),
z toho vyplývá, že x musí být typu [Char]. Dostáváme
[Char] -> b -> c.
Parametr y je použit jako první argument funkce
takeWhile :: (a -> Bool) -> [a] -> [a]. Protože už
víme, že x je typu [Char] a to je zároveň typ druhého
argumentu takeWhile, vidíme, že typ y je Char -> Bool.
Dostáváme [Char] -> (Char -> Bool) -> c.
IB015: Algoritmické typování podzim 2018 5 / 5
Typování funkcí – lambda-abstrakce
Jaký typ má funkce: (\x y -> takeWhile y ('a': x)) ?
Vidíme, že funkce bere 2 argumenty (x a y) a vrací jednu
hodnotu. Takže zatím máme typ: a -> b -> c.
V těle lambda-abstrakce je x použito ve výrazu ('a': x),
z toho vyplývá, že x musí být typu [Char]. Dostáváme
[Char] -> b -> c.
Parametr y je použit jako první argument funkce
takeWhile :: (a -> Bool) -> [a] -> [a]. Protože už
víme, že x je typu [Char] a to je zároveň typ druhého
argumentu takeWhile, vidíme, že typ y je Char -> Bool.
Dostáváme [Char] -> (Char -> Bool) -> c.
Návratová hodnota funkce je stejná jako funkce takeWhile,
čili [a]. Po naší specializaci je výsledkem
(\x y -> takeWhile y ('a': x)) :: [Char] ->
(Char -> Bool) -> [Char]
IB015: Algoritmické typování podzim 2018 5 / 5