Подтвердить что ты не робот

Связь между `DList` и` [] `с Codensity

В последнее время я экспериментировал с Codensity, который должен относиться к DList с [] между прочим. Во всяком случае, я никогда не нашел код, в котором говорится об этом отношении. После некоторых экспериментов я закончил с этим:

{-# LANGUAGE RankNTypes #-}
module Codensity where

newtype Codensity f a = Codensity
  { runCodensity :: forall b. (a -> f b) -> f b }

type DList a = Codensity [] [a]

nil :: DList a
nil = Codensity ($ [])

infixr 5 `cons`
cons :: a -> DList a -> DList a
cons x (Codensity xs) = Codensity ($ (xs (x:)))

append :: DList a -> DList a -> DList a
append (Codensity xs) ys = Codensity ($ (xs (++ toList ys)))

toList :: DList a -> [a]
toList xs = runCodensity xs id

fromList :: [a] -> DList a
fromList xs = Codensity (\k -> k xs)

Однако определение DList в моем примере немного нехорошее. Есть ли другой способ сформулировать это отношение? Это даже правильный способ сделать это?

4b9b3361

ОТВЕТЫ

Ответ 1

Один вид может заключаться в том, что DList - это способ переупорядочения моноидных операций, так же как Codensity - способ переупорядочения операций монады.

[] - свободный моноид на a, поэтому пусть представляют списки, используя монаду свободного писателя, то есть Free ((,) a):

module Codensity where

import Control.Monad
import Control.Monad.Free
import Control.Monad.Codensity
import Control.Monad.Trans (lift)

type DList a = Free ((,) a) ()

Теперь мы можем определить стандартные операции списка:

nil :: DList a
nil = return ()

singleton :: a -> DList a
singleton x = liftF (x, ())

append :: DList a -> DList a -> DList a
append = (>>)

infixr 5 `snoc`
snoc :: DList a -> a -> DList a
snoc xs x = xs >> singleton x

exec :: Free ((,) a) () -> [a]
exec (Free (x, xs)) = x : exec xs
exec (Pure _) = []

fromList :: [a] -> DList a
fromList = mapM_ singleton

toList :: DList a -> [a]
toList = exec

Это представление имеет те же недостатки, что и список, когда дело доходит до snoc. Мы можем проверить, что

last . toList . foldl snoc nil $ [1..10000]

занимает значительное (квадратичное) количество времени. Однако, как и каждая свободная монада, ее можно улучшить с помощью Codensity. Мы просто заменим определение на

type DList a = Codensity (Free ((,) a)) ()

и toList с

toList = exec . lowerCodensity

Теперь одно и то же выражение выполняется мгновенно, поскольку Codensity переупорядочивает операции, как и исходные списки различий.

Ответ 2

TL; ДР: DList для (++) выполняет ту же задачу, что и Codensity для (>>=): перераспределение операторов вправо.

Это полезно, потому что для обоих, (++) и (>>=), левые связанные вычисления (может) демонстрировать поведение квадратичного времени выполнения.

1. Полная история

План выглядит следующим образом:

  • Мы шаг за шагом делаем пример для (++) и (>>=), эмулируя проблему ассоциативности.
  • Мы используем CPS, чтобы избежать квадратичной сложности с DList и Codensity
  • Последствия и бонусы (Обобщите от (++) до (<>))

2. Проблема: квадратичное поведение во время выполнения

2a. Список (++)

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

Итак, давайте сначала рассмотрим проблему со списками. Конкатентная операция для списков обычно определяется как:

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

что означает, что (++) всегда будет вести аргумент first из начинать с конца. Чтобы увидеть, когда это проблема, рассмотрите следующие два вычисления:

as, bs, cs:: [Int]

rightAssoc :: [Int]
rightAssoc = (as ++ (bs ++ cs))

leftAssoc :: [Int]
leftAssoc = ((as ++ bs) ++ cs)

Начнем с rightAssoc и пройдем оценку.

as = [1,2]
bs = [3,4]
cs = [5,6]
rightAssoc = ([1,2] ++ ([3,4] ++ [5,6]))
           -- pattern match gives (1:[2]) for first arg
           = 1 : ([2] ++ ([3,4] ++ [5,6]))
           -- pattern match gives (2:[]) for first arg
           = 1 : 2 : ([] ++ ([3,4] ++ [5,6]))
           -- first case of (++)
           = 1 : 2 : ([3,4] ++ [5,6])
           = 1 : 2 : 3 : ([4] ++ [5,6])
           = 1 : 2 : 3 : 4 : ([] ++ [5,6])
           = 1 : 2 : 3 : 4 : [5,6]
           = [1,2,3,4,5,6]

Итак, мы должны пройти через as и bs.

Хорошо, что это было не так уж плохо, продолжайте leftAssoc:

as = [1,2]
bs = [3,4]
cs = [5,6]
leftAssoc = (([1,2] ++ [3,4]) ++ [5,6])
          = ((1 : ([2] ++ [3,4])) ++ [5,6])
          = ((1 : 2 : ([] ++ [3,4])) ++ [5,6])
          = ((1 : 2 : [3,4]) ++ [5,6])
          = ([1,2,3,4] ++ [5,6])
          -- uh oh
          = 1 : ([2,3,4] ++ [5,6])
          = 1 : 2 : ([3,4] ++ [5,6])
          = 1 : 2 : 3 : ([4] ++ [5,6])
          = 1 : 2 : 3 : 4 : ([] ++ [5,6])
          = 1 : 2 : 3 : 4 : [5,6]
          = [1,2,3,4,5,6]

Ух, ты видел, что нам пришлось пройти через as дважды? Как только [1,2], а затем снова внутри as ++ bs = [1,2,3,4]. С каждым дополнительный операнд, который неправильно связан, список на слева of (++), которые мы должны полностью пересекать каждый раз, будет расти больше на каждом шаге, что приводит к квадратичному времени выполнения.

Итак, как вы видите выше, связанный с левым (++) будет уничтожать производительность. Что приводит нас к:

2b. Свободная монада (>>=)

Имейте в виду, что, хотя я использую Free в качестве примера, это   также случай для других монадов, например. экземпляр для Tree ведет себя   подобный этому тоже

Сначала мы используем наивный тип Free:

data Free f a = Pure a | Free (f (Free f a))

Вместо (++), мы смотрим на (>>=), который определяется как и использует (>>=) в форме префикса:

instance Functor f => Monad (Free f) where
  return = Pure
  (>>=) (Pure a) f = f a
  (>>=) (Free m) f = Free ((>>= f) <$> m)

Если вы сравните это с определением (++) от 2a выше, вы можете см., что определение (>>=) снова смотрит на первый аргумент. Это вызывает первое беспокойство, будет ли это работать так же плохо, как в случай (++), если он связан неправильно? Ну, посмотрим, я использую Identity здесь для простоты, но выбор функтора не является важный факт здесь:

-- specialized to 'Free'
liftF :: Functor f => f a -> Free f a
liftF fa = Free (Pure <$> fa)

x :: Free Identity Int
x = liftF (Identity 20) = Free (Identity (Pure 20))

f :: Int -> Free Identity Int
f x = liftF (Identity (x+1)) = Free (Identity (Pure (x+1)))

g :: Int -> Free Identity Int
g x = liftF (Identity (x*2)) = Free (Identity (Pure (x*2)))

rightAssoc :: Free Identity Int
rightAssoc = (x >>= \x -> (f x >>= g))

leftAssoc :: Free Identity Int
leftAssoc = ((x >>= f) >>= g)

Сначала мы снова начинаем с варианта rightAssoc:

rightAssoc = (x >>= \x -> (f x >>= g))
                    ~~~
           -- definition of x
           = ((Free (Identity (Pure 20))) >>= \x -> (f x >>= g))
              ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           -- second case of definition for 'Free (>>=)
           = Free ((>>= \x -> (f x >>= g)) <$> Identity (Pure 20))
                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           -- (<$>) for Identity
           = Free (Identity ((Pure 20) >>= \x -> (f x >>= g)))
                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           -- first case of the definition for 'Free (>>=)
           = Free (Identity (f 20 >>= g))
                             ~~~~
           = Free (Identity ((Free (Identity (Pure 21))) >>= g))
                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           -- second case of definition for 'Free (>>=)
           = Free (Identity (Free ((>>= g) <$> Identity (Pure 21))))
                                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = Free (Identity (Free (Identity ((Pure 21) >>= g))))
                                             ~~~~~~~~~~~~~~~
           = Free (Identity (Free (Identity (g 21))))
                                             ~~~~
           = Free (Identity (Free (Identity (Free (Identity (Pure 42))))))

Puh, хорошо, я добавил ~~~~ под выражение, которое уменьшено в следующий шаг для ясности. Если вы достаточно сильно прищурились, вы можете увидеть некоторые знакомство с 2a 's' для rightAssoc: мы проходим два первых аргументы (теперь x и f вместо as и bs)). Не теряя времени, здесь leftAssoc:

