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

Я просмотрел 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 чисты, и технически они находятся. Но давайте будем честными: если у вас есть приложение, которое полностью живя в государстве, вы не получаете преимуществ от мутация, которую вы хотите от чистого кода. Можно также назвать вещи своими именами spade, и примите, что у вас есть изменяемая переменная.

Это заставляет меня думать, что это действительно так: с 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)

Ответ 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, и у нее было множество недостатков: хелло-запутанные типы, сложные для реализации экземпляров, невозможные для получения экземпляров, иногда запутанное поведение. Не очень хорошая ситуация.

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 ..., различается, поэтому закон нарушается. Кроме того, наблюдаемые эффекты различны, что тоже не очень.