Как два продолжения могут компенсировать друг друга?

Question

Я читаю Некоторые хитрости для манипулирования списками , и он содержит следующее:

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k c = k (\((y:ys),r) -> c (ys,(x,y):r)) 

То, что мы видим здесь, это то, что у нас есть два продолжения в стекедруг на другаКогда это происходит, они часто могут «отменять», например:

zipRev xs ys = snd (foldr f (ys,[]) xs)
  where
    f x (y:ys,r) = (ys,(x,y):r)

Я не понимаю, как вы «отменяете» сложенные продолжения, чтобы попасть из верхнего блока кода в нижнийодин.Какой шаблон вы ищете, чтобы сделать это преобразование, и почему оно работает?

Answer 1

Функция f :: a -> b может быть «замаскирована» внутри двойного продолжения как функция f' :: ((a -> r1) -> r2) -> ((b -> r1) -> r2).

obfuscate :: (a -> b) -> ((a -> r1) -> r2) -> (b -> r1) -> r2
obfuscate f k2 k1 = k2 (k1 . f)

obfuscate обладает приятным свойством, что она сохраняет состав и идентичность функции: вы можете доказатьчто obfuscate f . obfuscate g === obfuscate (f . g) и что obfuscate id === id в несколько шагов.Это означает, что вы часто можете использовать это преобразование, чтобы распутать вычисления с двойным продолжением, которые составляют obfuscate d функций вместе, вычленяя obfuscate из композиции.Этот вопрос является примером такого распутывания.

f в верхнем кодовом блоке является obfuscate d версией f в нижнем блоке (точнее, top f xobfuscate d версия bottom f x).Вы можете увидеть это, заметив, как top f применяет внешнее продолжение к функции, которая преобразует свой вход, а затем применяет все это к внутреннему продолжению, как в теле obfuscate.

мы можем начать распутывать zipRev:

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x = obfuscate (\(y:ys,r) -> (ys,(x,y):r))

Так как действие foldr здесь состоит в том, чтобы составить кучу obfuscate d функций друг с другом (и применить все это к id,который мы можем оставить справа), мы можем вычислить obfuscate снаружи всей складки:

zipRev xs ys = obfuscate (\accum -> foldr f accum xs) id snd (ys,[])
  where
    f x (y:ys,r) = (ys,(x,y):r)

Теперь примените определение obfuscate и упростите:

zipRev xs ys = obfuscate (\accum -> foldr f accum xs) id snd (ys,[]) 
zipRev xs ys = id (snd . (\accum -> foldr f accum xs)) (ys,[])
zipRev xs ys = snd (foldr f (ys,[]) xs)

QED!

Answer 2

Для данной функции

g :: a₁ -> a₂

мы можем поднять ее до функции в продолжениях, переключив порядок:

lift g = (\c a₁ -> c (g a₁))
    :: (a₂ -> t) -> a₁ -> t

Это преобразование является контравариантным функтором, то естьон взаимодействует с композицией функций, переключая ее порядок:

g₁ :: a₁ -> a₂
g₂ :: a₂ -> a₃

lift g₁ . lift g₂
== (\c₁ a₁ -> c₁ (g₁ a₁)) . (\c₂ a₂ -> c₂ (g₂ a₂))
== \c₂ a₁ -> (\a₂ -> c₂ (g₂ a₂)) (g₁ a₁)
== \c₂ a₁ -> c₂ (g₂ (g₁ a₁)) 
== lift (g₂ . g₁)
    :: (a₃ -> t) -> a₁ -> t

lift id
== (\c a₁ -> c a₁)
== id
    :: (a₁ -> t) -> a₁ -> t

Таким же образом мы можем снова поднять поднятую функцию для функции на сложенных продолжениях с обратным порядком порядка:

lift (lift g)
== (\k c -> k ((\c a₁ -> c (g a₁)) c))
== (\k c -> k (\a₁ -> c (g a₁)))
    :: ((a₁ -> t) -> u) -> (a₂ -> t) -> u