leftAssoc = ((x >>= f) >>= g)
             ~~~
          = ((Free (Identity (Pure 20)) >>= f) >>= g)
             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = (Free ((>>= f) <$> Identity (Pure 20)) >>= g)
                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = (Free (Identity ((Pure 20) >>= f)) >>= g)
                             ~~~~~~~~~~~~~~~
          = (Free (Identity (f 20)) >>= g)
                             ~~~~
          = (Free (Identity (Free (Identity (Pure 21)))) >>= g)
            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = Free ((>>= g) <$> (Identity (Free (Identity (Pure 21)))))
                  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          -- uh oh
          = Free (Identity (Free (Identity (Pure 21)) >>= g))
                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = Free (Identity (Free ((>>= g) <$> Identity (Pure 21))))
                                  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = Free (Identity (Free (Identity ((Pure 21) >>= g))))
                                            ~~~~~~~~~~~~~~~~
          = Free (Identity (Free (Identity (g 21))))
                                            ~~~~
          = Free (Identity (Free (Identity (Free (Identity (Pure 42))))))

Если вы посмотрите внимательно, после uh oh нам нужно снести промежуточной структуры снова, как и в случае (++) (также отмечен uh oh).

2с. Результат пока

В обоих случаях leftAssoc приводит к квадратичному поведению исполнения, потому что мы несколько раз перестраиваем аргумент first и разрываем его вниз снова для следующей операции. Это означает, что на каждом этапе в оценке мы должны строить и промежуточная структура --- плохая.

