Как понять требование MonadUnliftIO о том, что «монады без состояния» не нужны?

Question

Я просмотрел https://www.fpcomplete.com/blog/2017/06/tale-of-two-brackets,, хотя просматривал некоторые части, и до сих пор не совсем понимаю основную проблему "StateT - это плохо, IO - это нормально", за исключением смутного пониманиячто Haskell позволяет писать плохие StateT монады (или, как мне кажется, в конечном итоге в статье MonadBaseControl вместо StateT).

В пикшах должен соблюдаться следующий закон:

askUnliftIO >>= (\u -> liftIO (unliftIO u m)) = m

Таким образом, это говорит о том, что состояние не изменяется в монаде m при использовании askUnliftIO.Но, на мой взгляд, в IO весь мир может быть государством.Я мог бы, например, читать и писать в текстовый файл на диске.

Цитировать еще одну статью Майкла ,

Ложная чистота Мы говорим WriterT иStateT чисты, и технически они есть.Но давайте будем честными: если у вас есть приложение, которое полностью живет в StateT, вы не получите тех преимуществ сдержанной мутации, которые вам нужны от чистого кода.Можно также назвать вещи своими именами и признать, что у вас есть изменяемая переменная.

Это заставляет меня думать, что это действительно так: с IO мы честны, с StateT мыне честны в отношении изменчивости ... но это кажется другой проблемой, чем то, что пытается показать закон вышев конце концов, MonadUnliftIO предполагает IO.У меня возникают проблемы с концептуальным пониманием того, как IO является более строгим, чем что-либо еще.

Обновление 1

После сна (некоторые) я все еще смущен, но япостепенно становится все меньше с течением дня.Я разработал законное доказательство для IO.Я понял наличие id в README.В частности,

instance MonadUnliftIO IO where
  askUnliftIO = return (UnliftIO id)

Таким образом, askUnliftIO, по-видимому, возвращает IO (IO a) на UnliftIO m.

Prelude> fooIO = print 5
Prelude> :t fooIO
fooIO :: IO ()
Prelude> let barIO :: IO(IO ()); barIO = return fooIO
Prelude> :t barIO
barIO :: IO (IO ())

Возвращаясь к закону, он действительно говоритэто состояние не видоизменяется в монаде m при выполнении туда-обратно преобразованной монады (askUnliftIO), где в оба конца входит unLiftIO -> liftIO.

Возобновление примера выше, barIO :: IO (), так что если мы сделаем barIO >>= (u -> liftIO (unliftIO u m)), то u :: IO () и unliftIO u == IO (), затем liftIO (IO ()) == IO ().** Таким образом, поскольку все в основном были приложения id под капотом, мы можем видеть, что ни одно состояние не было изменено, даже если мы используем IO.Важно отметить, что важно то, что значение в a никогда не запускается и никакое другое состояние не изменяется в результате использования askUnliftIO.Если это так, то, как и в случае randomIO :: IO a, мы не сможем получить то же значение, если бы не запустили askUnliftIO.(Попытка проверки 1 ниже)

Но все равно кажется, что мы могли бы сделать то же самое для других монад, даже если они поддерживают состояние.Но я также вижу, что для некоторых монад мы не можем этого сделать.Думая о надуманном примере: каждый раз, когда мы получаем доступ к значению типа a, содержащемуся в монаде с состоянием, некоторое внутреннее состояние изменяется.

Попытка проверки 1

> fooIO >> askUnliftIO
5
> fooIOunlift = fooIO >> askUnliftIO
> :t fooIOunlift
fooIOunlift :: IO (UnliftIO IO)
> fooIOunlift
5

Пока хорошо, но не совсем понятно, почему происходит следующее:

 > fooIOunlift >>= (\u -> unliftIO u)

