Как написать эту более общую версию `Control.Monad.Writer.censor`?

Стандарт Control.Monad.Writer.censor является двойным стандарту Control.Monad.Reader.local, при censor изменении состояния записи после вычисления и local изменения состояния считывателя перед вычислением:

censor :: (w -> w) -> Writer w a -> Writer w a
local  :: (r -> r) -> Reader r a -> Reader r a

Однако монады Reader и Writer не полностью симметричны. А именно, вычисление писателя дает результат в дополнение к писательскому состоянию, и я пытаюсь написать альтернативу версии censor, которая использует эту асимметрию. я хочу написать функцию

censorWithResult :: (a -> w -> w) -> Writer w a -> Writer w a

который принимает трансформатор типа a -> w -> w, который получает результат вычисления в дополнение к состоянию записи. Я не см., как записать эту функцию, используя tell, listen и pass.

Точное поведение, которое я ожидаю от censorWithResult, состоит в том, что если

ma :: Writer w a
f  :: a -> w -> w

и

runWriter ma = (r , y)

затем

runWriter (censorWithResult f ma) = (r , f r y)

тогда

runWriter (censor g ma) = (r , g y)

когда g :: w -> w.

Пример

Это не обязательно для понимания вопроса, но здесь упрощенная версия мотивирующего примера:

import Control.Applicative
import Control.Monad.Writer

-- Call-trace data type for functions from 'Int' to 'Int'.
--
-- A 'Call x subs r' is for a call with argument 'x', sub calls
-- 'subs', and result 'r'.
data Trace = Call Int Forest Int
type Forest = [Trace]

-- A writer monad for capturing call traces.
type M a = Writer Forest a

-- Recursive traced negation function.
--
-- E.g. we expect that
--
--   runWriter (t 2) = (-2 , Call 2 [Call 1 [Call 0 [] 0] -1] -2)
t , n :: Int -> M Int
t x = trace n x
n x = if x <= 0 then pure 0 else subtract 1 <$> t (x - 1)

trace :: (Int -> M Int) -> (Int -> M Int)
trace h x = do
  censorWithResult (\r subs -> [Call x subs r]) (h x)

-- The idea is that if 'ma :: Writer w a' and 'runWriter ma = (r , y)'
-- then 'runWriter (censorWithResult f ma) = (r , f r y)'. I.e.,
-- 'censorWithResult' is like 'Control.Monad.Writer.censor', except it
-- has access to the result of the 'Writer' computation, in addition
-- to the written data.
censorWithResult :: (a -> w -> w) -> Writer w a -> Writer w a
censorWithResult = undefined

Ответ 1

Если нам разрешено использовать только tell, pass и listen, единственная функция, которая имеет доступ к выходу, это

-- | `pass m` is an action that executes the action `m`, which returns a value
-- and a function, and returns the value, applying the function to the output. 
pass :: (MonadWriter w m) => m (a, w -> w) -> m a

Итак, для censorWithResult нам нужно частично применить заданную функцию типа a -> w -> w, чтобы получить w -> w и обработать ее до pass. Это может быть выполнено как

censorWithResult :: (MonadWriter w m) => (a -> w -> w) -> m a -> m a
censorWithResult f m = pass $ do
    a <- m
    return (a, f a)

Действие внутри pass выполняет данное действие, частично применяет к нему f, а pass затем соответствующим образом изменяет выход.

Ответ 2

Точное поведение, которое я ожидаю от censorWithResult, заключается в том, что если
ma :: Writer w a
f  :: a -> w -> w
и
runWriter ma = (r , y)
затем
runWriter (censorWithResult f ma) = (r , f r y)

Хорошо, тогда сделаем это. Единственное, что вам нужно знать, это то, что writer является левым обратным для runWriter. Затем мы получаем следующую цепочку равенств, сначала с помощью writer с обеих сторон, затем путем исключения левого обратного.

        runWriter (censorWithResult f ma)  =        (r, f r y)
writer (runWriter (censorWithResult f ma)) = writer (r, f r y)
                   censorWithResult f ma   = writer (r, f r y)

Единственное, что нам нужно сделать, это подключить ваше уравнение runWriter ma = (r, y):

censorWithResult f ma = let (r, y) = runWriter ma in writer (r, f r y)

Не является ли эквациональное рассуждение грандиозным?