3. Соотношение между DList и Codensity

Здесь мы обнаружим связь между DList и Codensity. Каждый из них решает проблему ошибочно связанных вычислений, рассмотренных выше, с использованием CPS для эффективного вправо.

3a. DList

Сначала мы введем определение DList и append:

newtype DList a = DL { unDL :: [a] -> [a] }

append :: DList a -> DList a -> DList a
append xs ys = DL (unDL xs . unDL ys)

fromList :: [a] -> DList a
fromList = DL . (++)

toList :: DList a -> [a]
toList = ($[]) . unDL

и теперь наши старые друзья:

as,bs,cs :: DList Int
as = fromList [1,2] = DL ([1,2] ++)
bs = fromList [3,4] = DL ([3,4] ++)
cs = fromList [5,6] = DL ([5,6] ++)

rightAssoc :: [Int]
rightAssoc = toList $ as `append` (bs `append` cs)

leftAssoc :: [Int]
leftAssoc = toList $ ((as `append` bs) `append` cs)

Оценка примерно следующая:

rightAssoc = toList $ (DL ([1,2] ++)) `append` (bs `append` cs)
           = toList $ DL $ unDL (DL ([1,2] ++)) . unDL (bs `append` cs)
                           ~~~~~~~~~~~~~~~~~~~~
           = toList $ DL $ ([1,2] ++) . unDL (bs `append` cs)
                                              ~~
           = toList $ DL $ ([1,2] ++) . unDL ((DL ([3,4] ++)) `append` cs)
                                              ~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = toList $ DL $ ([1,2] ++) . unDL (DL $ unDL (DL ([3,4] ++)) . unDL cs)
                                                   ~~~~~~~~~~~~~~~~~~~~
           = toList $ DL $ ([1,2] ++) . unDL (DL $ ([3,4] ++) . unDL cs)
                                                                     ~~
           = toList $ DL $ ([1,2] ++) . unDL (DL $ ([3,4] ++) . unDL (DL ([5,6] ++)))
           = toList $ DL $ ([1,2] ++) . unDL (DL $ ([3,4] ++) . ([5,6] ++))
                                        ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = toList $ DL $ ([1,2] ++) . (([3,4] ++) . ([5,6] ++))
             ~~~~~~
           -- definition of toList
           = ($[]) . unDL $ DL $ ([1,2] ++) . (([3,4] ++) . ([5,6] ++))
                     ~~~~~~~~~
           -- unDL . DL == id
           = ($[]) $ (([1,2] ++) . (([3,4] ++) . ([5,6] ++)))
           -- move ($[]) to end
           = (([1,2] ++) . (([3,4] ++) . ([5,6] ++))) []
           -- def: (.) g f x = g (f x)
           = (([1,2] ++) ((([3,4] ++) . ([5,6] ++)) []))
           = (([1,2] ++) (([3,4] ++) (([5,6] ++) [])))
           -- drop unnecessary parens
           = (([1,2] ++) (([3,4] ++) ([5,6] ++ [])))
           = ([1,2] ++ ([3,4] ++ ([5,6] ++ [])))
                                  ~~~~~~~~~~~
           -- (xs ++ []) == xs
           = ([1,2] ++ ([3,4] ++ ([5,6])))
           = (as ++ (bs ++ cs))

