Kodowanie Churcha

church.md

Kodowanie Churcha

Dziś chcę opowiedzieć o kodowaniu Churcha, które jest za równo piękną konstrukcją w teorii obliczeń, jak i w praktyce.

Wymagana wiedza:

• podstawy rachunku lambda;
• podstawy Haskella (struktury danych, klasy typów; byłoby świetnie, gdybyś znał: dyrektywy RankNTypes, INLINE, SPECIALIZE, stream fusing).

Czym jest kodowanie Churcha?

Pierwotnie, kodowanie Churcha pozwalało na zapisanie liczb naturalnych jako lambda-termów. Te zaś, intuicyjnie, odpowiadały n-krotnej aplikacji termu na x, podobnie jak n-krotne złożenie funkcji na x.

Wbrew pozorom, ta zabawka pozwoliła na dowiedzenie, że mogą istnieć takie obiekty, które są podobne do liczb naturalnych (de facto nie są, ale są takie same z dokładnością do izomorfizmu). Można było pokazać, że zbiór N takich lambda-termów wraz z (N, +, S, 0 *) tworzą tzw. arytmetykę Peano, czyli pewną formalizację liczb naturalnych. Nie będę tego tutaj robić, ale możecie mi wierzyć na słowo.

By pobudzić Waszą intuicję, przykładowymi liczebnikami Churcha są:

zero = \f x -> x
three = \f x -> f ( f ( f x ) ) 
seven = \f x -> f ( f ( f ( f ( f ( f ( f x ) ) ) ) ) )
-- i tak dalej...

Liczby Churcha w Haskellu

Zacznijmy najpierw od klasycznego przykładu w Haskellu.

Jak widzimy, mamy do czynienia z obiektem, który jest typu (a -> a) -> a -> a, ponieważ f jest typu a -> a skoro ma być składany ze samym sobą. Również potrzebujemy wartości, którą zaaplikujemy do złożenia — nie jest to niespodzianką, że ta wartość jest typu a. Stąd możemy zrobić wrapper na obiekty tego typu za pomocą newtype.

newtype NatC a = NC { unNat :: (a -> a) -> a -> a }

Skoro są to obiekty izomorficzne z liczbami naturalnymi, zaimplementujmy je. Potrzebujemy najpewniej element neutralny dodawania, czyli zero. Podaliśmy go już wyżej, ale napiszmy go jeszcze raz:

zero :: NatC a
zero = NC $ \f x -> x

Potrzebujemy również funkcji następnika, która będzie polegać na nałożeniu funkcji f jeszcze raz.

succ :: NatC a -> NatC a
succ (NC n) = NC $ \f x -> f (n f x)

czy też, alternatywnie

succ (NC n) = NC $ \f x -> n f (f x)

Do tego będziemy chcieli mieć funkcję pomocniczą, która zamieni Int na NatC a.

toNatC :: Int -> NatC a
toNatC 0 = zero
toNatC n = NC $ \f x -> f (unNat (toNatC (n - 1)) f x)

Dodawanie, z prostej obserwacji, jest n-krotnym złożeniem na m-krotnym złożeniu funkcji f na x (f^m(f^n(x)) = f^(m + x) (x)), co zapisujemy:

(+) :: NatC a -> NatC a -> NatC a
(NatC n) + (NatC m) = NC $ \f x -> n f (m f x)

Mnożenie, w podobny sposób, jest n-krotnym złożeniem m-krotnego złożenia f na x (n razy składamy m-krotne złożenie, czyli dostajemy n * m-krotne złożenie).

(*) :: NatC a -> NatC a -> NatC a 
(NatC n) * (NatC m) = NC $ \f x -> n (m f) x

W taki sposób otrzymaliśmy pewną reprezentację liczby naturalnej jako sposób działania na niej niżeli jako zwyczajny obiekt. Co więcej, liczebniki Churcha zapisać jako

data NatP
  = Succ NatP
  | Zero

i wskazać między nimi izomorfizm:

pToC :: NatP -> NatC a
pToC Zero = zero
pToC (Succ nP) = NC $ \f x -> f (unNat (pToC nP) f x)

