При каких обстоятельствах монадические вычисления являются хвост-рекурсивными?

В Haskell Wiki Рекурсия в монаде есть пример, который, как утверждается, является хвостом-рекурсивным

f 0 acc = return (reverse acc)
f n acc = do
    v  <- getLine
    f (n-1) (v : acc)

В то время как императивная нотация приводит нас к мысли, что она рекурсивна, она не настолько очевидна вообще (по крайней мере для меня). Если мы де сахара do, получим

f 0 acc = return (reverse acc)
f n acc = getLine >>= \v -> f (n-1) (v : acc)

и переписывание второй строки приводит к

f n acc = (>>=) getLine (\v -> f (n-1) (v : acc))

Итак, мы видим, что f происходит во втором аргументе >>=, а не в хвостовой рекурсивной позиции. Нам нужно изучить IO >>=, чтобы получить ответ. Очевидно, что , имеющий рекурсивный вызов в качестве последней строки в блоке do, не является достаточным условием, чтобы функция была хвосторекурсивной.

Скажем, что монада является хвост-рекурсивной, если каждая рекурсивная функция в этой монаде определяется как

f = do
    ...
    f ...

или эквивалентно

f ...  =  (...) >>= \x -> f ...

является хвостовым рекурсивным. Мой вопрос:

  • Какие монады являются хвостовыми рекурсивными?
  • Есть ли какое-то общее правило, которое мы можем использовать, чтобы сразу отличить хвостовые рекурсивные монады?

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

f 0 acc = acc
f n acc = do
    r <- acc
    f (n - 1) (map (r +) acc)

должен быть хвост-рекурсивным. Однако обессоливание второй линии приводит к

f n acc = acc >>= \r -> f (n - 1) (map (r +) acc)
        = (flip concatMap) acc (\r -> f (n - 1) (map (r +) acc))

Ясно, что это не хвостовая рекурсия, и IMHO не может быть сделано. Причина в том, что рекурсивный вызов не является окончанием вычисления. Он выполняется несколько раз, и результаты объединяются, чтобы сделать окончательный результат.

Ответы

Ответ 1

Монадическое вычисление, которое ссылается на себя, никогда не является хвостовым рекурсивным. Тем не менее, в Haskell у вас есть лень и корекурсия, и это важно. Позвольте использовать этот простой пример:

forever :: (Monad m) => m a -> m b
forever c' = let c = c' >> c in c

Такое вычисление выполняется в постоянном пространстве тогда и только тогда, когда (>>) является нестрогим во втором аргументе. Это действительно очень похоже на списки и repeat:

repeat :: a -> [a]
repeat x = let xs = x : xs in xs

Так как конструктор (:) не является строгим во втором аргументе, это работает, и список может быть пройден, потому что у вас есть конечная слабая головная нормальная форма (WHNF). Пока потребитель (например, сбрасывает список) только когда-либо запрашивает WHNF, это работает и работает в постоянном пространстве.

Потребитель в случае forever - это то, что интерпретирует монадическое вычисление. Если монада [], то (>>) является нестрогим во втором аргументе, когда его первым аргументом является пустой список. Таким образом, forever [] приведет к [], а forever [1] будет расходиться. В случае монады IO интерпретатор является самой самой системой времени выполнения, и вы можете думать, что (>>) всегда не является строгим во втором аргументе.

Ответ 2

Что действительно важно, так это постоянное пространство стека. Ваш первый пример хвост рекурсивный по модулю против, благодаря лени.

(getLine >>=) будет выполнен и испарится, оставив нас снова с вызовом f. Важно то, что это происходит в постоянном количестве шагов - там нет нарастания громкости.

Второй пример,

f 0 acc = acc
f n acc = concat [ f (n - 1) $ map (r +) acc | r <- acc]

будет только линейным (в n) в его нарастании потока, поскольку список результатов будет доступен слева (опять же из-за лени, поскольку concat является нестрогим). Если он потребляется в головке, он может работать в пространстве O (1) (не считая линейного пространства thunk, f(0), f(1), ..., f(n-1) на левом краю).

Намного хуже было бы

f n acc = concat [ f (n-1) $ map (r +) $ f (n-1) acc | r <- acc]

или в do -notation,

f n acc = do
  r <- acc
  f (n-1) $ map (r+) $ f (n-1) acc

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