Хах! Результат точно такой же, как rightAssoc из 2a. Хорошо, с нарастанием напряжения, мы переходим к leftAssoc:

leftAssoc = toList $ ((as `append` bs) `append` cs)
          = toList $ (((DL ([1,2]++)) `append` bs) `append` cs)
          = toList $ ((DL (unDL (DL ([1,2]++)) . unDL bs)) `append` cs)
          = toList $ ((DL (unDL (DL ([1,2]++)) . unDL (DL ([3,4]++)))) `append` cs)
          = toList $ ((DL (([1,2]++) . ([3,4]++))) `append` cs)
          = toList $ (DL (unDL (DL (([1,2]++) . ([3,4]++))) . unDL cs))
          = toList $ (DL (unDL (DL (([1,2]++) . ([3,4]++))) . unDL (DL ([5,6]++))))
          = toList $ (DL ((([1,2]++) . ([3,4]++)) . ([5,6]++)))
          = ($[]) . unDL $ (DL ((([1,2]++) . ([3,4]++)) . ([5,6]++)))
          = ($[]) ((([1,2]++) . ([3,4]++)) . ([5,6]++))
          = ((([1,2]++) . ([3,4]++)) . ([5,6]++)) []
          -- expand (f . g) to \x -> f (g x)
          = ((\x -> ([1,2]++) (([3,4]++) x)) . ([5,6]++)) []
          = ((\x -> ([1,2]++) (([3,4]++) x)) (([5,6]++) []))
          -- apply lambda
          = ((([1,2]++) (([3,4]++) (([5,6]++) []))))
          = ([1,2] ++ ([3,4] ++ [5,6]))
          = as',bs',cs' ~ versions of 2a with no prime
          = (as' ++ (bs' ++ cs'))

Эврика! Результат корректно связан (справа), нет квадратичное замедление.

3b. Codensity

Хорошо, если вы пришли к этому моменту, вам должно быть серьезно интересно, что хорошо, потому что я тоже:). Начнем с определения и Monad экземпляра Codensity (с сокращенными именами):

newtype Codensity m a = C { run :: forall b. (a -> m b) -> m b }

instance Monad (Codensity f) where
  return x = C (\k -> k x)
  m >>= k = C (\c -> run m (\a -> run (k a) c))