<interactive>:50:24: error:
    * Couldn't match expected type `IO b'
                  with actual type `IO a0 -> IO a0'
    * Probable cause: `unliftIO' is applied to too few arguments
      In the expression: unliftIO u
      In the second argument of `(>>=)', namely `(\ u -> unliftIO u)'
      In the expression: fooIOunlift >>= (\ u -> unliftIO u)
    * Relevant bindings include
        it :: IO b (bound at <interactive>:50:1)

Answer 1

«StateT - это плохо, IO в порядке»

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

finally :: StateT s IO a -> StateT s IO a -> StateT s IO a является отличным примером.Если вы используете «StateT - присоединяет изменяемую переменную типа s к метафоре монады m», то вы можете ожидать, что действие финализатора получит доступ к самому последнему значению s при возникновении исключения.

forkState :: StateT s IO a -> StateT s IO ThreadId еще один.Вы можете ожидать, что изменения состояния от ввода будут отражены в исходном потоке.

lol :: StateT Int IO [ThreadId]
lol = do
  for [1..10] $ \i -> do
    forkState $ modify (+i)

Вы можете ожидать, что lol можно переписать (по модулю производительности) как modify (+ sum [1..10]).Но это не правильно.Реализация forkState просто передает начальное состояние разветвленному потоку, и тогда никогда не сможет получить какие-либо изменения состояния .Простое / общее понимание StateT вас здесь не устраивает.

Вместо этого вы должны принять более детализированное представление StateT s m a как «преобразователь, который предоставляет локальную для потока неизменяемую переменную типа sкоторый неявно пронизывается через вычисление, и можно заменить эту локальную переменную новым значением того же типа для будущих этапов вычисления. "(более или менее подробный английский пересказ s -> m (a, s)). При таком понимании поведение finally становится немного более понятным: это локальная переменная, поэтому она не переживает исключений.Аналогично, forkState становится более понятным: это локальная переменная потока, поэтому очевидно, что изменение другого потока не повлияет на другие.

Это иногда , что вы хотите.Но обычно это не то, как люди пишут код IRL, и это часто смущает людей.

В течение долгого времени в экосистеме по умолчанию выбирали эту операцию "понижения", равную MonadBaseControl, и это имело кучуНедостатки: hella запутанные типы, трудно реализовать экземпляры, невозможно получить экземпляры, иногда запутанное поведение.Непростая ситуация.

MonadUnliftIO ограничивает вещи более простым набором монадных преобразователей и может обеспечить относительно простые типы, производные экземпляры и всегда предсказуемое поведение.Цена заключается в том, что трансформаторы ExceptT, StateT и т. Д. Не могут его использовать.

Основополагающий принцип заключается в следующем: ограничивая то, что возможно, мы облегчаем понимание того, что может произойти.MonadBaseControl чрезвычайно мощный и общий, и в результате довольно сложный в использовании и запутывающий.MonadUnliftIO менее мощный и общий, но его гораздо проще использовать.

Таким образом, это говорит о том, что состояние не изменяется в монаде m при использовании askUnliftIO.

Это не так - закон гласит, что unliftIO не должен ничего делать с трансформатором монады, кроме как снизить его до IO.Вот что нарушает этот закон:

newtype WithInt a = WithInt (ReaderT Int IO a)
  deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader Int)

instance MonadUnliftIO WithInt where
  askUnliftIO = pure (UnliftIO (\(WithInt readerAction) -> runReaderT 0 readerAction))

Давайте проверим, что это нарушает данный закон: askUnliftIO >>= (\u -> liftIO (unliftIO u m)) = m.

test :: WithInt Int
test = do
  int <- ask
  print int
  pure int

checkLaw :: WithInt ()
checkLaw = do
  first <- test
  second <- askUnliftIO >>= (\u -> liftIO (unliftIO u test))
  when (first /= second) $
    putStrLn "Law violation!!!"

Значение, возвращаемое test и askUnliftIO ...Понижение / подъем разные, поэтому закон нарушен.Кроме того, наблюдаемые эффекты различны, что тоже не очень.