Есть ли монада, у которой нет соответствующего монадного трансформатора (кроме IO)?

Question

До сих пор каждая монада (которая может быть представлена ​​как тип данных), с которой я столкнулся, имела соответствующий монадный преобразователь или могла иметь его. Есть ли такая монада, которая не может иметь ее? Или у всех монад есть соответствующий трансформатор?

Трансформатором t соответствует монаде m я имею в виду, что t Identity изоморфен m, И, конечно же, он удовлетворяет законам монадного трансформатора и t n это монада для любой монады n,

Я хотел бы увидеть либо доказательство (в идеале конструктивное), что у каждой монады есть такая, либо пример конкретной монады, у которой ее нет (с доказательством). Меня интересуют как более ориентированные на Хаскелл ответы, так и теоретические (категории).

Как дополнительный вопрос, есть ли монада m который имеет два разных трансформатора t1 а также t2? То есть, t1 Identity изоморфен t2 Identity и к m но есть монада n такой, что t1 n не изоморфен t2 n,

(IO а также ST У меня особая семантика, поэтому я не принимаю их здесь во внимание, и давайте полностью их игнорируем. Давайте сосредоточимся только на "чистых" монадах, которые могут быть построены с использованием типов данных.)

Answer 1

Я с @Rhymoid на этом, я думаю, что у всех монад есть два (!!) трансформатора. Моя конструкция немного отличается и гораздо менее завершена. Я хотел бы иметь возможность взять этот набросок в качестве доказательства, но я думаю, что я либо скучаю по навыкам / интуиции и / или это может быть довольно сложным.

Благодаря Клейсли каждая монада (m) можно разложить на два функтора F_k а также G_k такой, что F_k оставлен присоединенным к G_k и это m изоморфен G_k * F_k (Вот * это функторная композиция). Кроме того, из-за присоединения, F_k * G_k образует комонаду.

