Какой явный пример монады без монада-трансформатора?

Трансформаторы Monad известны для всех стандартных монадов (Reader, Writer, State, Cont, List и т.д.), Но каждый из этих монадных трансформаторов работает несколько иначе. Не существует общего метода или формулы для построения монадного трансформатора с определением конструктора типа с экземпляром монады. Таким образом, не гарантируется, что тип данных монады, разработанный в соответствии с некоторыми произвольными бизнес-требованиями, будет иметь трансформатор монады. Есть ли такой явный пример?

Связанных с работой

Другой вопрос объясняет, что функторная композиция из двух монад не обязательно является монадой. См. Также этот вопрос. Эти примеры не отвечают на данный вопрос - они просто иллюстрируют проблему отсутствия общего метода построения монадного трансформатора. Эти примеры показывают, что, учитывая две монады M и N, мы иногда обнаруживаем, что M (N a) является монадой, иногда N (M a) является монадой, а иногда и не будет монадой. Но это не показывает, как построить монадный трансформатор для M или N, и не существует ли вообще.

Ответ на другой вопрос утверждает, что монада IO не может иметь трансформатор монады, потому что если бы у него был один IOT, мы могли бы применить IOT к List, а затем, подняв пустой список (lift []) в результирующую монаду, пришлось бы отменить сторону эффекты, выполненные "раньше" монадой IO. Этот аргумент основан на идее о том, что монада IO "фактически выполняет" побочные эффекты, которые, по-видимому, не могут быть отменены. Однако монада IO не является явным конструктором типов.

обсуждение

В каждом примере, где явно задан тип монады, может быть найден какой-то монадный трансформатор - иногда с определенной изобретательностью. Например, трансформатор ListT который существовал в библиотеке Haskell, относительно недавно был обнаружен некорректным тонким способом, но проблема в конечном итоге была устранена путем изменения определения ListT.

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

Кажется, что не существует алгоритма, который автоматически выводит монадные трансформаторы из исходного кода монады. Мы даже знаем, что это всегда возможно?

Чтобы было более ясно, что я подразумеваю под "явным примером" монады: предположим, я утверждаю, что

может иметь законный экземпляр Monad отношению к параметру типа a, и я создаю исходный код для реализации экземпляра Monad для Q uv когда return и join чистые функции. Знаем ли мы тогда, что Q uv имеет монадный трансформатор QT uv такой, что QT uv Id эквивалентен Q uv, и имеют место законы монадных трансформаторов? Знаем ли мы, как построить QT явно? Я не.

Ответы

Ответ 1

Это не ответ, но он слишком большой для комментария. Мы можем написать

{-# LANGUAGE GeneralizedNewtypeDeriving
  , DeriveFunctor #-}

import Control.Monad.Free

-- All the IO primops you could ever need
data IOF a = PutStrLn String a
           | GetLine (String -> a)
           deriving Functor

newtype MyIO a = MyIO {unMyIO :: Free IOF a}
  deriving (Functor, Applicative, Monad)

Но мы можем сделать из этого трансформатор монады:

import Control.Monad.Trans.Free

newtype IOT m a = IOT {unIOT :: FreeT IOF m a}
  deriving (Functor, Applicative, Monad, MonadTrans)

Поэтому я действительно не думаю, что даже IO исключается, хотя изоморфизм в этом случае не является "внутренним".