Тип Переменная Расположение в Трансформаторах

Question

Рассмотрим State тип - или хотя бы упрощенная версия:

newtype State s a = State { runState :: s -> (a, s) }

Теперь, скажем, мы хотим получить StateT монадный трансформатор. transformers определяет это следующим образом:

newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }

Здесь m был размещен справа от стрелки функции, но вне кортежа. Однако, если мы не знали правильный ответ, мы могли бы вместо этого поставить m где-нибудь еще:

newtype StateT s m a = StateT { runStateT :: m (s -> (  a,  s)) }
newtype StateT s m a = StateT { runStateT ::    s -> (m a,  s)  }

Очевидно, что версия в transformers правильно, но почему? В более общем смысле, как узнать, куда поместить переменную типа для "внутренней" монады при определении преобразователя монад? Обобщая еще больше, есть ли подобное правило для comonad трансформаторов?

Answer 1

Я думаю, что разницу можно легко понять, когда m ~ IO:

s -> IO (a, s)

тип действия, которое может прочитать текущее состояние sвыполнить IO в зависимости от этого (например, распечатать текущее состояние, прочитать строку от пользователя), а затем произвести оба новых состояния sи возвращаемое значение a,

Вместо:

IO (s -> (a, s))

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

Это похоже на предыдущий тип, поскольку новое состояние и возвращаемое значение могут зависеть как от предыдущего состояния, так и от ввода-вывода. Однако ввод-вывод не может зависеть от текущего состояния: например, печать текущего состояния запрещена.

Вместо,

s -> (IO a,  s)

тип действия, которое читает текущее состояние sи затем выполняет ввод-вывод в зависимости от этого (например, печать текущего состояния, чтение строки от пользователя), а затем производит возвращаемое значение a, Зависит от текущего состояния, бот не от ввода-вывода, создается новое состояние. Этот тип эффективно изоморфен паре функций (s -> IO a, s -> s),

Здесь IO может прочитать строку от пользователя и вывести возвращаемое значение a в зависимости от этого, но новое состояние не может зависеть от этой линии.

Поскольку первый вариант является более общим, мы хотим, чтобы он был нашим преобразователем состояния.

Я не думаю, что есть "общее правило" для решения, куда поставить m: это зависит от того, чего мы хотим достичь.