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

Рассмотрим следующий пример.

newtype TooBig = TooBig Int deriving Show

choose :: MonadPlus m => [a] -> m a
choose = msum . map return

ex1 :: (MonadPlus m, MonadError TooBig m) => m Int
ex1 = do
    x <- choose [5,7,1]
    if x > 5
        then throwError (TooBig x)
        else return x

ex2 :: (MonadPlus m, MonadError TooBig m) => m Int
ex2 = ex1 `catchError` handler
  where
    handler (TooBig x) = if x > 7
        then throwError (TooBig x)
        else return x

ex3 :: Either TooBig [Int]
ex3 = runIdentity . runExceptT . runListT $ ex2

Каким должно быть значение ex3? Если мы используем MTL, то ответ будет Right [7], что имеет смысл, потому что ex1 завершается, поскольку выдает ошибку, а handler просто возвращает чистое значение return 7, которое равно Right [7].

Однако в статье Олега Киселева и др. . авторы говорят, что это «неожиданный и нежелательный результат». Они ожидали, что результатом будет Right [5,7,1], потому что handler восстанавливается после исключения, не вызывая его повторно. По сути, они ожидали, что catchError будет перемещено в ex1 следующим образом.

newtype TooBig = TooBig Int deriving Show

choose :: MonadPlus m => [a] -> m a
choose = msum . map return

ex1 :: (MonadPlus m, MonadError TooBig m) => m Int
ex1 = do
    x <- choose [5,7,1]
    if x > 5
        then throwError (TooBig x) `catchError` handler
        else return x
  where
    handler (TooBig x) = if x > 7
        then throwError (TooBig x)
        else return x

ex3 :: Either TooBig [Int]
ex3 = runIdentity . runExceptT . runListT $ ex1

Именно это и делают расширяемые эффекты. Они изменяют семантику программы, перемещая обработчики эффектов ближе к источнику эффекта. Например, local перемещается ближе к ask, а catchError перемещается ближе к throwError. Авторы статьи рекламируют это как одно из преимуществ расширяемых эффектов перед монадными преобразователями, утверждая, что монадные преобразователи обладают «негибкой семантикой».

Но что, если я по какой-то причине хочу, чтобы результат был Right [7] вместо Right [5,7,1]? Как показано в приведенных выше примерах, преобразователи монад могут использоваться для получения обоих результатов. Однако, поскольку расширяемые эффекты всегда перемещают обработчики эффектов ближе к источнику эффекта, кажется невозможным получить результат Right [7].

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


functional-programming haskell monads monad-transformers free-monad
person Aadit M Shah    schedule 06.01.2021    source источник

Ответы (1)


arrow_upward
5
arrow_downward

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

Подход MTL в каком-то смысле наиболее очевиден и универсален: у вас есть интерфейс (или эффект), вы помещаете его в класс типов и заканчиваете. Цена этой общности заключается в том, что она беспринципна: вы не знаете, что происходит, когда вы объединяете интерфейсы вместе. Эта проблема проявляется наиболее конкретно, когда вы реализуете интерфейс: вы должны реализовать их все одновременно. Нам нравится думать, что каждый интерфейс может быть реализован изолированно в выделенном преобразователе, но если у вас есть два интерфейса, скажем, MonadPlus и MonadError, реализованные преобразователями ListT и ExceptT, чтобы скомпоновать их, вам также придется либо реализовать MonadError для ListT или MonadPlus для ExceptT. Эта проблема экземпляра O (n ^ 2) обычно понимается как просто шаблон, но более глубокая проблема заключается в том, что если мы позволим интерфейсам иметь любую форму, невозможно сказать, какая опасность может скрываться в этом шаблоне, если это вообще можно реализовать вообще.

Мы должны сделать эти интерфейсы более структурированными. Для некоторого определения подъемной силы (lift из MonadTrans) эффекты, которые мы можем равномерно поднять с помощью трансформаторов, являются в точности алгебраическими эффектами. (См. также Монадные преобразователи и модульные алгебраические эффекты, что их связывает< /а>.)

Это не совсем ограничение. Хотя некоторые интерфейсы не являются алгебраическими в техническом смысле, например MonadError (из-за catch), их обычно все же можно выразить в рамках алгебраических эффектов, только менее буквально. Ограничивая определение интерфейса, мы также получаем более богатые способы их использования.

Так что я думаю, что алгебраические эффекты — это другой, более точный способ думать об интерфейсах прежде всего. Таким образом, как способ мышления, его можно принять, ничего не меняя в вашем коде, поэтому сравнения, как правило, рассматривают один и тот же код дважды, и трудно увидеть суть, не понимая окружающий контекст и мотивы. Если вы думаете, что проблема O(n^2) экземпляров является тривиальной проблемой шаблонного шаблона, вы уже верите в принцип, согласно которому интерфейсы должны быть компонуемыми; алгебраические эффекты — это один из способов явного проектирования библиотек и языков на основе этого принципа.

Алгебраические эффекты — это расплывчатое понятие без фиксированного определения. В настоящее время они наиболее узнаваемы по синтаксису с конструкцией call и handle (или op/perform/throw/raise и catch/match). call — это единственная конструкция для использования интерфейсов, а handle — это то, как мы их реализуем. Идея, общая для таких языков, заключается в том, что существуют уравнения (следовательно, алгебраические), которые обеспечивают базовую интуицию того, как call и handle ведут себя независимо от интерфейса, в частности, посредством взаимодействия handle с последовательной композицией (>>=).

Семантически смысл программы можно обозначить деревом calls, а handle является преобразованием таких деревьев. Вот почему многие воплощения алгебраических эффектов в Haskell начинаются со свободных монад, типов деревьев, параметризованных типом узлов f:

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

С этой точки зрения программа ex2 представляет собой дерево с тремя ветвями, причем ветвь с номером 7 заканчивается исключением:

ex2 :: Free ([] :+: Const Int) Int  -- The functor "Const e" models exceptions (the equivalent of "MonadError e")
ex2 = Free [Pure 5, Free (Const 7), Pure 1]
-- You can write this with do notation to look like the original ex2, I'd say "it's just notation".
-- NB: constructors for (:+:) omitted

И каждый из эффектов [] и Const Int соответствует некоторому способу преобразования дерева, устранению этого эффекта из дерева (возможно, введению других, включая себя самого).

  • Перехват исключения соответствует обработке эффекта Const путем преобразования Free (Const x) узлов в некоторое новое дерево h x.

  • Одним из способов обработки эффекта [] является составление всех дочерних элементов узла Free [...] с использованием (>>=), собирая их результаты в окончательный список. Это можно рассматривать как обобщение поиска в глубину.

Вы получите результат [7] или [5,7,1] в зависимости от того, как упорядочены эти преобразования.

Конечно, есть соответствие двум порядкам монадных преобразователей в подходе MTL, но интуиция программ как деревьев, которая обычно применима ко всем алгебраическим эффектам, не так очевидна, когда вы находитесь в середине реализации. например, MonadError e для ListT. Эта интуиция может иметь смысл апостериорно, но она априори запутана, поскольку экземпляры классов типов не являются первоклассными значениями, как обработчики, а преобразователи монад обычно выражаются в терминах окончательная интерпретация (скрытая в m монаде, которую они трансформируют) вместо исходного синтаксиса.

person Li-yao Xia    schedule 07.01.2021