cToP :: NatC a -> NatP
cToP (NC n) = n Succ Zero

Więc czemu nie korzystać z wersji, która siedzi w pamięci zamiast tej, która opisuje sposób przetworzenia tej struktury danych za pomocą jej zwinięcia?

Zaskakujący fakt

Okazuje się, że zwinięcie (a.k.a foldr/foldl, bądź po prostu fold) jest w pewien sposób tożsame ze strukturą danych. To oznacza, że również możemy przechowywać strukturę danych jako jej zwinięcie.

Ma to swoje wady i zalety. Zdecydowanie wadą tego rozwiązania jest potrzeba zamiany toższamej z foldr struktury na tą, która istnieje w pamięci, więc nie jest to dobra struktura do zastosowań, gdzie całe dane muszą istnieć w pamięci.

Czasem jest wygodniej operować na takich strukturach, jeśli one bazują na innych, na których możemy zrobić fold-a, ponieważ część z nich oferuje optymalizacje znane też jako ang. stream fusion.

Fuzja strumieni

Stream fusion jest techniką, która nieco odpowiada technice loop fusing, lub loop unwinding w językach imperatywnych. Twórcy bibliotek tj. bytestring, vector, czy też biblioteki standardowej, udostępniają kompilatorowi pewne reguły przepisywania drzew syntaktycznych. Kompilator, widząc je, podczas optymalizacji przepisuje kod za pomocą tych reguł na bardziej specjalistyczne funkcje.

Przykładem może być taki kod:

bitStream :: [Word8] -> [Bool]
bitStream = concat . map extractBits

który może być śmiało zapisany jako

bitStream = concatMap extractBits

przez co zyskujemy na pojedynczym przebiegu przez listę bajtów.

Podobne optymalizacje dzieją się w bibliotekach bytestring, czy vector, ponieważ te optymalizacje są wprowadzane za pomocą dyrektyw RULES. Więcej tu.

Lista Churcha

Tym samym tropem można pójść, pisząc listę za pomocą kodowania Churcha.

Dlaczego byśmy chcieli ją pisać? I jaki ma związek z stream fusion? Nie należy zapominać, że struktury zapisane za pomocą kodowania Churcha to nic innego jak złożone ze sobą funkcje. Złożenia funkcji łatwiej poddać stream fusion, niż strukturze, która już istnieje w pamięci; tym bardziej, nie jestem w stanie sobie wyobrazić, jak by miał działać stream fusion na bytach, które nie przetwarzają danej struktury.

Przypomnijmy sobie typ funkcji foldr dla listy.

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

Podobnie jak w NatP funkcja a -> b -> b odpowiada za (:) a b jako []. Poza tym, faktem jest, że:

xs == foldr (:) [] xs

Stąd możemy śmiało stworzyć strukturę danych