Суммирование двух контравариантных функторов дает нам (ковариантный) функтор:

lift (lift g₁) . lift (lift g₂)
== lift (lift g₂ . lift g₁)
== lift (lift (g₁ . g₂))
    :: ((a₁ -> t) -> u) -> (a₃ -> t) -> u

lift (lift id)
== lift id
== id
    :: ((a₁ -> t) -> u) -> (a₁ -> t) -> u

Это именно то преобразование, которое в вашем примере инвертируется с помощью g = \(y:ys, r) -> (ys, (x, y):r).Этот g является эндоморфизмом (a₁ = a₂), и foldr составляет кучу его копий с различными x.То, что мы делаем, это замена композиции функций с двойным поднятием на функцию двойного лифта композиции функций, что является просто индуктивным применением законов функторов:

f :: x -> a₁ -> a₁
c :: (a₁ -> t) -> u
xs :: [x]

foldr (\x -> lift (lift (f x))) c xs
== lift (lift (\a₁ -> foldr f a₁ xs)) c
    :: (a₁ -> t) -> u

Answer 3

пользователь user11228628 привел меня к пониманию.Вот несколько идей, которые я получил во время чтения, и некоторые пошаговые преобразования.

---

Insights

• Продолжения не отменяются напрямую.Они в конечном итоге могут быть отменены (путем бета-сокращения), потому что их можно выделить.
• Шаблон, который вы ищете для этого преобразования, - \k c -> k (c . f) (или, если вы любите нечитабельные, бессмысленные, (. (. f))) для любого f (обратите внимание, что f не является параметром для лямбды).
• Как duplode указывает в комментарии , функции стиля продолжения передачиможет рассматриваться как функтор, и obfuscate является их определением fmap.
• Хитрость извлечения функции, подобной этой, из foldr работает для любой функции, которая может быть допустимой fmap.

---

Полное преобразование из первого блока кода во второй

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k c = k (\((y:ys),r) -> c (ys,(x,y):r))

Извлечение c из лямбды

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k c = k (c . \((y:ys),r) -> (ys,(x,y):r))

Замена obfuscate для его определения

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x = obfuscate (\((y:ys),r) -> (ys,(x,y):r))

Извлечение obfuscate из лямбды

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f = obfuscate . \x ((y:ys),r) -> (ys,(x,y):r)

Извлечение obfuscate из f

zipRev xs ys = foldr (obfuscate . f) id xs snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

Сobfuscate следует законам Функтора, мы можем вытащить его из foldr

zipRev xs ys = obfuscate (flip (foldr f) xs) id snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

Inline obfuscate

