Vyhodnocovací strategie (lenost vs. striktnost)
IB016 Seminář z funkcionálního programování
Fakulta informatiky, Masarykova univerzita
IB016: Cvičení 04 jaro 2023 1 / 26
Líné vyhodnocování: příklad
fst (1, undefined) ∗ 1
druhá složka dvojice se vůbec nevyhodnotí
IB016: Cvičení 04 jaro 2023 2 / 26
Líné vyhodnocování: příklad
fst (1, undefined) ∗ 1
druhá složka dvojice se vůbec nevyhodnotí
let fact n = product [1..n]
in map fact [1000000, 999999 .. 0] !! 999995 ∗ 120
jednotlivé prvky jsou vypočítány, jen když jsou vyžádány
(počítá se jen faktoriál pětky)
IB016: Cvičení 04 jaro 2023 2 / 26
Líné vyhodnocování: příklad
fst (1, undefined) ∗ 1
druhá složka dvojice se vůbec nevyhodnotí
let fact n = product [1..n]
in map fact [1000000, 999999 .. 0] !! 999995 ∗ 120
jednotlivé prvky jsou vypočítány, jen když jsou vyžádány
(počítá se jen faktoriál pětky)
let fibs = 0:1:zipWith (+) fibs (tail fibs)
in fibs !! 100 ∗ 354224848179261915075
seznam je konstruován líně, tedy jen prvky, které jsou potřeba
už jednou vypočítané prvky seznamu se nepočítají znovu
IB016: Cvičení 04 jaro 2023 2 / 26
Líné vyhodnocování
každá hodnota v Haskellu může být
a) vyhodnocená
b) nevyhodnocená – tzv. thunk – výraz, který lze vyhodnotit
pokud se snažíme nevypočítanou hodnotu přečíst, vypočítá se
při příštím čtení je již vypočítaná
vyhodnocuje se vždy jen to, co je nezbytně nutné
– jen ty části výrazů, jejichž výsledek je potřeba
– jen do té hloubky, dokud je to nutné
(vzpomeňte na take na nekonečných seznamech)
IB016: Cvičení 04 jaro 2023 3 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
(map fact [1..]) !! (1 - 1)
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
(map fact [1..]) !! (1 - 1)
(map fact (1:[2..])) !! (1 - 1)
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
(map fact [1..]) !! (1 - 1)
(map fact (1:[2..])) !! (1 - 1)
(fact 1 : map fact [2..]) !! (1 - 1)
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
(map fact [1..]) !! (1 - 1)
(map fact (1:[2..])) !! (1 - 1)
(fact 1 : map fact [2..]) !! (1 - 1)
(fact 1 : map fact [2..]) !! 0
IB016: Cvičení 04 jaro 2023 4 / 26
Líné vyhodnocování
fact n = product [1..n]
facts = map fact [0..]
[] !! _ = error "(!!): index too large"
(x:_) !! 0 = x
(_:xs) !! n = xs !! (n - 1)
facts !! 1
(map fact [0..]) !! 1
(map fact (0:[1..])) !! 1
(fact 0 : map fact [1..]) !! 1
(map fact [1..]) !! (1 - 1)
(map fact (1:[2..])) !! (1 - 1)
(fact 1 : map fact [2..]) !! (1 - 1)
(fact 1 : map fact [2..]) !! 0
fact 1 product [1..1] ∗ 1
IB016: Cvičení 04 jaro 2023 4 / 26
Striktnost a lenost
selectsort :: Ord a => [a] -> [a]
selectsort [] = []
selectsort xs = min : selectsort (withoutMin xs)
where
min = minimum xs
withoutMin (y:ys)
| y == min = ys
| otherwise = y : withoutMin ys
IB016: Cvičení 04 jaro 2023 5 / 26
Striktnost a lenost
selectsort :: Ord a => [a] -> [a]
selectsort [] = []
selectsort xs = min : selectsort (withoutMin xs)
where
min = minimum xs
withoutMin (y:ys)
| y == min = ys
| otherwise = y : withoutMin ys
striktní vzhledem ke struktuře seznamu (vyžaduje vyhodnotit seznam až po [])
vyhodnotí všechny prvky až do té míry jak vyžaduje (<)
ale produkuje výstup líně!
IB016: Cvičení 04 jaro 2023 5 / 26
Striktnost a lenost
selectsort :: Ord a => [a] -> [a]
selectsort [] = []
selectsort xs = min : selectsort (withoutMin xs)
where
min = minimum xs
withoutMin (y:ys)
| y == min = ys
| otherwise = y : withoutMin ys
striktní vzhledem ke struktuře seznamu (vyžaduje vyhodnotit seznam až po [])
vyhodnotí všechny prvky až do té míry jak vyžaduje (<)
ale produkuje výstup líně!
– jaká je složitost head (selectsort [10000,9999..0])?
IB016: Cvičení 04 jaro 2023 5 / 26
Striktnost a lenost
selectsort :: Ord a => [a] -> [a]
selectsort [] = []
selectsort xs = min : selectsort (withoutMin xs)
where
min = minimum xs
withoutMin (y:ys)
| y == min = ys
| otherwise = y : withoutMin ys
striktní vzhledem ke struktuře seznamu (vyžaduje vyhodnotit seznam až po [])
vyhodnotí všechny prvky až do té míry jak vyžaduje (<)
ale produkuje výstup líně!
– jaká je složitost head (selectsort [10000,9999..0])?
– O(n)
IB016: Cvičení 04 jaro 2023 5 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2)
*
+ +
1 2 1 2
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
*
3 +
1 2
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3
*
3 3
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
square a = a * a
square (1 + 2)
square
+
1 2
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
square a = a * a
square (1 + 2) (1 + 2) * (1 + 2)
*
+a =
1 2
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
square a = a * a
square (1 + 2) (1 + 2) * (1 + 2)
3 * 3
*
3a =
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
square a = a * a
square (1 + 2) (1 + 2) * (1 + 2)
3 * 3 9
9
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení podvýrazů
(1 + 2) * (1 + 2) 3 * (1 + 2)
3 * 3 9
9
square a = a * a
square (1 + 2) (1 + 2) * (1 + 2)
3 * 3 9
9
= grafová redukce (graph reduction)
IB016: Cvičení 04 jaro 2023 6 / 26
Sdílení v GHCi
GHCi vypisuje hodnoty pomocí print, což obvykle způsobuje plné vyhodnocení
pomocí :sprint lze vypsat bez vynucení vyhodnocení
pozor, polymorfní výrazy se vyhodnocují vždy znovu
IB016: Cvičení 04 jaro 2023 7 / 26
Sdílení v GHCi
GHCi vypisuje hodnoty pomocí print, což obvykle způsobuje plné vyhodnocení
pomocí :sprint lze vypsat bez vynucení vyhodnocení
pozor, polymorfní výrazy se vyhodnocují vždy znovu
> f a = [a, 1, 2] ++ [3, a, 4]
> xs = f (5 + 2 :: Int)
> :sprint xs
xs = _ -- xs je thunk (nevyhodnocený výraz)
> head xs
7
> :sprint xs
xs = 7 : _ -- ocásek xs se zatím nevyhodnotil
> length xs
6
> :sprint xs
xs = [7, _, _, _, 7, _]
IB016: Cvičení 04 jaro 2023 7 / 26
Teoretická vsuvka: vyhodnocovací strategie
Striktní vyhodnocovací strategie
výrazy vyhodnoceny při přiřazení do proměnných
argumenty vyhodnoceny před voláním
pořadí vyhodnocování obvykle do značné míry jasné ze zdrojového kódu
typické pro imperativní jazyky, ale i mnohé funkcionální (*ML)
head (take (2 + 2) [1..10])
∗ head (take 4 [1, 2, 3, 4, 5, 6, 7, 8, 9, 10])
∗ head [1, 2, 3, 4]
∗ 1
IB016: Cvičení 04 jaro 2023 8 / 26
Teoretická vsuvka: vyhodnocovací strategie
Normální/nestriktní vyhodnocovací strategie
výrazy se vyhodnocují, až když jsou potřeba
umožňuje existenci potenciálně nekonečných datových struktur
pořadí vyhodnocení méně viditelné
může mít větší spotřebu paměti (nevyhodnocené výrazy)
head (take (2 + 2) [1..10])
∗ head (take 4 (1 : [2..10]))
∗ head (1 : take 3 [2..10])
∗ 1
IB016: Cvičení 04 jaro 2023 9 / 26
Teoretická vsuvka: vyhodnocovací strategie
Normální/nestriktní vyhodnocovací strategie
výrazy se vyhodnocují, až když jsou potřeba
umožňuje existenci potenciálně nekonečných datových struktur
pořadí vyhodnocení méně viditelné
může mít větší spotřebu paměti (nevyhodnocené výrazy)
head (take (2 + 2) [1..10])
∗ head (take 4 (1 : [2..10]))
∗ head (1 : take 3 [2..10])
∗ 1
Líná vyhodnocovací strategie
normální + sdílení podvýrazů
IB016: Cvičení 04 jaro 2023 9 / 26
Teoretická vsuvka: vyhodnocovací strategie
Churchova–Rosserova věta
Výsledná hodnota ukončeného výpočtu výrazu nezáleží na redukční strategii: pokud
výpočet skončí, je jeho výsledek vždy stejný.
Věta o normalizaci
Jestliže pro nějaký výraz M existuje redukční strategie, s jejímž použitím se úprava
výrazu M nezacyklí, pak se tento výpočet nezacyklí ani s použitím normální (či líné)
redukční strategie.
IB016: Cvičení 04 jaro 2023 10 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
IB016: Cvičení 04 jaro 2023 11 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
výraz je produktivní, pokud
– ho lze plně vyhodnotit v konečném čase, nebo
– se po konečném počtu kroků vyhodnotí na hodnotový konstruktor aplikovaný na
produktivní podvýrazy
funkce je produktivní, jestliže každý výraz, který vznikne její aplikací na
produktivní výrazy, je produktivní
IB016: Cvičení 04 jaro 2023 11 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
výraz je produktivní, pokud
– ho lze plně vyhodnotit v konečném čase, nebo
– se po konečném počtu kroků vyhodnotí na hodnotový konstruktor aplikovaný na
produktivní podvýrazy
funkce je produktivní, jestliže každý výraz, který vznikne její aplikací na
produktivní výrazy, je produktivní
– inf 42
IB016: Cvičení 04 jaro 2023 11 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
výraz je produktivní, pokud
– ho lze plně vyhodnotit v konečném čase, nebo
– se po konečném počtu kroků vyhodnotí na hodnotový konstruktor aplikovaný na
produktivní podvýrazy
funkce je produktivní, jestliže každý výraz, který vznikne její aplikací na
produktivní výrazy, je produktivní
– inf 42 není produktivní
– repeat 42
IB016: Cvičení 04 jaro 2023 11 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
výraz je produktivní, pokud
– ho lze plně vyhodnotit v konečném čase, nebo
– se po konečném počtu kroků vyhodnotí na hodnotový konstruktor aplikovaný na
produktivní podvýrazy
funkce je produktivní, jestliže každý výraz, který vznikne její aplikací na
produktivní výrazy, je produktivní
– inf 42 není produktivní
– repeat 42 je produktivní
– [1..10] ++ inf 42
IB016: Cvičení 04 jaro 2023 11 / 26
Teoretická vsuvka: produktivní algoritmy
u algoritmů, které vracejí konečné datové struktury, nás zajímá, zda skončí
pokud ale produkují nekonečné datové struktury, tak jistě neskončí
neskončení ale může být různé:
– repeat x = x : repeat x
– inf x = inf x
výraz je produktivní, pokud
– ho lze plně vyhodnotit v konečném čase, nebo
– se po konečném počtu kroků vyhodnotí na hodnotový konstruktor aplikovaný na
produktivní podvýrazy
funkce je produktivní, jestliže každý výraz, který vznikne její aplikací na
produktivní výrazy, je produktivní
– inf 42 není produktivní
– repeat 42 je produktivní
– [1..10] ++ inf 42 není produktivní
IB016: Cvičení 04 jaro 2023 11 / 26
Vzory, ovlivňování lenosti
IB016: Cvičení 04 jaro 2023 12 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
f2 (undefined:undefined) ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
f2 (undefined:undefined) ∗ ()
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
f2 (undefined:undefined) ∗ ()
f3 (undefined:undefined) ∗
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
f2 (undefined:undefined) ∗ ()
f3 (undefined:undefined) ∗ *** Exception: ...
IB016: Cvičení 04 jaro 2023 13 / 26
Vzory vynucují vyhodnocení
f1, f2, f3 :: [a] -> ()
f1 _ = ()
f2 (_:_) = ()
f3 (_:_:[]) = ()
f1 undefined ∗ ()
f2 undefined ∗ *** Exception: Prelude.undefined
f1 [] ∗ ()
f2 [] ∗ *** Exception: ...
f2 [undefined,undefined] ∗ ()
f3 [undefined,undefined] ∗ ()
f2 (undefined:undefined) ∗ ()
f3 (undefined:undefined) ∗ *** Exception: ...
Argument se vyhodnocuje jen do hloubky nutné k rozhodnutí, zda hodnota
odpovídá vzoru.
IB016: Cvičení 04 jaro 2023 13 / 26
Líné vzory
Vlnovkou před vzorem lze odložit pattern matching až do doby, kdy se nějaký
argument navázaný vzorem použije.
Takový vzor nevynucuje vyhodnocení a vždy uspěje.
Srovnejte:
strict, lazy :: Bool -> Maybe Int -> Int
strict b (Just x) = if b then x else 0
lazy b ~(Just x) = if b then x else 0
IB016: Cvičení 04 jaro 2023 14 / 26
Líné vzory
Vlnovkou před vzorem lze odložit pattern matching až do doby, kdy se nějaký
argument navázaný vzorem použije.
Takový vzor nevynucuje vyhodnocení a vždy uspěje.
Srovnejte:
strict, lazy :: Bool -> Maybe Int -> Int
strict b (Just x) = if b then x else 0
lazy b ~(Just x) = if b then x else 0
strict False Nothing ∗ ???
lazy False Nothing ∗ ???
lazy True Nothing ∗ ???
IB016: Cvičení 04 jaro 2023 14 / 26
Líné vzory
f ~(x, y) = g x y se přeloží na (něco jako) f p = g (fst p) (snd p)
v do-notaci potlačuje navíc požadavek na MonadFail:
~(x:xs) <- listOf1 arbitrary
(fragment generátoru pro QuickCheck, listOf1 generuje neprázdné seznamy)
IB016: Cvičení 04 jaro 2023 15 / 26
seq vynucuje vyhodnocení
Funkce seq :: a -> b -> b
a `seq` b zaručuje, že a bude vyhodnoceno, a vrátí b
k vyhodnocení dojde až když něco vynutí výpočet výrazu a `seq` b
nevyhodnocuje a plně, nýbrž jen po nejvyšší konstruktor:
(undefined, undefined) `seq` 1 ∗ 1
undefined `seq` 1 ∗ *** Exception: ...
IB016: Cvičení 04 jaro 2023 16 / 26
seq vynucuje vyhodnocení
Funkce seq :: a -> b -> b
a `seq` b zaručuje, že a bude vyhodnoceno, a vrátí b
k vyhodnocení dojde až když něco vynutí výpočet výrazu a `seq` b
nevyhodnocuje a plně, nýbrž jen po nejvyšší konstruktor:
(undefined, undefined) `seq` 1 ∗ 1
undefined `seq` 1 ∗ *** Exception: ...
Striktní aplikace ($!) :: (a -> b) -> a -> b
obdoba ($), ale vynutí vyhodnocení argumentu před aplikací
f1 $! undefined ∗ *** Exception: ...
IB016: Cvičení 04 jaro 2023 16 / 26
⋆ Weak head normal form
seq vynucuje vyhodnocení pouze do tzv. weak head normal form:
po nejvyšší (i část. aplik.) hodnotový konstruktor, nebo
dokud výraz není λ-abstrakce, nebo
dokud výraz není nedostatečně aplikovanou vestavěnou funkcí.
Příklady výrazů a jejich WHNF:
replicate 3 'A' (:) 'A' (replicate (3-1) 'A')
replicate 3 \x -> x : replicate (3-1) x
head \(x:xs) -> x
(\x -> if x then Right else Left) (4 < 3) Left
Just (replicate 3 'A') už je ve WHNF
(+) (4 * 5) už je ve WHNF (uvažujeme-li vestavěné plus)
IB016: Cvičení 04 jaro 2023 17 / 26
Proč striktnost?
striktní výpočet může být rychlejší, paměťově efektivnější
> :set +s
(0.18 secs, 74075592 bytes)
> const () $! product [1..100000]
()
(18.32 secs, 9052106864 bytes)
> :m + Data.List
> const () $! foldl' (*) 1 [1..100000]
()
(2.73 secs, 9045968328 bytes)
foldl' je striktní verze foldl
IB016: Cvičení 04 jaro 2023 18 / 26
Proč striktnost?
readFiles :: [FilePath] -> IO [String]
readFiles paths = mapM readFile paths
readFile vrací obsah souboru líně
soubor je zavřen, až když je dočten na konec!
lehce můžeme překročit limit na množství otevřených souborů
seq nepomůže
IB016: Cvičení 04 jaro 2023 19 / 26
Control.DeepSeq
Úplné/hluboké vyhodnocení.
import Control.DeepSeq
readFiles :: [FilePath] -> IO [String]
readFiles paths = forM paths $ \p ->
withFile p ReadMode $ \h -> do
c <- hGetContents h
return $!! c
($!!) :: NFData a => (a -> b) -> a -> b
plně vyhodnotí argument, pak aplikuje funkci
deepseq :: NFData a => a -> b -> b
class NFData a where
rnf :: a -> ()
plně vyhodnotí argument
IB016: Cvičení 04 jaro 2023 20 / 26
Control.DeepSeq
import Control.DeepSeq
data BinTree a = Empty
| Node a (BinTree a) (BinTree a)
deriving (Show, Eq)
instance NFData a => NFData (BinTree a) where
rnf Empty = ()
rnf (Node v t1 t2) = rnf v `seq` rnf t1 `seq` rnf t2
IB016: Cvičení 04 jaro 2023 21 / 26
Rozšíření BangPatterns
{-# LANGUAGE BangPatterns #-}
Umožňuje snadno vynutit striktnost u vzoru, výrazu let, argumentu hodnotového
konstruktoru.
data Tuple a b = Tuple !a !b
lazy, strict :: a -> ()
lazy _ = ()
strict !_ = ()
taková hodnota je pak před aplikací funkce/konstruktoru vyhodnocena do WHNF
(po první konstruktor)
v let způsobí vyhodnocení příslušného výrazu před započetím vyhodnocování
části in (striktní let)
($!) :: (a -> b) -> a -> b
($!) f x = let !ex = x in f ex
IB016: Cvičení 04 jaro 2023 22 / 26
Rozšíření StrictData a Strict
{-# LANGUAGE StrictData #-}
jako by všechna pole v datových definicích v daném modulu byla definována
pomocí ! (z rozšíření BangPatterns)
lenost může být vynucena vlnovkou (data T = D ~Int)
IB016: Cvičení 04 jaro 2023 23 / 26
Rozšíření StrictData a Strict
{-# LANGUAGE StrictData #-}
jako by všechna pole v datových definicích v daném modulu byla definována
pomocí ! (z rozšíření BangPatterns)
lenost může být vynucena vlnovkou (data T = D ~Int)
{-# LANGUAGE Strict #-}
obsahuje StrictData
argumenty funkcí, definice where/let, vazby v case/do jsou také striktní
vnořené vzory a top-level definice nadále striktní nejsou
IB016: Cvičení 04 jaro 2023 23 / 26
Rozšíření StrictData a Strict
{-# LANGUAGE StrictData #-}
jako by všechna pole v datových definicích v daném modulu byla definována
pomocí ! (z rozšíření BangPatterns)
lenost může být vynucena vlnovkou (data T = D ~Int)
{-# LANGUAGE Strict #-}
obsahuje StrictData
argumenty funkcí, definice where/let, vazby v case/do jsou také striktní
vnořené vzory a top-level definice nadále striktní nejsou
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_
exts.html#extension-StrictData
IB016: Cvičení 04 jaro 2023 23 / 26
Striktnost v knihovně
Data.List: foldl', foldl1' – akumulátorem je jediná, vždy vyhodnocená
hodnota namísto potenciálně obrovského thunku (nevyhodnoceného výrazu).
Data.Map.Lazy – klíče se vyhodnocují striktně (ukládají se už vyhodnocené pro
rychlejší vyhledávání).
Data.Map.Strict – klíče i hodnoty se ukládají vyhodnocené.
⋆ Pokročilé věci související s transformátory monád a ST.
IB016: Cvičení 04 jaro 2023 24 / 26
Lenost v jiných jazycích
zkrácené vyhonocování logických výrazů ve většině jazyků (včetně vedlejších
efektů!)
IB016: Cvičení 04 jaro 2023 25 / 26
Lenost v jiných jazycích
zkrácené vyhonocování logických výrazů ve většině jazyků (včetně vedlejších
efektů!)
iterátory se mohou chovat líně (map/filter/. . . v Pythonu, C++ ranges, C#
LINQ, . . . )
IB016: Cvičení 04 jaro 2023 25 / 26
Lenost v jiných jazycích
zkrácené vyhonocování logických výrazů ve většině jazyků (včetně vedlejších
efektů!)
iterátory se mohou chovat líně (map/filter/. . . v Pythonu, C++ ranges, C#
LINQ, . . . )
future/promise – často mohou běžet paralelně, či podle potřeby (líně)
IB016: Cvičení 04 jaro 2023 25 / 26
Procvičení
Naprogramujte variantu ohodnocených binárních stromů se striktními hodnotami
(StrictValTree), ale línou reprezentací stromové struktury, a variantu, která je plně
striktní jak ve struktuře tak v hodnotách (StrictTree).
rozmyslete si, pro jaké použití by se mohly jednotlivé varianty hodit a kdy byste
naopak použili línou variantu
rozmyslete si, jaké prostředky z tohoto cvičení chcete použít pro vynucení
striktnosti v jednotlivých případech a proč
pro obě verze stromů implementujte instanci Functor
IB016: Cvičení 04 jaro 2023 26 / 26