-- hidden as a instance for `MonadTrans`
liftCodensity :: Monad m => m a -> Codensity m a
liftCodensity m = C (m >>=)

lowerCodensity :: Monad m => Codensity m a -> m a
lowerCodensity a = run a return

Я думаю, вы знаете, что будет дальше:

x :: Codensity (Free Identity) Int
x = liftCodensity (Free (Identity (Pure 20)))
  = C (Free (Identity (Pure 20)) >>=)
  -- note the similarity to (DL (as ++))
  -- with DL ~ Codensity and (++) ~ (>>=) !

f :: Int -> Codensity (Free Identity) Int
f x = liftCodensity (Free (Identity (Pure (x+1))))
    = C (Free (Identity (Pure (x+1))) >>=)

g :: Int -> Codensity (Free Identity) Int
g x = liftCodensity (Free (Identity (Pure (x*2))))
    = C (Free (Identity (Pure (x*2))) >>=)

rightAssoc :: Free Identity Int
rightAssoc = lowerCodensity (x >>= \x -> (f x >>= g))

leftAssoc :: Free Identity Int
leftAssoc = lowerCodensity ((x >>= f) >>= g)

Прежде чем мы снова рассмотрим оценку, вы, возможно, заинтересованы в сравнении append от DList и (>>=) от Codensity (unDL ~ run), продолжайте и сделайте это, если вы хочу, я буду ждать тебя.

Итак, начинаем с rightAssoc:

