О церковных зашифрованных списках в Хаскеле

Question

Различные проблемы оптимизации, такие как этот , привели к закодированным в Church спискам как к способу объединения потоков, то есть устранению промежуточных результатов компилятором (например, списков).Вот определение, которое было успешно использовано в задаче оптимизации:

{-# LANGUAGE RankNTypes #-}

-- A list encoded as a strict left fold.
newtype ListL a = ListL {build :: forall b. (b -> a -> b) -> b -> b}

Вот как я смотрю на что-то из Церкви: вместо того, чтобы спрашивать, что такое «что-то» , это , спрашивайте, что это может сделать для вас.В случае списков ответ таков: списки можно сложить.Чтобы сложить, мне нужна функция «update» типа b->a->b и начальное значение типа b.Затем я верну вам результат сгиба типа b.Отсюда и определение ListL.Вот несколько основных операций над ListL:

mapL :: (a -> a') -> ListL a -> ListL a'
mapL f l = ListL (\f' b' -> build l (\b a -> f' b (f a)) b')

instance Functor ListL where fmap = mapL

fromList :: [a] -> ListL a
fromList l = ListL (\c z -> foldl' c z l)

toList :: ListL a -> [a]
toList l = build l snoc [] where snoc xs x = xs ++ [x]

nullL :: ListL a -> Bool
nullL l = build l (\_ _->False) True

Вот еще:

filterL :: (a->Bool) -> ListL a -> ListL a
filterL p l = ListL (\f b->build l (\b' a'->if p a' then f b' a' else b') b)

iterUntil :: (a->Bool) -> a -> (a->a) -> ListL a
iterUntil p a f = ListL (\g b-> snd $ until (p.fst) (\(a',b')->(f a', g b' a')) (a,b))

iterUntil выполняет итерацию функции a->a, начиная с некоторого значения типа a, пока не будет выполнен предикат a->bool.Такая функция, как Prelude iterate, невозможна - по крайней мере, я не знаю, как ее определить, это должна быть какая-то рекурсия.

Продолжая с примерами,length и sum - просто упражнения по выбору правильной функции «update» и начального значения в foldl:

lengthL :: ListL a -> Int
lengthL l = build l (\b _ -> b+1) 0

sumL :: Num a => ListL a -> a
sumL l = build l (+) 0

Теперь давайте попробуем headL:

headL :: ListL a -> a
headL l = build l (\_ a->a) _   -- this does not compile!

Независимо от того, какой стартовый номер b указан, первый a должен быть возвращен.build l нужен b, но у нас его нет.Это странно: в основном мы хотим сказать компилятору: вам не нужно b, поверьте мне ... A headL' :: ListL a -> ListL a, с другой стороны, легко построить.error "empty list!" вместо отверстия _ не работает, потому что его всегда называют - лень, кажется, не заботится об этом.Итак, с headL я застрял.Поэтому здесь

Вопрос 1: Как реализовано headL?

Вторая проблема возникает при попытке реализовать эквивалент repeatM :: Monad m => m a -> m [a].Как и в случае iterUntil, для остановки итерации необходим предикат a->Bool:

iterUntilM :: Monad m => (a->Bool) -> m a -> m (ListL a)

Цель ясна: повторять монадическое действие m a до тех пор, пока a->Bool не будет выполнено.Идея, конечно, состоит в том, чтобы сразу сложить ListL a и добиться объединения потоков (объединение списков).Например:

import System.Random (randomIO)

main :: IO ()
main = do
     rs <- iterUntilM (>42::Int) randomIO
     print $ lengthL rs

Пример довольно надуманный, он печатает количество проведенных розыгрышей, пока не было найдено первое число> 42.В более реалистичной настройке монада m представляет собой, например, монаду ST s, которая оборачивает некоторую FFI.Дело в том, что это должно работать эффективно.Я полностью застрял с этим.Как мне связать (>>=) :: m a -> (a->m b) -> m b с build, чтобы получить m (ListL a)?Т.е. это

Вопрос 2: Как реализовано iterUntilM?

Является ли это хорошим учебным упражнением, разве это хорошая идея?

Answer 1

В общем случае, когда вы удаляете предположения о типе, функция, которую вы пишете, будет не только более общей (с точки зрения того, какие типы она может использовать), она также будет более специфичной относительно того, что именноэто делает.Вот что происходит с церковным кодированием, допускающим слияние: когда списки представлены как

data [a] = [] | a : [a]

Существует бесчисленное множество способов использовать их в функции, только один из которых - foldr.Однако, когда у вас есть:

newtype List a = { runList :: forall b. (a -> b -> b) -> b -> b }

только *1011* способ использовать этот тип через foldr.Это то, что позволяет вам делать оптимизацию, которую мы знаем и любим.Кстати, Stream Fusion - лишь один из них: вы также получаете O (1) append, например.

Ваш тип еще более ограничен: он говорит нам, что базовый списокне может быть (многозначно) бесконечным.

Существует еще одно ограниченное представление списков, которое смещает фокус:

data List a = forall b. List b (b -> Maybe (a, b))

Если список, закодированный церковью, является потребителем, это производитель .В нем ничего не говорится о том, как можно использовать этот список, но о том, как его можно составить, очень много.

Итак, мы увидели, что мы многое получаем из этих ограниченных представлений, что мы теряем?tail хороший пример.Для производителя:

tail (List x f) = case f x of
  Just (_,xs) -> List xs f

А для потребителя:

tail xs =
    List (\c n ->
        runList xs 
            (\h t g -> g h (t c)) 
            (const n) 
            (const id))

Реализация для потребителя составляет O (n) , тогда как для производителя, очевидно, O (1) .

Оба эти типа могут допускать объединение, но некоторые функции могут быть реализованы более эффективно в одном, чем в другом.Случайно GHC выбрал первое представление в качестве основы для слияния, но нет ничего фундаментального, что делает этот выбор превосходным: большинство функций, которые использовал Хаскеллер, просто, казалось, работали лучше в паттерне слияния foldr/build, чем другие.В других местах используется шаблон развертывания.

Эта преамбула на пути, есть два вопроса, которые мы должны задать:

• Выполните эти функции(head и iterUntilM) эффективно работают только в представлении foldr (например, добавление), или в представлении unfoldr (например, tail), или в обоих (например, map)?
• Правильно ли выбрана строгая кодировка влево?Это слишком ограниченно (т.е. нам нужно foldr?), Или оно может быть ограничено еще больше?

head может быть легко реализовано в списках с кодировкой foldr:

head xs = runList xs const (error "head: empty list")

В foldl' -списках это немного сложнее:

head xs =
    fromMaybe
        (error "head: empty list")
        (build xs (\xs x -> maybe (Just x) Just xs) Nothing)

Вы заметите, что эта функция (например, tail в foldr -списках) О (п) * * тысячу семьдесят-один.Это также не работает для бесконечных списков.Это хороший признак того, что foldl' не является правильным выбором для слияния head.

Теперь для iterUntilM мы видим случай, когда (я не думаю), даже Возможен сплав .Поскольку m заканчивается снаружи, вы должны запустить все эффекты в списке (материализуя его).

Для хорошего обзора этой области, посмотрите this сообщение в блоге.