Я утверждаю что t_mk определяется так, что t_mk n = G_k * n * F_k это монадный трансформатор. Очевидно, что t_mk Id = G_k * Id * F_k = G_k * F_k = m, определяющий return для этого функтора не сложно, т.к. F_k является "остроконечным" функтором и определяющим join должно быть возможно, так как extract от комонады F_k * G_k может использоваться для уменьшения значений типа (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a к значениям типа G_k * n * n * F_k, который затем дополнительно уменьшается с помощью join от n,

Мы должны быть немного осторожны, так как F_k а также G_k не являются эндофункторами на Hask. Таким образом, они не являются экземплярами стандарта Functor класс типов, а также не может быть напрямую n как показано выше. Вместо этого мы должны "проектировать" n в категорию Клейсли до композиции, но я считаю, return от m обеспечивает эту "проекцию".

Я считаю, что вы также можете сделать это с разложением монады Эйленберга-Мура, давая m = G_em * F_em, tm_em n = G_em * n * F_emи аналогичные конструкции для lift, return, а также join с аналогичной зависимостью от extract от комонады F_em * G_em,

Answer 2

Вот волнообразный ответ, который я не совсем уверен.

Монады можно рассматривать как интерфейс императивных языков. return это то, как вы вводите чистую ценность в язык, и >>= это то, как вы соединяете части языка вместе. Законы Монады гарантируют, что "рефакторинг" частей языка работает так, как вы ожидаете. Любые дополнительные действия, предоставляемые монадой, могут рассматриваться как ее "операции".

Монадные Трансформеры являются одним из способов решения проблемы "расширяемых эффектов". Если у нас есть монадный трансформатор t который превращает монаду mТогда мы могли бы сказать, что язык m расширяется за счет дополнительных операций, доступных через t, Identity монада это язык без эффектов / операций, поэтому применение t в Identity просто получит вам язык только с операциями, предоставленными t,

Поэтому, если мы думаем о Monads с точки зрения модели "инжектирование, слияние и другие операции", то мы можем просто переформулировать их, используя Free Monad Transformer. Таким образом, даже монаду IO можно превратить в трансформер. Единственный улов в том, что вам, вероятно, нужен какой-то способ снять этот слой со стека трансформаторов в какой-то момент, и единственный разумный способ сделать это, если у вас есть IO в нижней части стека, так что вы можете просто выполнять операции там.

Answer 3

1. Я думаю, что нашел по крайней мере один контрпример: простую и явную монаду, которая не имеет простого и явного преобразователя монад.

Конструктор типа монады L для этого контрпример определяется

  type L z a  = Either a (z -> a)

Цель этой монады - украсить монаду обычного читателя. z -> a с явным pure значение (Left x). Рядовой читатель монада pure значение является постоянной функцией pure x = _ -> x, Однако, если нам дано значение типа z -> aмы не сможем определить, является ли это значение постоянной функцией. С L z a, pure значение представляется явно как Left x, Теперь пользователи могут сравнивать L z a и определить, является ли данное монадическое значение чистым или имеет эффект. Кроме этого, монада L z делает то же самое, что и читатель монада.

Экземпляр монады:

  instance Monad (L z) where
     return x = Left x
     (Left x) >>= f = f x
     (Right q) >>= f = Right(join merged) where
        join :: (z -> z -> r) -> z -> r
        join f x = f x x -- the standard `join` for Reader monad
        merged :: z -> z -> r
        merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
        merge :: Either a (z -> a) -> z -> a 
        merge (Left x) _ = x
        merge (Right p) z = p z

Эта монада L z является частным случаем более общей конструкции, (Monad m) => Monad (L m) где L m a = Either a (m a), Эта конструкция украшает данную монаду m добавив явный pure значение (Left x), так что теперь пользователи могут сравнивать L m решить, является ли ценность чистой. В остальном, L m представляет тот же вычислительный эффект, что и монада m,

Экземпляр монады для L m почти такой же, как в примере выше, за исключением join а также fmap монады m нужно использовать и вспомогательную функцию merge определяется

    merge :: Either a (m a) -> m a
    merge (Left x) = return @m x
    merge (Right p) = p

Я проверил, что законы монады L m с произвольной монадой m,

Я так думаю L m не имеет монадный трансформатор, либо для общего m или даже для простой монады m = Reader, Достаточно рассмотреть L z как определено выше; даже эта простая монада, похоже, не имеет трансформатора.

(Эвристическая) причина отсутствия монадного трансформатора состоит в том, что эта монада имеет Reader внутри Either, Either монадный трансформер нуждается в том, чтобы его базовая монада была составлена ​​внутри внешней монады, EitherT e m a = m (Either e a)потому что монадный трансформатор работает с использованием обхода. Похоже, что любая монада, которая содержит Either в его типе данных потребуется обход для работы монадного преобразователя, поэтому в преобразователе должна быть "внутренняя" композиция. Тем не менее Reader монадный трансформер нуждается в том, чтобы его базовая монада была составлена вне внешней монады, ReaderT r m a = r -> m a, Монада L представляет собой композицию типа данных, которая требует составного внутреннего преобразователя и монады, которая требует составного внешнего преобразователя, а вторая монада находится внутри первого, что невозможно согласовать. Независимо от того, как мы пытаемся определить L-трансформатор LTКажется, что мы не можем удовлетворить законы монадных трансформаторов.

Одна возможность определения конструктора типа LT было бы LT z m a = Either a (z -> m a), Результатом является законная монада, но морфизм m a -> LT z m a не сохраняет m"s return так как return x отображается в Right (\z -> return x)который не является L"s return (всегда Left x).

Другая возможность LT z m a = z -> Either a (m a), В результате получается монада, но опять же m"s return отображается в \_ -> Right (...) вместо Left (...) как требуется для монады z -> Either a (m a),

Еще одна возможность объединения доступных конструкторов типов LT z m a = Either a (m (z -> a) ), но это не монада для произвольной монады m,

Я не уверен, как строго доказать, что L не имеет монадного преобразователя, но нет комбинации конструкторов типов Either, ->, а также m Кажется, работает правильно.

Итак, монада L z и вообще монады вида L m похоже, нет простого и удобного в использовании монадного преобразователя, который был бы явным конструктором типа (комбинация Either, -> а также m).

2. Другой пример монады, которая, кажется, не имеет явного монадного преобразователя:

type S a = (a -> Bool) -> Maybe a

Эта монада появилась здесь в контексте "поисковых монад". В работе Жюля Хеджеса также упоминается поисковая монада и, в более общем смысле, "выборочные" монады вида

 type Sq n q a = (a -> n q) -> n a

для данной монадыnи фиксированный типq, Приведенная выше поисковая монада является частным случаем монады выбора с n a = Maybe a а также q = (), Тем не менее, статья Хеджеса (на мой взгляд, неправильно) утверждает, что Sq является монадой трансформатором для монады (a -> q) -> a,

Мое мнение таково, что монада(a -> q) -> aимеет монадный трансформатор(m a -> q) -> m aтипа "составлено снаружи". Это связано со свойством "жесткости", исследованным в вопросе. Является ли это свойство функтора более сильным, чем монада? А именно, (a -> q) -> aявляется жесткой монадой, и все жесткие монады имеют монадные трансформаторы типа "составной снаружи".

Тем не мение,(a -> n q) -> n aне жесткая, если только монадаnжесткая. Поскольку не все монады жесткие (например, Maybe а также Cont не жесткие), монада (a -> n q) -> n a не будет иметь монадный трансформатор типа "составной снаружи", (m a -> n q) -> n (m a), Также у него не будет "составного" трансформатора, m((a -> n q) -> n a) - это не монада для произвольной монады m; принимать m = Maybe для контрпример. Тип (a -> m (n q)) -> m (n a)аналогично не является монадой для произвольных монад m а также n, Тип m(a -> n q) -> n a это монада для любого mно не допускает подъема m a -> m (a -> n q) -> n a потому что мы не можем вычислить значение n a учитывая только некоторые значения, заключенные в произвольную монаду m,

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

Вот эвристический аргумент в пользу несуществования монадного преобразователя. Если бы существовало определение типа данных для монадного преобразователя(a -> n q) -> n aэто работает для всех монадn, что определение типа данных дало бы "составной снаружи" преобразователь для жесткого n и какой-то другой трансформатор для нежестких n, Но такой выбор невозможен для выражения типа, которое использует n естественно и параметрически (то есть как конструктор непрозрачного типа с экземпляром монады).

3. Как правило, трансформированные монады сами не обладают монадным трансформером. То есть, как только мы возьмем какую-то иностранную монадуmи применить какой-то монадный трансформаторtк нему мы получаем новую монаду t m и эта монада не имеет трансформатора: дана новая иностранная монада n мы не знаем как преобразовать nс монадой t m, Если мы знаем трансформатор mt для монады mмы можем сначала преобразовать n с mtа затем преобразовать результат с t, Но если у нас нет трансформатора для монады m мы застряли: нет конструкции, которая создает трансформатор для монады t mиз знания tодин и работает для произвольных иностранных монад m,

4. Ответ @JamesCandy предполагает, чтодля любой монады(в том числе IO?!), можно написать (общее, но сложное) выражение типа, представляющее соответствующий монадный преобразователь. А именно, вам сначала нужно закодировать Church тип вашего монады, который делает тип похожим на монаду продолжения, а затем определить его преобразователь монад, как будто для монады продолжения. Но я думаю, что это неправильно - это не дает рецепт для производства монадного трансформатора в целом.

Взятие церковного кодирования типаaозначает записать тип

 type ca = forall r. (a -> r) -> r

Этот типcaполностью изоморфенaпо лемме Йонеды. До сих пор мы не достигли ничего, кроме того, что сделали тип намного более сложным, введя количественный параметр типа forall r,

Теперь давайте закодируем церковную базовую монадуL:

 type CL a = forall r. (L a -> r) -> r

Опять же, мы ничего не достигли до сих пор, так какCL aполностью эквивалентноL a,

Теперь представьте на секунду, чтоCL aмонаду продолжения (что не так!) и запишите монадный преобразователь, как если бы он был монадой продолжения, заменив тип результатаrчерез m r:

 type TCL m a = forall r. (L a -> m r) -> m r

Утверждается, что это "церковно-закодированный монадный трансформатор" дляL, Но это кажется неправильным. Нам нужно проверить свойства:

• TCL mявляется законной монадой для любой иностранной монадыmи для любой базовой монадыL
• m a -> TCL m aзаконный монадический морфизм

Второе свойство имеет место, но я считаю, что первое свойство не работает, - другими словами,TCL mне является монадой для произвольной монадыm, Возможно, некоторые монады m признай это, а другие нет. Я не смог найти общий экземпляр монады для TCL mсоответствует произвольной базовой монаде L,

Еще один способ утверждать, чтоTCL mне вообще монада стоит отметить чтоforall r. (a -> m r) -> m rдействительно является монадой для любого конструктора типа m, Обозначим эту монаду CM, Сейчас, TCL m a = CM (L a), Если TCL mбыла бы монада, это означало бы, что CMможет быть составлен с любой монадой L и дает законную монаду CM (L a), Однако маловероятно, что нетривиальная монада CM (в частности, тот, который не эквивалентен Reader) буду сочинять со всеми монадами L, Монады обычно не сочиняют без строгих дополнительных ограничений.

Конкретный пример, где это не работает, для читателей монад. РассматриватьL a = r -> aа такжеm a = s -> aгде r а также s некоторые фиксированные типы. Теперь мы хотели бы рассмотреть "Церковно-закодированный монадный трансформатор" forall t. (L a -> m t) -> m t, Мы можем упростить выражение этого типа, используя лемму Йонеды,

 forall t. (x -> t) -> Q t  = Q x

(для любого функтораQ) и получить

 forall t. (L a -> s -> t) -> s -> t
 = forall t. ((L a, s) -> t) -> s -> t
 = s -> (L a, s)
 = s -> (r -> a, s)

Так что это типовое выражение дляTCL m aв этом случае. ЕслиTCLбыли монадой трансформатором тогда P a = s -> (r -> a, s) будет монадой. Но можно явно проверить, что это P на самом деле не монада (нельзя реализовать return а также bind которые удовлетворяют законам).

Даже если это сработало (т.е.если предположить, что я допустил ошибку, заявив, чтоTCL mэто вообще не монада) эта конструкция имеет определенные недостатки:

• Он не является функториальным (т.е. не ковариантным) по отношению к иностранной монаде mпоэтому мы не можем делать такие вещи, как интерпретировать преобразованную свободную монаду в другую монаду или объединить два монадных преобразователя, как объяснено здесь. Существует ли принципиальный способ составления двух монадных преобразователей, если они разного типа, но лежащая в их основе монада того же типа??
• Наличие forall r делает тип довольно сложным для рассуждений и может привести к снижению производительности (см. статью "Кодирование Церковью считается опасным") и переполнению стека (поскольку кодирование Церковью обычно небезопасно для стека)
• Церковно-закодированный преобразователь монад для базовой монады (L = Id) не дает неизменной иностранной монады: T m a = forall r. (a -> m r) -> m r и это не то же самое, что m a, На самом деле, довольно сложно понять, что это за монада, учитывая монаду. m,

В качестве примера, показывающего, почему forall r затрудняет рассуждение, рассмотрим иностранную монаду m a = Maybe a и попытаться понять, что тип forall r. (a -> Maybe r) -> Maybe r на самом деле означает. Я не смог упростить этот тип или найти хорошее объяснение того, что этот тип делает, то есть, какой "эффект" он представляет (так как это монада, он должен представлять какой-то "эффект") и как можно было бы использовать такой тип.

• Кодированный Церковью монадный трансформатор не эквивалентен стандартным хорошо известным монадным трансформаторам, таким как ReaderT, WriterT, EitherT, StateT и так далее.

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

Answer 4

Мое решение использует логическую структуру терминов Haskell. Всем известно, что функцию в Haskell с типом возврата t можно превратить в монадическую функцию с типом возврата (Monad m) => m t. Следовательно, если функция "связать" могла бы соответствующим образом "монодифицировать" свой программный текст, результатом был бы преобразователь монад.

Камнем преткновения является то, что нет никаких причин, по которым "монадификация" оператора "связывания" должна удовлетворять законам, в частности ассоциативности. Вот тут-то и возникает исключение среза. Теорема об исключении среза влияет на программный текст, заключающий в себе все привязки, анализ случаев и приложения. Кроме того, все вычисления для конкретного термина выполняются в одном месте.

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

Это действительно шерстяное, вот пример. Рассмотрим следующую строгую монаду списка:

rseq x y = case x of
    x:xs -> (x:xs) : y
    [] -> [] : y


evalList (x:xs) = rseq x (evalList xs)
evalList [] = []

instance Monad [] where
    return x = [x]
    ls >>= f = concat (evalList (map f ls))

Этот порядок оценки приводит к стандартному ListT (на самом деле не монада). Тем не менее, путем устранения сокращения:

instance Monad [] where
    return x = [x]
    ls >>= f = case ls of
        [] -> []
        x:xs -> case f x of
            y:ys -> (y:ys) ++ (xs >>= f)
            [] -> [] ++ (xs >>= f)

Это обеспечивает точный порядок оценки, подлежащий "монадификации".

---

В ответ Петру Пудлаку:

Если тип рассматриваемой монады - это некоторый тип функции (это удобно для кодирования по Чёрчу всех типов данных), то тип функции конвертируется путем украшения всех возвращаемых значений типа преобразованной монадой. Это типовая часть монадификации. Часть значения монадификации поднимает чистые функции, используя "возврат", и комбинирует их с использованием жителей типа монады, используя "связывание", сохраняя порядок оценки исходного текста программы.

Монада строгого списка приведена в качестве примера порядка оценки, который не составляется ассоциативно, о чем свидетельствует тот факт, что ListT использует тот же порядок оценки, что и монада строгого списка.

Чтобы завершить пример, церковная кодировка монады списка:

data List a = List (forall b. b -> (a -> List a -> b) -> b)

Monadified, это становится:

data ListT m a = ListT (forall b. m b -> (a -> List a -> m b) -> m b)

cons x xs = \_ f -> f x xs

nil = \x _ -> x

instance (Monad m) => Monad (ListT m) where
    return x = cons x nil
    ls >>= f = ls nil (\x xs -> f x >>= \g ->
        g (liftM (nil ++) (xs >>= f)) (\y ys -> liftM (cons y ys ++) (xs >>= f))

Чтобы пояснить вышеизложенное, на этапе исключения выреза все значения потребляются с использованием дисциплины стека, гарантируя, что порядок результатов в структуре соответствует порядку оценки - это достигается ценой возможного многократного выполнения одного и того же действия.

[Технически, то, что вам нужно, это исключение срезов аппроксимантов: A является исключением среза (аппроксимаций) B, если для каждого конечного аппроксимата B существует конечный аппроксимат A, такой, что A является исключением B среза B.]

Надеюсь, это поможет.