rightAssoc = lowerCodensity (x >>= \x -> (f x >>= g))
                            ~~~
           -- def of x
           = lowerCodensity ((C (Free (Identity (Pure 20)) >>=)) >>= \x -> (f x >>= g))
           -- (>>=) of codensity
           = lowerCodensity (C (\c -> run (C (Free (Identity (Pure 20)) >>=)) (\a -> run ((\x -> (f x >>= g)) a) c)))
           -- run . C == id
           = lowerCodensity (C (\c -> Free (Identity (Pure 20)) >>= \a -> run ((\x -> (f x >>= g)) a) c))
           -- substitute x' for 'Free (Identity (Pure 20))' (same as only x from 2b)
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (f x >>= g)) a) c))
                                                                ~~~
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (Free (Identity (Pure (x+1))) >>=)) >>= g) a) c))
                                                                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> run (C (Free (Identity (Pure (x+1))) >>=)) (\a2 -> run (g a2) c2)))) a) c))
                                                                           ~~~~~~
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (Free (Identity (Pure (x+1))) >>=) (\a2 -> run (g a2) c2)))) a) c))
           -- again, substitute f' for '\x -> Free (Identity (Pure (x+1)))' (same as only f from 2b)
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> run (g a2) c2)))) a) c))
                                                                                                   ~~~~
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> run (C (Free (Identity (Pure (a2*2))) >>=)) c2)))) a) c))
                                                                                              ~~~~~~
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> (Free (Identity (Pure (a2*2))) >>=) c2)))) a) c))
           -- one last time, substitute g' (g from 2b)
           = lowerCodensity (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> (g' a2 >>=) c2)))) a) c))
           -- def of lowerCodensity
           = run (C (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> (g' a2 >>=) c2)))) a) c)) return
           = (\c -> x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> (g' a2 >>=) c2)))) a) c) return
           = (x' >>= \a -> run ((\x -> (C (\c2 -> (f' x >>=) (\a2 -> (g' a2 >>=) c2)))) a) return)
                                 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = (x' >>= \a -> run (C (\c2 -> (f' a >>=) (\a2 -> (g' a2 >>=) c2))) return)
                           ~~~~~~
           = (x' >>= \a -> (\c2 -> (f' a >>=) (\a2 -> (g' a2 >>=) c2)) return)
                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
           = (x' >>= \a -> (f' a >>=) (\a2 -> g' a2 >>= return))
           -- m >>= return ~ m
           = (x' >>= \a -> (f' a >>=) (\a2 -> g' a2))
           -- m >>= (\x -> f x) ~ m >>= f
           = (x' >>= \a -> (f' a >>= g'))
           -- rename a to x
           = (x' >>= \x -> (f' x >>= g'))

И теперь мы можем видеть, что (>>=) связаны справа, это пока еще не удивительно, учитывая, что это также имеет место в начале. Итак, в ожидании, мы обращаем наше внимание на наши последняя и окончательная оценка, leftAssoc:

leftAssoc = lowerCodensity ((x >>= f) >>= g)
          -- def of x
          = lowerCodensity ((C (Free (Identity (Pure 20)) >>=) >>= f) >>= g)
          -- (>>=) from Codensity
          = lowerCodensity ((C (\c -> run (C (Free (Identity (Pure 20)) >>=)) (\a -> run (f a) c))) >>= g)
                                      ~~~~~~
          = lowerCodensity ((C (\c -> (Free (Identity (Pure 20)) >>=) (\a -> run (f a) c))) >>= g)
          -- subst x'
          = lowerCodensity ((C (\c -> (x' >>=) (\a -> run (f a) c))) >>= g)
          -- def of f
          = lowerCodensity ((C (\c -> (x' >>=) (\a -> run (C (Free (Identity (Pure (a+1))) >>=)) c))) >>= g)
                                                      ~~~~~~
          = lowerCodensity ((C (\c -> (x' >>=) (\a -> (Free (Identity (Pure (a+1))) >>=) c))) >>= g)
          -- subst f'
          = lowerCodensity ((C (\c -> (x' >>=) (\a -> (f' a >>=) c))) >>= g)
                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
          = lowerCodensity (C (\c2 -> run (C (\c -> (x' >>=) (\a -> (f' a >>=) c))) (\a2 -> run (g a2) c2)))
                                      ~~~~~~
          = lowerCodensity (C (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> run (g a2) c2)))
          -- def of g
          = lowerCodensity (C (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> run (C (Free (Identity (Pure (a2*2))) >>=)) c2)))
                                                                                    ~~~~~~
          = lowerCodensity (C (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> (Free (Identity (Pure (a2*2))) >>=) c2)))
          -- subst g'
          = lowerCodensity (C (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> (g' a2 >>=) c2)))
          -- def lowerCodensity
          = run (C (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> (g' a2 >>=) c2))) return
          = (\c2 -> (\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> (g' a2 >>=) c2)) return
          = ((\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> g' a2 >>= return))
          = ((\c -> (x' >>=) (\a -> (f' a >>=) c)) (\a2 -> g' a2))
          = ((\c -> (x' >>=) (\a -> (f' a >>=) c)) g')
          = (x' >>=) (\a -> (f' a >>=) g')
          = (x' >>=) (\a -> (f' a >>= g')
          = (x' >>= (\a -> (f' a >>= g'))
          = (x' >>= (\x -> (f' x >>= g'))

Наконец,, мы имеем это, все привязки, связанные с правом, просто как они нам нравятся!

4. Последствие

Если вы сделали это до сих пор, поздравляю. Обозначим, что мы сделал:

  • Мы продемонстрировали проблему с неверно ассоциированным (++) в 2a и (>>=) в 2b
  • Мы показали решение, используя DList в 3a и Codensity в 3b.
  • Продемонстрирована сила эквационального рассуждения в Haskell:)

5. Бонус

Actuall, мы можем обобщить DList из (++) и вместо этого использовать (<>) получить DMonoid, переупорядочить (<>).

newtype DMonoid m = DM { unDM :: m -> m }

instance Monoid m => Monoid (DMonoid m) where
  mempty = DM (mempty <>)
  x `mappend` y = DM (unDM x . unDM y)

liftDM :: Monoid m => m -> DMonoid m
liftDM = DM . (<>)

lowerDM :: Monoid m => DMonoid m -> m
lowerDM = ($ mempty) . unDM

Тогда сравнение идет следующим образом:

  • DMonoid - это (мое изобретение) " моноидный трансформатор", переписывающий (<>) вправо
  • Codensity - это монадный трансформатор, перезаписывающий (>>=) вправо