{-# LANGUAGE RankNTypes #-} -- by móc kwantyfikować typy na poziomie sub-termów.
newtype ListC a = LC { unList :: forall b. (a -> b -> b) -> b -> b } 

Oczywiście pozostaje implementacja mapC, concatC, concatMapC, nilC, czy consC.

mapC :: (a -> b) -> ListC a -> ListC b
mapC f as = LC $ \op z -> unList as (\a b -> (f a) `op` b) z

concatC :: ListC (ListC a) -> ListC a
concatC f aas = LC $ \op z -> unList aas (\as b -> unList as op b) z

concatMapC :: (a -> ListC b) -> ListC a -> ListC b
concatMapC f as = LC $ \op z -> unList as (\a b -> unList (f a) `op` b) z

nilC :: ListC a
nilC = LC $ \op z -> z

consC :: a -> ListC a -> ListC a
consC a as = LC $ \op z -> a `op` (unList as op z)

{-# INLINE mapC, concatC, concatMapC, nilC, consC #-}

Do tych funkcji możemy dorzucić, przykładowo, funkcję zamieniającą leniwy ByteString na ListC Word8.

import qualified Data.ByteString.Lazy as L

-- ... --

fromLazyBS :: L.ByteString -> ListC Word8
fromLazyBS bs = LC $ \op z -> L.foldr op z bs

{-# INLINE fromLazyBS #-}

W łatwy sposób możemy z takiej listy zrobić listę bitów.

import Data.Bits (testBit)

-- ... --

fromFoldable :: (Foldable f) => f a -> ListC a
fromFoldable fa = LC $ \op z -> foldr op z fa
{-# SPECIALIZE fromFoldable :: [a] -> ListC a #-}

toBitStream :: L.ByteString -> ListC Bool
toBitStream bs = concatMapC (fromFoldable . bits) . fromLazyBS
  where
    bits b = map (b `testBit) (reverse [0..7])
    
{-# INLINE fromFoldable, toBitStream #-}

Dodając tylko, dyrektywy INLINE pozwalają na dosłowne przepisanie kodu w ramach wywołania. Co więcej, chcemy mieć możliwość INLINE wszystkich funkcji, ponieważ liczymy bardzo na zaimplementowany mechanizm stream fusion w bibliotece bytestring.

Ponadto poddałem specjalizacji fromFoldable, przez co Haskell zaciągnie mi konkretną instancję foldr dla list i, co więcej, będę mógł liczyć stąd na dalszy stream fusing.

Jakiś przykład zastosowania?

Załóżmy, że mamy do policzenia najdłuższy ciąg tych samych bitów po sobie danym strumieniu. Wobec tego możemy napisać taki kod:

data LongestRun 
  = LR
  { lastBit    :: {-# UNPACK #-} !Bool
  , longestRun :: {-# UNPACK #-} !Int
  , run        :: {-# UNPACK #-} !Int
  }

step :: Bool -> LongestRun -> LongestRun
step b (LongestRun lastBit longestRun run) = LongestRun b (max longest current) current
  where
    current = if lastBit == b then run + 1 else 1

initState :: LongestRun
initState = LongestRun True 0 0

longestRunC :: ListC Bool -> Int
longestRunC bs = longestRun $ build bs step initState

{-# INLINE step, initState, longestRunC #-}

Połączmy wszystko w całość:

import qualified Data.ByteString.Lazy as L

main :: IO ()
main = do
  bs <- L.getContents
  print $ longestRunC $ toBitStream bs

(Dyrektywa UNPACK pozwala na pozbycie się thunka z pola, a wykrzyknik wymaga, by pole było obliczane gorliwie, tzw. strict evaluation).

Na moim komputerze, wykonywanie tego programu, dla jednomegabajtowego wycinku /dev/urandom zajęło mi jakieś 0.8–0.9 sekundy, przy flagach -O -O2. Dla porównania dla takiego samego programu napisanego w C zajęło mi to 0.2 sekundy, więc w zasadzie tracimy do C jedynie 3 razy tyle. Piękne, prawda?

Podsumowanie

Kodowanie Churcha okazuje się być przydatne w kontekście optymalizacji, kiedy zależy nam na traktowaniu przekształceń na liście jako samej listy. Dzięki temu można użyć fuzji strumieni, przez co kod staje się optymalny i czysty — należy zauważyć, że ani razu nie wykorzystaliśmy kodu, który by sugerował niskopoziomowy dostęp do danych. Jedynie przez przepisywanie drzew i inlining mogliśmy użyć stream fusion, który zadziałał.

Ta technika wydaje się obiecująca dla przetwarzania strumieniowego. Warto zauważyć, że zachowywaliśmy stałą pamięć, ponieważ fold na leniwym bytestringu był, jak się okazuje, leniwy. Stąd przekształcanie takiej listy nie prowadzi do wyliczenia w całości tego bytestringa.

Można również rozważyć użycie takiej listy z użyciem monady stanu, czy ST. Również ciekawe wydaje się użycie monady Writer nad monoidem Data.ByteString.Builder w ramach kodowania danych (Builder jest czystym interfejsem opartym o monoid, który pozwala na konstrukcję różnych leniwych bytestringów).

I ktoś mi powie, że studia nie przydały się w życiu…