Понимание сигнатур монадного типа трансформатора

Question

В настоящее время я занимаюсь монадными преобразователями и пытаюсь по-настоящему понять сигнатуры типов, и у меня возникло некоторое замешательство. Давайте использовать следующий стек для обсуждения:

newtype Stack s m a = Stack { runStack :: ReaderT s (StateT s IO) a }

Я пытаюсь пройти слой за слоем и написать развернутые сигнатуры типов, но застреваю:

newtype Stack s m a = Stack { 
    runStack :: ReaderT s         (StateT s IO)       a }
--              ReaderT s                  m          a
--                      s ->               m          a
--                      s ->         (StateT s IO)    a
--                            StateT  s     m         a
--                      s ->         (s -> IO (a, s)) a  

Это просто не похоже на действительную сигнатуру возвращаемого типа в последней строке, у нас есть функция, которая принимает s и возвращает функцию, противостоящую a?

Я получаю , что внутренняя функция в конечном итоге превращается в монаду, и именно поэтому это m в ReaderT r m a, но она изгибает мой мозг.

Может ли кто-нибудь предложить какое-либо понимание, если бы я корректно проанализировал типы, и я просто должен признать, что s -> (s -> IO (a, s)) a действительно действителен?

Спасибо

Answer 1

Стек, который вы написали, немного странный, потому что он параметризован m слева, но специализирован для IO справа, поэтому давайте посмотрим на полностью m -параметризованный вариант:

newtype Stack s m a = Stack { runStack :: ReaderT s (StateT s m) a }

Теперь runStack вот только имя поля, поэтому мы можем отбросить его и написать эквивалентное newtype определение:

newtype Stack s m a = Stack (ReaderT s (StateT s m) a)

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

newtype ReaderT r1 m1 a1 = ReaderT (r1 -> m1 a1)
newtype StateT s2 m2 a2 = StateT (s2 -> m2 (a2, s2))

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

type Stack s m a = ReaderT s (StateT s m) a
type ReaderT r1 m1 a1 = r1 -> m1 a1
type StateT s2 m2 a2 = s2 -> m2 (a2, s2)

Теперь легко расширить тип Stack:

Stack s m a
= ReaderT s (StateT s m) a
-- expand ReaderT with r1=s, m1=StateT s m, a1=a
= s -> (StateT s m) a
= s -> StateT s m a
-- expand StateT with s2=s m2=m a2=a
= s -> (s -> m (a, s))
= s -> s -> m (a, s)

Как заметил @duplode, здесь нет лишних a.

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