12rap2.md

Wnioskowanie o programach 2

Poprzednio mówiliśmy o dowodzeniu prostych własności funkcji w Haskellu.

Dziś porozmawiamy o:

• bardziej zaawansowanych własnościach
• równości funkcji
• własności metod klasowych
• wykorzystaniu wnioskowania do konstrukcji programów ("konstruktywna indukcja")

Rozgrzewka

Przypomnijmy sobie funkcję map:

map f [] = []                          -- map1
map f (x:xs) = f x : map f xs          -- map2

W arytmetyce mamy własność rozdzielności, np. mnożenie jest rozdzielne względem dodawania:

a*(b+c) = a*b + a*c

Tu chcemy pokazać, że map jest rozdziekne względem składania funkcji:

map id xs = xs                         -- mapId
map (f . g) xs = (map f . map g) xs    -- mapComp

gdzie

id x = x                               -- id
(f . g) x = f(g x)                     -- comp

Wykażmy map id xs = xs przez indukcję po xs:

Krok podstawowy: map id [] ={map1}= []

Krok indukcyjny: (IH:: map id xs = xs) → map id (x:xs) = (x:xs)

map id (x:xs)   ={map2}=
id x:map id xs  ={id}=
x:map id xs     ={IH}=
x:xs

📝 Ćwiczenie: wykaż mapComp

Równość funkcji

Składanie funkcji tworzy monoid (półgrupę z jedynką)

f . id = id . f = f                    -- compId
(f . g) . h = (f . g) . h              -- compAssoc

Jak już wiemy, porównywanie funkcji jest kłopotliwe - funkcje nie są obserwowalne. Możemy natomiast (czasami) zaobserwować, jak funkcja zachowuje się dla konkretnych argumentów.

Dlatego, nie wnikając w subtelności filozoficzne przyjmiemy ekstensjonalną równość funkcji: dla f,g::a → b powiemy, że

f = g wtw gdy ∀ x::a.f x = g x

przy takiej definicji możemy łatwo wykazać compId

(f . id) x   ={comp}=
f(id x)      ={id}=
f x

podobnie można wykazać compAssoc (ćwiczenie).

Teraz własności map możemy zapisać jako

map id = id                            -- mapId
map (f . g) = (map f . map g)          -- mapComp

Patrząc na ostatnie równanie, zauważmy, że o ile lewa i prawa strona dają te same wartości, to mogą mieć inny koszt: LHS przechodzi listę raz, a RHS - dwa razy. Dlatego równość ta może być podstawą optymalizacji. GHC pozwala deklarować takie reguły, np.

{-# RULES
      "map/map"    forall f g xs.  map f (map g xs) = map (f.g) xs
#-}

Klasy, metody i własności

Klasy pozwalają nam na tworzenie funkcji generycznych, np.

elem :: Eq a => [a] -> [a]

czy

foo :: Functor f => (a->b) -> f a -> f b
foo f x = fmap f . fmap id 

dla podobnej funkcji na listach

bar :: (a->b) -> [a] -> [b]
bar f = map f . map id

dzięki wykazanym wcześniej własnościom map, wiemy, że bar = map. Ale co jeśli chcemy wykazać podobną własność foo?

Dlatego zwykle definiując klasę postulujemy spełnienie pewnych własności, np dla klasy Functor

fmap id = id                           -- fmapId
fmap (f . g) = (fmap f . fmap g)       -- fmapComp

dzięki nim możemy wykazać foo = fmap.

Ćwiczenie: wykaż odpowiednie własności dla

instance Functor Maybe where
  fmap f Nothing  = Nothing
  fmap f (Just x) = Just (f x)

data Tree a = Leaf a | Node (Tree a) (Tree a)

instance Functor Tree where
  fmap f (Leaf x) = Leaf (f x)
  fmap f (Node l r) = Node (fmap f l) (fmap f r)

Prawa dla Monad i Applicative

Każda instancja Monad musi spełniać własności gwarantujace, że sekwencjonowanie jest (w pewnym sensie) łączne a return jest jego elementem neutralnym:

return x >>= f    =  f x
mx >>= return     =  mx
(mx >>= f) >>= g  =  mx >>= (\y -> f y >>= g)

Asymetria tych praw wynika z asymetrii operatora (>>=):

(>>=) :: Monad m => m a -> (a -> m b) -> m b

można temu zaradzić, wyrażając je w terminach operatora złożenia Kleisli (>=>):

(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x -> f x >>= g

return >=> f      =  f
f >=> return      =  f
(f >=> g) >=> h   =  f >=> (g >=> h)

Ćwiczenie: wykaż, że powyzsze prawa są spełnione dla

instance Monad Maybe where
  return         = Just
  Nothing  >>= f = Nothing
  (Just x) >>= f = Just (f x)

Prawa dla Applicative są (przynajmniej na pierwszy rzut oka) trochę bardziej złozone:

pure id <*> x  =  x                              -- identity
pure (g x)     =  pure g <*> pure x              -- homomorphism
x <*> pure y   =  pure (\g -> g y) <*> x         -- interchange
x <*> (y <*> z) = (pure (.) <*> x <*> y) <*> z   -- composition

Ponadto mamy fmap f x = pure f <*> x.

Jeśli mamy też instancję Monad, to dodatkowo powinno zachodzić

pure = return
m1 <*> m2 = m1 >>= (x1 -> m2 >>= (x2 -> return (x1 x2)))

Ćwiczenie: wykaż spełnienie praw Applicative dla

instance Applicative Maybe where
  pure                  = Just
  Nothing  <*> _        = Nothing
  _        <*> Nothing  = Nothing
  (Just f) <*> (Just x) = Just (f x)

Konstruktywna indukcja

Metody pdobne do używanych do dowodzenia własności mogą pozwolić na konstruowanie funkcji ze specyfikacji.

Rozważmy funkcję odwracającą listę

rev :: [a] -> [a]
rev []     = []
rev (x:xs) = rev xs ++ [x]

Zauważmy, że ma ona złożoność kwadratową, gdyż (++) ma złożoność liniową zwn długość pierwszego argumentu.

Skoro problemem jest tu konkatencja, możemy spróbować zaradzić temu pisząc funkcję ogólniejszą, która łączy odwracanie i konkatenację:

rev' xs ys = rev xs ++ ys

oczywiście gdybyśmy potraktowali to jako definicję, nic by to nie pomogło, ale mozemy potraktować powyższą równość jako specyfikację i systematycznie skonstruować lepszą definicję rev':

rev' [] ys   = 
rev [] ++ ys =
[] ++ ys = ys

rev' (x:xs) ys   =
rev (x:xs) ++ ys =
(rev xs ++ [x]) ++ ys = 
rev xs ++ ([x] ++ ys) =
rev xs ++ (x:ys) =
rev' xs (x:ys)

w ten sposób otrzymujemy następującą definicję rev':

rev' [] ys     = ys
rev' (x:xs) ys = rev' xs (x:ys)

która ma złożoność liniową zwn długość pierwszego argumentu. W związku z tym

reverse xs = rev' xs []

też ma złożoność liniową.

Ćwiczenie: spróbuj podobnie ulepszyć funkcję

flatten :: Tree a -> [a]
flatten (Leaf x)   = [x]
flatten (Node l r) = flatten l ++ flattten r

Ćwiczenie: dla powyższej definicji reverse wykaż

reverse (reverse xs) = xs
reverse (xs ++ ys)   = reverse ys ++ reverse xs