zipRev xs ys = (\k c -> k (c . flip (foldr f) xs)) id snd (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

Бета-уменьшение

zipRev xs ys = (id (snd . flip (foldr f) xs)) (ys,[])
  where
    f x ((y:ys),r) = (ys,(x,y):r)

Упрощение

zipRev xs ys = snd (foldr f (ys,[]) xs)
  where
    f x (y:ys,r) = (ys,(x,y):r)

---

Обоснование для функций вытягивания, которые действительны fmap с из foldr

foldr (fmap . f) z [x1,x2,...,xn]

Расширение foldr

(fmap . f) x1 . (fmap . f) x2 . ... . (fmap . f) xn $ z

Встроенный внутренний . s

fmap (f x1) . fmap (f x2) . ... . fmap (f xn) $ z

Применение законов Функтора

fmap (f x1 . f x2 . ... . f xn) $ z

Этап-расширениераздел в скобках

fmap (\z2 -> f x1 . f x2 . ... . f xn $ z2) z

Напишите лямбда-тело в терминах foldr

fmap (\z2 -> foldr f z2 [x1,x2,...,xn]) z

Напишите лямбда-тело в терминах flip

fmap (flip (foldr f) [x1,x2,...,xn]) z

---

Бонус: Обоснование для функций вытягивания, которые действительны contramap с из foldr

foldr (contramap . f) z [x1,x2,...,xn]

Расширение foldr

(contramap . f) x1 . (contramap . f) x2 . ... . (contramap . f) xn $ z

Встроенный внутренний .s

contramap (f x1) . contramap (f x2) . ... . contramap (f xn) $ z

Применение контравариантных законов

contramap (f xn . ... . f x2 . f x1) $ z

Этап - разверните раздел в скобках

contramap (\z2 -> f xn . ... . f x2 . f x1 $ z2) z

Напишите лямбда-тело в терминах foldr

contramap (\z2 -> foldr f z2 [xn,...,x2,x1]) z

Напишите лямбда-тело в виде flip

contramap (flip (foldr f) [xn,...,x2,x1]) z

Применить foldr f z (reverse xs) = foldl (flip f) z xs

contramap (flip (foldl (flip f)) [x1,x2,...,xn]) z

Answer 4

Давайте начнем с нескольких косметических настроек:

-- Note that `g x` is an endomorphism.
g :: a -> ([b], [(a,b)]) -> ([b], [(a,b)])
g x ((y:ys),r) = (ys,(x,y):r)

zipRev xs ys = foldr f id xs snd (ys,[])
  where
    f x k = \c -> k (c . g x)

f передает продолжение (c . g x) в другую функцию (k, "двойное продолжение", как user11228628).

В то время как мы можем разумно ожидать, что повторное использование f в процессе сгибания каким-то образом будет составлять g x эндоморфизмы, составленные из элементов списка, порядок, в которомсоставные эндоморфизмы могут быть не очевидны сразу, поэтому нам лучше пройти несколько шагов сгиба, чтобы убедиться:

-- x0 is the first element, x1 the second, etc.
f x0 k0 
\c -> k0 (c . g x0)
\c -> (f x1 k1) (c . g x0) -- k0 is the result of a fold step.
\c -> (\d -> k1 (d . g x1)) (c . g x0) -- Renaming a variable for clarity.
\c -> k1 (c . g x0 . g x1)
-- etc .
-- xa is the *last* element, xb the next-to-last, etc.
-- ka is the initial value passed to foldr.
\c -> (f xa ka) (c . g x0 . g x1 . . . g xb)
\c -> (\d -> ka (d . g xa)) (c . g x0 . g x1 . . . g xb)
\c -> ka (c . g x0 . g x1 . . . g xb . g xa)

ka, начальное значение, переданное в foldr, равно id,что делает вещи немного проще:

foldr f id xs = \c -> c . g x0 . g x1 . . . g xa

Поскольку все, что мы делаем с аргументом c, переданным foldr f id xs, это посткомпоновка его с эндоморфизмами, мы могли бы также выделить его изсложите:

zipRev xs ys = (snd . foldr h id xs) (ys,[])
  where
    h x e = g x . e

Обратите внимание, как мы прошли путь от c . g x до g x . e.Это, вероятно, можно описать как побочный эффект обмана CPS в исходной реализации.

Последний шаг - это замечание того, как h x e = g x . e точно соответствует тому, что мы сделали бы для реализации foldr в терминахfoldMap для Endo моноида .Или, если выразить это более явно:

foldEndo g i xs = foldr g i xs  -- The goal is obtaining an Endo-like definition.

foldEndo _ i [] = i
foldEndo g i (x : xs) = g x (foldEndo g i xs)

foldEndo g i xs = go xs i
    where
    go [] = \j -> j
    go (x : xs) = \j -> g x (foldEndo g j xs)

foldEndo g i xs = go xs i
    where
    go [] = \j -> j
    go (x : xs) = \j -> g x (go xs j)

foldEndo g i xs = go xs i
    where
    go [] = id
    go (x : xs) = g x . go xs

foldEndo g i xs = go xs i
    where
    h x e = g x . e
    go [] = id
    go (x : xs) = h x (go xs)

foldEndo g i xs = go xs i
    where
    h x e = g x . e
    go xs = foldr h id xs

foldEndo g i xs = foldr h id xs i
    where
    h x e = g x . e

Это в конечном итоге приводит нас к тому, что мы искали:

zipRev xs ys = snd (foldr g (ys,[]) xs)

Answer 5

Давайте попробуем разобраться в этом коде с элементарной точки зрения. Что это вообще делает, интересно?

zipRev xs ys = foldr f id xs snd (ys,[])
  where
     -- f x k c = k (\(y:ys, r) -> c (ys, (x,y):r))
        f x k c = k (g x c) 
     --         = (k . g x) c   -- so,
     -- f x k   =  k . g x

        g x   c       (y:ys, r) =  c (ys, (x,y):r)

Здесь мы использовали лямбда-лифтинг , чтобы восстановить g комбинатор .

Итак, поскольку f x k = k . g x, где k идет влево из x, список ввода переводится в обратную цепочку композиций,

foldr f id [x1, x2, x3, ..., xn]   where  f x k = k . g x
  ===>> 
   (((...(id . g xn) .  ...  . g x3) . g x2) . g x1)

и, таким образом, он просто делает то, что сделал бы левый сгиб,

zipRev [] ys = []
zipRev [x1, x2, x3, ..., xn] ys 
      = (id . g xn  .  ...  . g x3 . g x2 . g x1)  snd         (ys, [])
      = g xn (g xn1 (  ...  ( g x3 ( g x2 ( g x1   snd)))...)) (ys, [])
   where     ----c--------------------------------------------
        g x  c     (y:ys, r) = c (ys, (x,y):r)

Итак, мы перешли к глубокому концу списка xs, а затем возвращаемся назад, потребляя список ys слева направо (то есть сверху вниз) на обратном пути справа налево на xs список (т.е. снизу вверх). Это просто закодировано как правый сгиб со строгим редуктором, поэтому поток действительно справа налево на xs. Самое нижнее действие (snd) в цепочке выполняется последним, поэтому в новом коде оно становится самым верхним (все еще выполняется последним):

zipRev xs ys = snd (foldr h (ys,[]) xs)
  where
        h x        (y:ys, r) =   (ys, (x,y):r)

g x c использовалось как продолжение в исходном коде, с c как продолжение второго уровня; но на самом деле все это было обычным сгибом справа.

---

Так что, действительно, он переворачивает первый список в обратном порядке со вторым. Это также небезопасно; он пропускает пункт:

        g x  c     ([],   r) = c ([], r)        -- or just `r`
        g x  c     (y:ys, r) = c (ys, (x,y):r)

---

(update:) Ответы duplode (и Joseph Sible) делают лямбда-поднятие немного по-другому, что лучше подходит для этой задачи. Это выглядит так:

zipRev xs ys = foldr f id xs  snd (ys,[])
  where
     f x k c = k      (\((y:ys), r) -> c (ys, (x,y):r)) 
             = k (c . (\((y:ys), r) ->   (ys, (x,y):r)) )
             = k (c . g x)
     g x     =        (\((y:ys), r) ->   (ys, (x,y):r))
  {- f x k c = k ((. g x) c) = (k . (. g x)) c = (. (. g x)) k c
     f x     =                                   (. (. g x))     -}

так тогда

foldr f id  [ x1,            x2,    ... ,         xn      ]  snd  (ys,[]) =
  = ( (. (. g x1)) $ (. (. g x2)) $ ... $ (. (. g xn)) id )  snd  (ys,[])  -- 1,2...n
  = ( id . (. g xn) .  ...  . (. g x2)  .    (. g x1)     )  snd  (ys,[])  -- n...2,1
  =      ( snd . g x1 .    g x2   . ... .       g xn            ) (ys,[])  -- 1,2...n!
  =        snd $ g x1 $    g x2   $ ... $       g xn              (ys,[])
  =        snd $  foldr g (ys,[])  [x1, x2, ...,  xn      ]

Simple. :) Дважды щелкнуть - это совсем не щелкнуть.