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).
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...
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?
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.
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.
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.
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?
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…